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

Update

This commit is contained in:
Thomas Baruchel 2023-10-31 09:19:23 +01:00
parent f2e18972d0
commit 5e73d31a1e
1 changed files with 13 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

28
src/subsequences.v
View File

@ -44,7 +44,7 @@ Qed.
Theorem subsequence_nil_cons_r {X: Type}: forall (l: list X) (a:X),
~ subsequence nil (a::l).
Proof.
intros l a. unfold not. intro H.
intros l a. intro H.
destruct H. destruct H. destruct H.
destruct x. rewrite app_nil_l in H0.
destruct x0. apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
@ -56,7 +56,7 @@ Qed.
Theorem subsequence2_nil_cons_r {X: Type}: forall (l: list X) (a:X),
~ subsequence2 nil (a::l).
Proof.
intros l a. unfold not. intro H. destruct H.
intros l a. intro H. destruct H.
destruct H. assert (x = nil). destruct x. reflexivity.
apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
rewrite H1 in H0. symmetry in H0. apply nil_cons in H0. contradiction H0.
@ -66,7 +66,7 @@ Qed.
Theorem subsequence3_nil_cons_r {X: Type}: forall (l: list X) (a:X),
~ subsequence3 nil (a::l).
Proof.
intros l a. unfold not. intro H. destruct H. destruct H. destruct H.
intros l a. intro H. destruct H. destruct H. destruct H.
destruct x. simpl in H. apply nil_cons in H. contradiction H.
simpl in H. apply nil_cons in H. contradiction H.
Qed.
@ -122,7 +122,7 @@ Proof.
destruct b. simpl in H0. inversion H0.
exists (false::x). split; try rewrite <- H; reflexivity.
simpl in H0. apply subsequence2_cons_l. apply IHl with (a := a0).
unfold subsequence2. exists (x). split. inversion H.
exists (x). split. inversion H.
reflexivity. assumption.
Qed.
@ -145,7 +145,7 @@ 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 H0. exists l0. exists x0.
inversion H. rewrite H3. split; reflexivity.
destruct x0.
apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
@ -220,10 +220,10 @@ Theorem subsequence2_dec {X: Type}:
-> forall (l s : list X), { subsequence2 l s } + { ~ subsequence2 l s }.
Proof.
intro H.
intro l. induction l. intro s. destruct s. left. apply subsequence2_nil_r.
intro l. induction l; intro s. destruct s. left. apply subsequence2_nil_r.
right. apply subsequence2_nil_cons_r.
intro s. assert({subsequence2 l s} + {~ subsequence2 l s}). apply IHl.
assert({subsequence2 l s} + {~ subsequence2 l s}). apply IHl.
destruct H0.
rewrite <- subsequence2_cons_eq with (a := a) in s0.
@ -231,11 +231,10 @@ Proof.
destruct s. left. apply subsequence2_nil_r.
assert ({x=a}+{x<>a}). apply H. destruct H0. rewrite e.
destruct IHl with (s := s).
left. rewrite subsequence2_cons_eq. assumption.
right. rewrite subsequence2_cons_eq. assumption.
destruct IHl with (s := s); [ left | right ];
rewrite subsequence2_cons_eq; assumption.
right. unfold not in n. unfold not. intro I.
right. intro I.
destruct I. destruct H0. destruct x0.
symmetry in H1. apply nil_cons in H1. contradiction H1.
destruct b.
@ -261,11 +260,10 @@ Proof.
destruct s. left. apply subsequence3_nil_r.
assert ({x=a}+{x<>a}). apply H. destruct H0. rewrite e.
destruct IHl with (s := s).
left. rewrite subsequence3_cons_eq. assumption.
right. rewrite subsequence3_cons_eq. assumption.
destruct IHl with (s := s); [ left | right ];
rewrite subsequence3_cons_eq; assumption.
right. unfold not in n. unfold not. intro I.
right. intro I.
destruct I. destruct H0. destruct H0. destruct x0.
inversion H0. rewrite H3 in n0. contradiction n0. reflexivity.