Update
This commit is contained in:
parent
5212fb691f
commit
86bc880092
@ -462,29 +462,32 @@ Proof.
|
|||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
|
Theorem Subsequence_filter {X: Type} :
|
||||||
|
forall (u v: list X) f, Subsequence (filter f u) v -> Subsequence u v.
|
||||||
|
|
||||||
Theorem subsequence_filter {X: Type} :
|
|
||||||
forall (u v: list X) f, subsequence (filter f u) v -> subsequence u v.
|
|
||||||
Proof.
|
Proof.
|
||||||
intro u. induction u; intros v f; intro H. assumption.
|
intro u. induction u; intros v f; intro H. assumption.
|
||||||
simpl in H. destruct (f a). assert (K := H).
|
simpl in H. destruct (f a). assert (K := H).
|
||||||
apply subsequence_eq_def_1 in H. destruct H. destruct H.
|
apply Subsequence_bools in H.
|
||||||
|
destruct H. destruct H.
|
||||||
destruct x. apply O_S in H. contradiction. destruct b.
|
destruct x. apply O_S in H. contradiction. destruct b.
|
||||||
destruct v. apply subsequence_nil_r. assert (x0 = a). inversion H0.
|
destruct v. apply Subsequence_nil_r. assert (x0 = a). inversion H0.
|
||||||
reflexivity. rewrite H1.
|
reflexivity. rewrite H1.
|
||||||
apply subsequence_eq_def_3. exists nil. exists u. split. reflexivity.
|
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 IHu with (f := f). rewrite H1 in K.
|
||||||
apply subsequence_double_cons in K. assumption.
|
apply Subsequence_double_cons in K. assumption.
|
||||||
apply subsequence_cons_l. apply IHu with (f := f).
|
apply Subsequence_cons_l. apply IHu with (f := f).
|
||||||
apply subsequence_eq_def_3. apply subsequence_eq_def_2.
|
apply Subsequence_bools.
|
||||||
exists x. split. inversion H. reflexivity. apply H0.
|
exists x. split. inversion H. reflexivity. apply H0.
|
||||||
apply subsequence_cons_l. apply IHu with (f := f). assumption.
|
apply Subsequence_cons_l. apply IHu with (f := f). assumption.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
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.
|
||||||
|
Loading…
x
Reference in New Issue
Block a user