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 07:55:52 +01:00
parent 7f8adb1640
commit 78fd497d19
1 changed files with 18 additions and 63 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

81
src/subsequences2.v
View File

@ -161,10 +161,6 @@ Proof.
Qed.
(** * Decidability of all definitions
*)
Lemma subsequence_dec_alt {X: Type}:
(forall x y : X, {x = y} + {x <> y})
-> forall (l s : list X), { exists (t: list bool),
@ -172,61 +168,11 @@ Lemma subsequence_dec_alt {X: Type}:
+ { ~ exists (t: list bool),
length t = length l /\ s = map snd (filter fst (combine t l)) }.
Proof.
assert (nil_r: forall (l': list X),
exists (t: list bool),
length t = length l' /\ nil = map snd (filter fst (combine t l'))).
intro. exists (repeat false (length l')). rewrite repeat_length.
split; try induction l'; easy.
assert (nil_cons_r: forall (l': list X) a,
~ (exists (t: list bool),
length t = length (nil: list X)
/\ a::l' = map snd (filter fst (combine t nil)))).
intros. 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.
assert (cons_l: forall (l s: list X) (a: X),
(exists (t: list bool),
length t = length l /\ s = map snd (filter fst (combine t l)))
-> (exists (t: list bool),
length t = length (a::l) /\ s = map snd (filter fst (combine t (a::l))))).
intros l s a. intro H. destruct H. destruct H. exists (false::x).
split; try apply eq_S; assumption.
assert (cons_r: forall (l s: list X) (a: X),
(exists (t: list bool),
length t = length l /\ a::s = map snd (filter fst (combine t l)))
-> (exists (t: list bool),
length t = length l /\ s = map snd (filter fst (combine t l)))).
intro l. induction l. intros. apply nil_cons_r in H.
contradiction H. intros s a0 . intro H. destruct H. destruct H. destruct x.
symmetry in H0. apply nil_cons in H0. contradiction H0.
destruct b. simpl in H0. inversion H0.
exists (false::x). split; try rewrite <- H; reflexivity.
apply cons_l. apply IHl with (a := a0).
exists x. split; inversion H; easy.
assert (cons_eq: forall (l1 l2: list X) (a: X),
(exists (t: list bool),
length t = length (a::l1) /\ (a::l2) = map snd (filter fst (combine t (a::l1))))
<-> (exists (t: list bool),
length t = length l1 /\ l2 = map snd (filter fst (combine t l1)))).
intros l s a. split; intro H; destruct H; destruct H.
destruct x. inversion H0. destruct b. exists x.
split; inversion H; try rewrite H2; inversion H0; reflexivity.
inversion H.
assert (exists (t: list bool),
length t = length l /\ a::s = map snd (filter fst (combine t l))).
exists x. split; assumption. rewrite H2.
apply cons_r with (a := a). assumption.
exists (true :: x). split. apply eq_S. assumption. rewrite H0. reflexivity.
intro H.
intro l. induction l; intro s. destruct s. left. apply nil_r.
right. apply nil_cons_r.
intro l. induction l; intro s. destruct s. left.
rewrite <- subsequence_bools. apply Subsequence_nil_r.
right. rewrite <- subsequence_bools. apply Subsequence_nil_cons_r.
assert (
{ exists (t: list bool),
@ -234,19 +180,28 @@ Proof.
+ { ~ exists (t: list bool),
length t = length l /\ s = map snd (filter fst (combine t l)) }).
apply IHl. destruct H0.
apply IHl.
destruct H0.
rewrite <- subsequence_bools in e.
rewrite <- cons_eq with (a := a) in e.
apply cons_r in e. left; assumption.
rewrite <- Subsequence_cons_eq with (a := a) in e.
apply Subsequence_cons_r in e. rewrite subsequence_bools in e.
left; assumption.
destruct s. left. apply nil_r.
destruct s. rewrite <- subsequence_bools in n.
left.
rewrite <- subsequence_bools.
apply Subsequence_nil_r.
assert ({x=a}+{x<>a}). apply H. destruct H0. rewrite e.
destruct IHl with (s := s); [ left | right ];
rewrite cons_eq; assumption.
rewrite <- subsequence_bools;
rewrite Subsequence_cons_eq. rewrite subsequence_bools. assumption.
rewrite subsequence_bools. assumption.
right. intro I.
destruct I. destruct H0. destruct x0.
symmetry in H1. apply nil_cons in H1. contradiction H1.
symmetry in H1.
apply nil_cons in H1. contradiction H1.
destruct b.
inversion H1. rewrite H3 in n0. easy.
apply n. exists x0; split; inversion H0; easy.