baruchel/coqbooks
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Update

Browse Source
This commit is contained in:
Thomas Baruchel 2023-11-23 18:35:58 +01:00
parent 35672797f1
commit 5158370a77
1 changed files with 23 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

25
src/subsequences.v
View File

@ -742,8 +742,7 @@ Proof.
assert (subsequence ((filter f x) ++ (filter f x0))
((filter f [a]) ++ (filter f v))).
apply subsequence_app. simpl. rewrite H0.
apply subsequence_incl in H1. apply incl_cons_inv in H1.
destruct H1.
apply subsequence_incl in H1. apply incl_cons_inv in H1. destruct H1.
assert (In a (filter f x)). apply filter_In. split; assumption.
apply subsequence_in. assumption. apply IHv. assumption.
rewrite <- filter_app in H3. rewrite <- H in H3. simpl in H3.
@ -752,3 +751,25 @@ Proof.
assumption.
Qed.
Theorem subsequence_add {X: Type} :
forall (u v w: list X) x, subsequence u v -> Add x u w -> subsequence w v.
Proof.
intros u v w. generalize u v. induction w; intros u0 v0 x; intro H.
intro I. inversion I. intro I. inversion I.
rewrite <- H2. apply subsequence_cons_l. rewrite <- H3. assumption.
assert (J := H). apply subsequence_eq_def_1 in H. rewrite <- H1 in H.
rewrite H0 in H. destruct H. destruct H.
destruct x1. apply O_S in H. contradiction. destruct b.
rewrite H4. simpl. apply subsequence_double_cons.
apply IHw with (u := l) (x := x).
apply subsequence_eq_def_3. apply subsequence_eq_def_2. exists x1.
inversion H. split; reflexivity. assumption.
apply subsequence_cons_r with (a:=a).
rewrite H4. simpl. apply subsequence_double_cons.
apply IHw with (u := l) (x := x).
apply subsequence_eq_def_3. apply subsequence_eq_def_2. exists x1.
inversion H. split; reflexivity. assumption.
Qed.