Update
This commit is contained in:
parent
4b4f52756f
commit
58a834c275
@ -620,24 +620,6 @@ Proof.
|
||||
Qed.
|
||||
|
||||
|
||||
Theorem subsequence_filter_2 {X: Type} :
|
||||
forall (u v: list X) f,
|
||||
subsequence u v -> subsequence (filter f u) (filter f v).
|
||||
Proof.
|
||||
(*
|
||||
intro u. induction u; intros v f; intro H.
|
||||
assert (v = nil). destruct v. reflexivity.
|
||||
apply subsequence_eq_def_1 in H. apply subsequence_eq_def_2 in H.
|
||||
destruct H. destruct H. destruct H.
|
||||
destruct x0; apply nil_cons in H; contradiction.
|
||||
rewrite H0. apply subsequence_nil_r.
|
||||
simpl. destruct (f a).
|
||||
*)
|
||||
intros u v. generalize u. induction v; intros u0 f; intro H.
|
||||
apply subsequence_nil_r. simpl. destruct (f a).
|
||||
apply subsequence_cons_r.
|
||||
|
||||
|
||||
Theorem subsequence_incl {X: Type} :
|
||||
forall (u v: list X), subsequence u v -> incl v u.
|
||||
Proof.
|
||||
@ -696,6 +678,78 @@ Proof.
|
||||
Qed.
|
||||
|
||||
|
||||
Theorem subsequence_split_2 {X: Type} :
|
||||
forall (u v w: list X),
|
||||
subsequence u (v++w)
|
||||
-> (exists a b, u = a++b /\ (subsequence a v) /\ subsequence b w).
|
||||
Proof.
|
||||
intros u v w. intro H. destruct H. destruct H. destruct H.
|
||||
exists (x ++
|
||||
flat_map (fun e : X * list X => fst e :: snd e) (combine v x0)).
|
||||
exists (
|
||||
flat_map (fun e : X * list X => fst e :: snd e)
|
||||
(combine w (skipn (length v) x0))).
|
||||
split. rewrite H0. rewrite <- app_assoc. apply app_inv_head_iff.
|
||||
rewrite <- flat_map_app.
|
||||
|
||||
assert (L: forall (w y: list X) (z : list (list X)),
|
||||
length z = length w + length y ->
|
||||
combine (w ++ y) z = combine w z ++ combine y (skipn (length w) z)).
|
||||
intros w0. induction w0; intros y z; intro I. reflexivity.
|
||||
destruct z. simpl. rewrite combine_nil. reflexivity.
|
||||
simpl. rewrite IHw0. reflexivity. inversion I. reflexivity.
|
||||
rewrite L. reflexivity. rewrite app_length in H. rewrite H.
|
||||
reflexivity. split.
|
||||
exists x. exists (firstn (length v) x0). split.
|
||||
rewrite firstn_length. rewrite <- H. rewrite app_length.
|
||||
rewrite min_l. reflexivity. apply PeanoNat.Nat.le_add_r.
|
||||
rewrite combine_firstn_l. reflexivity.
|
||||
|
||||
exists nil. exists (skipn (length v) x0). split.
|
||||
rewrite app_length in H. rewrite skipn_length. rewrite <- H.
|
||||
rewrite PeanoNat.Nat.add_sub_swap. rewrite PeanoNat.Nat.sub_diag.
|
||||
reflexivity. reflexivity. reflexivity.
|
||||
Qed.
|
||||
|
||||
|
||||
Theorem subsequence_filter_2 {X: Type} :
|
||||
forall (u v: list X) f,
|
||||
subsequence u v -> subsequence (filter f u) (filter f v).
|
||||
Proof.
|
||||
(*
|
||||
intro u. induction u; intros v f; intro H.
|
||||
assert (v = nil). destruct v. reflexivity.
|
||||
apply subsequence_eq_def_1 in H. apply subsequence_eq_def_2 in H.
|
||||
destruct H. destruct H. destruct H.
|
||||
destruct x0; apply nil_cons in H; contradiction.
|
||||
rewrite H0. apply subsequence_nil_r.
|
||||
simpl. destruct (f a).
|
||||
*)
|
||||
intros u v. generalize u. induction v; intros u0 f; intro H.
|
||||
apply subsequence_nil_r.
|
||||
|
||||
assert (f a = true \/ f a = false).
|
||||
destruct (f a); [ left | right ]; reflexivity. destruct H0.
|
||||
simpl. rewrite H0.
|
||||
replace (a::v) with ([a] ++ v) in H. apply subsequence_split in H.
|
||||
|
||||
|
||||
|
||||
|
||||
destruct H. destruct H. destruct x0. destruct H.
|
||||
apply PeanoNat.Nat.neq_succ_0 in H. contradiction.
|
||||
destruct H. simpl in H0. rewrite H0.
|
||||
|
||||
|
||||
|
||||
simpl. destruct (f a).
|
||||
|
||||
|
||||
|
||||
apply subsequence_cons_r.
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
(** * Tests
|
||||
@ -800,7 +854,6 @@ Proof.
|
||||
apply subsequence_cons_l. assumption.
|
||||
Qed.
|
||||
|
||||
|
||||
Theorem smerge_subsequence2 {X: Type}:
|
||||
(forall x y : X, {x = y} + {x <> y})
|
||||
-> forall (l s1 s2: list X), smerge l s1 s2 -> subsequence l s2.
|
||||
|
Loading…
x
Reference in New Issue
Block a user