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:03:37 +01:00
parent d62a5752ae
commit 23a6870a6a
1 changed files with 20 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

40
src/subsequences.v
View File

@ -142,7 +142,7 @@ Qed.
Theorem subsequence_cons_eq {X: Type} : forall (l1 l2: list X) (a: X),
subsequence (a::l1) (a::l2) <-> subsequence l1 l2.
Proof.
intros l s a. split. intro H.
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.
@ -154,7 +154,7 @@ Proof.
inversion H0. rewrite <- app_assoc. apply app_inv_head_iff.
rewrite app_comm_cons. reflexivity.
intro H. destruct H. destruct H. destruct H.
destruct H. destruct H. destruct H.
exists nil. exists (x::x0). simpl. split. rewrite H. reflexivity.
rewrite H0. reflexivity.
Qed.
@ -163,14 +163,14 @@ Qed.
Theorem subsequence2_cons_eq {X: Type}: forall (l1 l2: list X) (a: X),
subsequence2 (a::l1) (a::l2) <-> subsequence2 l1 l2.
Proof.
intros l s a. split. intro H. unfold subsequence2 in H.
destruct H. destruct H. destruct x. inversion H0.
intros l s a. split; intro H; destruct H; destruct H.
destruct x. inversion H0.
destruct b. exists (x). split. inversion H. rewrite H2. reflexivity. simpl in H0.
inversion H0. reflexivity. simpl in H0. inversion H.
assert (subsequence2 l (a::s)). exists x. split; assumption.
apply subsequence2_cons_r with (a := a). assumption.
intro H. destruct H. destruct H. exists (true :: x).
split. simpl. apply eq_S. assumption. simpl. rewrite H0. reflexivity.
exists (true :: x).
split. simpl. apply eq_S. assumption. rewrite H0. reflexivity.
Qed.
@ -314,6 +314,19 @@ Proof.
Qed.
Theorem subsequence_dec {X: Type}:
(forall x y : X, {x = y} + {x <> y})
-> forall (l s : list X), { subsequence l s } + { ~ subsequence l s }.
Proof.
intro H. intros l s.
assert ({ subsequence2 l s } + { ~ subsequence2 l s }).
apply subsequence2_dec. assumption. destruct H0.
rewrite <- subsequence_eq_def_2 in s0. left. assumption.
assumption. rewrite <- subsequence_eq_def_2 in n. right. assumption.
assumption.
Qed.
Theorem subsequence_eq_def_3 {X: Type} :
(forall (x y : X), {x = y} + {x <> y})
-> (forall l s : list X, subsequence l s <-> subsequence3 l s).
@ -349,19 +362,6 @@ Proof.
Qed.
Theorem subsequence_dec {X: Type}:
(forall x y : X, {x = y} + {x <> y})
-> forall (l s : list X), { subsequence l s } + { ~ subsequence l s }.
Proof.
intro H. intros l s.
assert ({ subsequence2 l s } + { ~ subsequence2 l s }).
apply subsequence2_dec. assumption. destruct H0.
rewrite <- subsequence_eq_def_2 in s0. left. assumption.
assumption. rewrite <- subsequence_eq_def_2 in n. right. assumption.
assumption.
Qed.
@ -381,7 +381,7 @@ Qed.
Example test3: subsequence [1;2;3;4;5] [1;3;5].
Proof.
rewrite subsequence_eq_def.
rewrite subsequence_eq_def_2.
exists [true; false; true; false; true].
split; reflexivity.
apply Nat.eq_dec.