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 08:21:51 +01:00
parent 2b0a214352
commit 82bc79b245
1 changed files with 12 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

29
src/subsequences2.v
View File

@ -223,21 +223,12 @@ Proof.
Qed. Qed.
Theorem Subsequence_trans {X: Type} :
Theorem subsequence_trans {X: Type} :
forall (l1 l2 l3: list X), forall (l1 l2 l3: list X),
subsequence l1 l2 -> subsequence l2 l3 -> subsequence l1 l3. Subsequence l1 l2 -> Subsequence l2 l3 -> Subsequence l1 l3.
Proof. Proof.
intros l1 l2 l3. intros H I. intros l1 l2 l3. intros H I. apply Subsequence_bools.
apply subsequence_eq_def_3. apply subsequence_eq_def_2. apply Subsequence_flat_map in H. apply Subsequence_bools in I.
apply subsequence_eq_def_1 in I.
destruct H. destruct H. destruct H. destruct I. destruct H1. destruct H. destruct H. destruct H. destruct I. destruct H1.
exists ( exists (
(repeat false (length x)) ++ (repeat false (length x)) ++
@ -301,12 +292,11 @@ Proof.
Qed. Qed.
Lemma subsequence_length {X: Type} : Theorem Subsequence_length {X: Type} :
forall (u v: list X), subsequence u v -> length v <= length u. forall (u v: list X), Subsequence u v -> length v <= length u.
Proof. Proof.
intros u v. generalize u. induction v; intro u0; intro H. apply Nat.le_0_l. intros u v. generalize u. induction v; intro u0; intro H. apply Nat.le_0_l.
apply subsequence_eq_def_1 in H. apply subsequence_eq_def_2 in H. destruct H. destruct H. destruct H.
destruct H. destruct H. destruct H. apply subsequence_eq_def_3 in H0.
apply IHv in H0. simpl. apply Nat.le_succ_l. rewrite H. apply IHv in H0. simpl. apply Nat.le_succ_l. rewrite H.
rewrite app_length. apply Nat.lt_lt_add_l. rewrite app_length. apply Nat.lt_lt_add_l.
rewrite <- Nat.le_succ_l. simpl. rewrite <- Nat.succ_le_mono. rewrite <- Nat.le_succ_l. simpl. rewrite <- Nat.succ_le_mono.
@ -314,6 +304,11 @@ Proof.
Qed. Qed.
Theorem subsequence_eq {X: Type} : Theorem subsequence_eq {X: Type} :
forall (u v: list X), forall (u v: list X),
subsequence u v -> subsequence v u -> u = v. subsequence u v -> subsequence v u -> u = v.