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-12-06 09:51:37 +01:00
parent 85bda82049
commit 9ad87a7470
1 changed files with 10 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
src/subsequences2.v
View File

@ -500,17 +500,13 @@ Proof.
Qed. Qed.
Theorem Subsequence_split {X: Type} :
Theorem subsequence_split {X: Type} :
forall (u v w: list X), forall (u v w: list X),
subsequence (u++v) w Subsequence (u++v) w
-> (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. destruct H. destruct H. apply Subsequence_bools in 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)
@ -535,13 +531,18 @@ Proof.
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. rewrite L. rewrite <- H. split. assumption.
split; apply subsequence_eq_def_3; apply subsequence_eq_def_2; split; apply Subsequence_bools;
[ exists x0 | exists x1]; split; try assumption; reflexivity. [ exists x0 | exists x1]; split; try assumption; reflexivity.
assumption. assumption.
Qed. Qed.
Theorem subsequence_split_2 {X: Type} : Theorem subsequence_split_2 {X: Type} :
forall (u v w: list X), forall (u v w: list X),
subsequence u (v++w) subsequence u (v++w)