Update
This commit is contained in:
parent
d3cb1fc175
commit
cc4b168720
@ -584,6 +584,64 @@ Theorem subsequence_map {X Y: Type} :
|
|||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
|
Theorem subsequence_double_cons {X: Type} :
|
||||||
|
forall (u v: list X) a, subsequence (a::u) (a::v) -> subsequence u v.
|
||||||
|
Proof.
|
||||||
|
intros u v a. intro H. destruct H. destruct H. destruct H.
|
||||||
|
destruct x; destruct x0. symmetry in H0. apply nil_cons in H0.
|
||||||
|
contradiction. inversion H0.
|
||||||
|
exists l. exists x0. split. inversion H. reflexivity. reflexivity.
|
||||||
|
apply PeanoNat.Nat.neq_succ_0 in H. contradiction.
|
||||||
|
inversion H0. exists (x1++x::l). exists x0. split. inversion H.
|
||||||
|
reflexivity. rewrite <- app_assoc. reflexivity.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
|
Theorem subsequence_filter {X: Type} :
|
||||||
|
forall (u v: list X) f, subsequence (filter f u) v -> subsequence u v.
|
||||||
|
Proof.
|
||||||
|
intro u. induction u; intros v f; intro H. assumption.
|
||||||
|
simpl in H. destruct (f a). assert (K := H).
|
||||||
|
apply subsequence_eq_def_1 in H. destruct H. destruct H.
|
||||||
|
destruct x. apply O_S in H. contradiction. destruct b.
|
||||||
|
destruct v. apply subsequence_nil_r. assert (x0 = a). inversion H0.
|
||||||
|
reflexivity. rewrite H1.
|
||||||
|
apply subsequence_eq_def_3. exists nil. exists u. split. reflexivity.
|
||||||
|
apply subsequence_eq_def_2. apply subsequence_eq_def_1.
|
||||||
|
apply IHu with (f := f). rewrite H1 in K.
|
||||||
|
apply subsequence_double_cons in K. assumption.
|
||||||
|
apply subsequence_cons_l. apply IHu with (f := f).
|
||||||
|
apply subsequence_eq_def_3. apply subsequence_eq_def_2.
|
||||||
|
exists x. split. inversion H. reflexivity. apply H0.
|
||||||
|
apply subsequence_cons_l. apply IHu with (f := f). assumption.
|
||||||
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
|
Theorem subsequence_filter {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_trans {X: Type} :
|
||||||
|
forall (l1 l2 l3: list X),
|
||||||
|
subsequence l1 l2 -> subsequence l2 l3 -> subsequence l1 l3.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
Theorem subsequence_incl {X: Type} :
|
Theorem subsequence_incl {X: Type} :
|
||||||
forall (u v: list X), subsequence u v -> incl v u.
|
forall (u v: list X), subsequence u v -> incl v u.
|
||||||
Proof.
|
Proof.
|
||||||
@ -610,14 +668,12 @@ Theorem subsequence_split {X: Type} :
|
|||||||
-> (exists a b, w = a++b /\ (subsequence u a) /\ subsequence v b).
|
-> (exists a b, w = a++b /\ (subsequence u a) /\ subsequence v b).
|
||||||
Proof.
|
Proof.
|
||||||
intros u v w. intro H.
|
intros u v w. intro H.
|
||||||
apply subsequence_eq_def_1 in H.
|
apply subsequence_eq_def_1 in H. destruct H. destruct H.
|
||||||
destruct H. destruct H.
|
|
||||||
|
|
||||||
assert (forall (b: list bool) (u v: list X),
|
assert (forall (b: list bool) (u v: list X),
|
||||||
length b = length (u++v)
|
length b = length (u++v)
|
||||||
-> exists x y, b = x++y /\ length x = length u /\ length y = length v).
|
-> exists x y, b = x++y /\ length x = length u /\ length y = length v).
|
||||||
intros b u0 v0. intro I.
|
intros b u0 v0. intro I. rewrite app_length in I.
|
||||||
rewrite app_length in I.
|
|
||||||
exists (firstn (length u0) b). exists (skipn (length u0) b).
|
exists (firstn (length u0) b). exists (skipn (length u0) b).
|
||||||
split. symmetry. apply firstn_skipn. split.
|
split. symmetry. apply firstn_skipn. split.
|
||||||
rewrite firstn_length_le. reflexivity. rewrite I.
|
rewrite firstn_length_le. reflexivity. rewrite I.
|
||||||
@ -633,16 +689,12 @@ Proof.
|
|||||||
assert (L: forall (g i: list bool) (h j: list X), length g = length h
|
assert (L: forall (g i: list bool) (h j: list X), length g = length h
|
||||||
-> (combine g h) ++ (combine i j) = combine (g++i) (h++j)).
|
-> (combine g h) ++ (combine i j) = combine (g++i) (h++j)).
|
||||||
intro g. induction g; intros i h j; intro I.
|
intro g. induction g; intros i h j; intro I.
|
||||||
symmetry in I. apply length_zero_iff_nil in I. rewrite I.
|
symmetry in I. apply length_zero_iff_nil in I. rewrite I. reflexivity.
|
||||||
reflexivity.
|
|
||||||
destruct h. apply PeanoNat.Nat.neq_succ_0 in I. contradiction.
|
destruct h. apply PeanoNat.Nat.neq_succ_0 in I. contradiction.
|
||||||
simpl. rewrite IHg. reflexivity. inversion I. reflexivity.
|
simpl. rewrite IHg. reflexivity. inversion I. reflexivity.
|
||||||
rewrite L. rewrite <- H. split. assumption. split.
|
rewrite L. rewrite <- H. split. assumption.
|
||||||
|
split; apply subsequence_eq_def_3; apply subsequence_eq_def_2;
|
||||||
apply subsequence_eq_def_3. apply subsequence_eq_def_2.
|
[ exists x0 | exists x1]; split; try assumption; reflexivity.
|
||||||
exists x0. split. assumption. reflexivity.
|
|
||||||
apply subsequence_eq_def_3. apply subsequence_eq_def_2.
|
|
||||||
exists x1. split. assumption. reflexivity.
|
|
||||||
|
|
||||||
assumption.
|
assumption.
|
||||||
Qed.
|
Qed.
|
||||||
|
Loading…
Reference in New Issue
Block a user