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

Compare commits

base: baruchel:00cf74be9c8bf45562d99b23a45657758e64db39
Branches Tags
baruchel:master
...
compare: baruchel:d80ca6b8bb940d2b5e4fd4f5a53d94a5007f7cd4
Branches Tags
baruchel:master

3 Commits
00cf74be9c ... d80ca6b8bb

Author SHA1 Message Date
Thomas Baruchel
d80ca6b8bb Update 2023-11-01 21:40:10 +01:00
Thomas Baruchel
43d97734b2 Update 2023-11-01 21:08:36 +01:00
Thomas Baruchel
24d88f1928 Update 2023-11-01 21:06:13 +01:00
1 changed files with 9 additions and 17 deletions
Show Stats Expand all files Collapse all files

26
src/subsequences.v
View File

@ -232,7 +232,6 @@ Proof.
apply length_zero_iff_nil in I. rewrite I. reflexivity.
destruct u. apply O_S in I. contradiction I.
simpl. rewrite H1. rewrite <- IHv; inversion I; reflexivity.
rewrite H1. rewrite <- H2; inversion H; reflexivity.
Qed.
@ -250,15 +249,11 @@ Proof.
rewrite J. apply subsequence3_nil_r.
destruct v. apply subsequence3_nil_r.
destruct w. apply Nat.neq_succ_0 in I. contradiction I.
destruct a. exists nil. exists w.
inversion J. apply IHu in H3.
split. reflexivity. inversion J. rewrite <- H5. assumption.
inversion I. reflexivity. simpl in J.
assert (subsequence3 w (x0::v)). apply IHu.
inversion I. reflexivity. assumption.
apply subsequence3_cons_l. assumption.
destruct a. exists nil. exists w. inversion J.
apply IHu in H3. split; inversion J; try rewrite <- H5; easy.
inversion I. reflexivity.
assert (subsequence3 w (x0::v)). apply IHu; inversion I; easy.
apply subsequence3_cons_l; assumption.
apply I with (u := x); assumption.
Qed.
@ -299,10 +294,8 @@ Proof.
destruct I. destruct H0. destruct x0.
symmetry in H1. apply nil_cons in H1. contradiction H1.
destruct b.
inversion H1. rewrite H3 in n0. contradiction n0. reflexivity.
assert (subsequence2 l (x::s)). exists x0. split; inversion H0; easy.
apply n in H2. contradiction H2.
inversion H1. rewrite H3 in n0. easy.
apply n. exists x0; split; inversion H0; easy.
Qed.
@ -430,9 +423,8 @@ Proof.
apply length_zero_iff_nil in I. rewrite I. reflexivity.
destruct u0. reflexivity. destruct v0.
apply PeanoNat.Nat.neq_succ_0 in J; contradiction J.
destruct b; simpl; rewrite K; rewrite IHw.
reflexivity. inversion I; reflexivity. inversion J; reflexivity.
reflexivity. inversion I; reflexivity. inversion J; reflexivity.
destruct b; simpl; rewrite K; rewrite IHw;
inversion I; inversion J; reflexivity.
rewrite H4; try rewrite H1; try rewrite H; reflexivity.
Qed.