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 10:57:47 +01:00
parent 9cdf76a97f
commit 26ddf37f50
1 changed files with 33 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

56
src/subsequences.v
View File

@ -60,6 +60,16 @@ Proof.
Qed.
Theorem subsequence_cons_l : forall (l s: list Type) (a: Type),
subsequence l s -> subsequence (a::l) s.
Proof.
intros l s a. intro H.
destruct H. destruct H. destruct H.
exists (a::x). exists x0. split. assumption.
rewrite H0. reflexivity.
Qed.
Theorem subsequence2_cons_l : forall (l s: list Type) (a: Type),
subsequence2 l s -> subsequence2 (a::l) s.
Proof.
@ -70,6 +80,21 @@ Proof.
Qed.
Theorem subsequence_cons_r : forall (l s: list Type) (a: Type),
subsequence l (a::s) -> subsequence l s.
Proof.
intros l s a. intro H. destruct H. destruct H. destruct H.
destruct x0. apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
exists (x++a::l0). exists x0. split. inversion H. reflexivity. rewrite H0.
rewrite <- app_assoc. apply app_inv_head_iff. simpl. reflexivity.
Qed.
Theorem subsequence2_cons_r : forall (l s: list Type) (a: Type),
subsequence2 l (a::s) -> subsequence2 l s.
Proof.
@ -168,27 +193,10 @@ Proof.
Qed.
Theorem subsequence2_dec :
(forall x y : Type, {x = y} + {x <> y})
-> forall (l s : list Type), { subsequence2 l s } + { ~ subsequence2 l s }.
Proof.
intro H.
intros l s. generalize l. induction s. left. apply subsequence2_nil_r.
intro l0. destruct l0. right. apply subsequence2_nil_cons_r.
assert ({ subsequence2 l0 s } + { ~ subsequence2 l0 s }). apply IHs.
assert ({T=a}+{T<>a}). apply H. destruct H0; destruct H1.
left. unfold subsequence2. unfold subsequence2 in s0. destruct s0.
destruct H0. exists (true::x). simpl. rewrite H0. split. reflexivity.
rewrite e. rewrite H1. reflexivity.
(*
assert ({In a l0}+{~ In a l0}). apply In_dec. assumption.
destruct H0. apply In_split in i. destruct i.
*)
(*
Theorem subsequence_dec : forall (l s : list Type),
{ subsequence l s } + { ~ subsequence l s }.
Proof.
@ -250,12 +258,14 @@ Proof.
*)
Theorem subsequence_eq_def : forall l s, subsequence l s <-> subsequence2 l s.
Theorem subsequence_eq_def :
(forall x y : Type, {x = y} + {x <> y})
-> (forall l s, subsequence l s <-> subsequence2 l s).
Proof.
intro l. induction l.
intro I. intro l. induction l.
(* first part of the induction *)
intro s. unfold subsequence. unfold subsequence2.
split. exists nil. split. reflexivity. simpl.
@ -286,8 +296,8 @@ Proof.
exists (a::l). exists (nil). simpl. split; try rewrite app_nil_r; reflexivity.
(* deux cas : a = n ou non *)
assert ({a=n} + {a<>n}). apply PeanoNat.Nat.eq_dec. destruct H.
unfold subsequence. unfold subsequence2. split.
assert ({a=T} + {a<>T}). apply I. destruct H.
rewrite e. rewrite subsequence2_cons_eq. rewrite <- IHl.