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-22 15:31:40 +01:00
parent dedf79490b
commit 57df938818
1 changed files with 6 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
src/subsequences.v
View File

@ -508,8 +508,10 @@ Proof.
Qed.
Theorem subsequence_reverse {X: Type} :
forall (u v: list X), subsequence u v -> subsequence (rev u) (rev v).
forall (u v: list X), subsequence u v <-> subsequence (rev u) (rev v).
Proof.
assert (MAIN: forall (u v: list X),
subsequence u v -> subsequence (rev u) (rev v)).
intros u v. intro H.
apply subsequence_eq_def_3. apply subsequence_eq_def_2.
apply subsequence_eq_def_1 in H. destruct H. destruct H.
@ -538,6 +540,9 @@ Proof.
simpl. destruct (v0 a). simpl. rewrite IHw. reflexivity.
rewrite IHw. symmetry. apply app_nil_r. rewrite LEMMA3.
reflexivity. assumption.
split. apply MAIN. intro H. apply MAIN in H.
rewrite rev_involutive in H. rewrite rev_involutive in H.
assumption.
Qed.