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-10-30 12:33:00 +01:00
parent 26ddf37f50
commit 61c8077d6c
1 changed files with 25 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

30
src/subsequences.v
View File

@ -90,11 +90,6 @@ Proof.
Qed.
Theorem subsequence2_cons_r : forall (l s: list Type) (a: Type),
subsequence2 l (a::s) -> subsequence2 l s.
Proof.
@ -109,6 +104,31 @@ Proof.
Qed.
Theorem subsequence_cons_eq : forall (l1 l2: list Type) (a: Type),
subsequence (a::l1) (a::l2) <-> subsequence l1 l2.
Proof.
intros l s a. split. intro H.
destruct H. destruct H. destruct H.
destruct x. destruct x0.
apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
simpl in H0. inversion H0. exists l0. exists x0.
inversion H. split; reflexivity.
destruct x0. simpl in H0.
apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
exists (x ++ (a::l0)). exists x0. inversion H. split. reflexivity.
inversion H0. rewrite <- app_assoc. apply app_inv_head_iff.
rewrite app_comm_cons. reflexivity.
intro H. destruct H. destruct H. destruct H.
exists nil. exists (x::x0). simpl. split. rewrite H. reflexivity.
rewrite H0. reflexivity.
Qed.
Theorem subsequence2_cons_eq : forall (l1 l2: list Type) (a: Type),
subsequence2 (a::l1) (a::l2) <-> subsequence2 l1 l2.
Proof.