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-05 23:06:31 +01:00
parent 61d38c396d
commit 7f8adb1640
1 changed files with 81 additions and 236 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

317
src/subsequences2.v
View File

@ -157,209 +157,7 @@ Theorem subsequence_bools {X: Type} :
Proof.
intros l s. split; intro. apply subsequence_alt_defs.
apply subsequence_flat_map. assumption.
(** * Various definitions
Different definitions of a subsequence are given; they are proved
below to be equivalent, allowing to choose the most convenient at
any step of a proof.
*)
Definition subsequence {X: Type} (l s : list X) :=
exists (l1: list X) (l2 : list (list X)),
length s = length l2
/\ l = l1 ++ flat_map (fun e => (fst e) :: (snd e)) (combine s l2).
Definition subsequence2 {X: Type} (l s : list X) :=
exists (t: list bool),
length t = length l /\ s = map snd (filter fst (combine t l)).
(** * Elementary properties
*)
Theorem subsequence_nil_r {X: Type}: forall (l : list X), subsequence l nil.
Proof.
intro l. exists l. exists nil. rewrite app_nil_r. split; easy.
Qed.
Theorem subsequence2_nil_r {X: Type} : forall (l : list X), subsequence2 l nil.
Proof.
intro l.
exists (repeat false (length l)). rewrite repeat_length.
split; try induction l; easy.
Qed.
Theorem subsequence_nil_cons_r {X: Type}: forall (l: list X) (a:X),
~ subsequence nil (a::l).
Proof.
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.
apply nil_cons in H0. contradiction H0.
apply nil_cons in H0. contradiction H0.
Qed.
Theorem subsequence2_nil_cons_r {X: Type}: forall (l: list X) (a:X),
~ subsequence2 nil (a::l).
Proof.
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.
Qed.
Theorem subsequence_cons_l {X: Type}: forall (l s: list X) (a: X),
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 {X: Type} : forall (l s: list X) (a: X),
subsequence2 l s -> subsequence2 (a::l) s.
Proof.
intros l s a. intro H. destruct H. destruct H. exists (false::x).
split; try apply eq_S; assumption.
Qed.
Theorem subsequence_cons_r {X: Type} : forall (l s: list X) (a: X),
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. reflexivity.
Qed.
Theorem subsequence2_cons_r {X: Type} : forall (l s: list X) (a: X),
subsequence2 l (a::s) -> subsequence2 l s.
Proof.
intro l. induction l. intros. apply subsequence2_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 subsequence2_cons_l. apply IHl with (a := a0).
exists x. split; inversion H; easy.
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; destruct H; destruct H; destruct H.
destruct x. destruct x0.
apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
inversion H0. exists l0. exists x0.
inversion H. rewrite H3. split; reflexivity.
destruct x0.
apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
exists (x1 ++ (a::l0)). exists x0. inversion H. rewrite H2.
split. reflexivity. inversion H0. rewrite <- app_assoc.
apply app_inv_head_iff. rewrite app_comm_cons. reflexivity.
exists nil. exists (x::x0). simpl.
split; [ rewrite H | rewrite H0 ]; reflexivity.
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; destruct H; destruct H.
destruct x. inversion H0. destruct b. exists (x).
split; inversion H; try rewrite H2; inversion H0; reflexivity.
inversion H. assert (subsequence2 l (a::s)).
exists x. split; assumption.
apply subsequence2_cons_r with (a := a). assumption.
exists (true :: x). split. apply eq_S. assumption. rewrite H0. reflexivity.
Qed.
(** * Equivalence of all definitions
The following three implications are proved:
- subsequence l s -> subsequence2 l s
- subsequence2 l s -> subsequence3 l s
- subsequence3 l s -> subsequence l s
*)
Theorem subsequence_eq_def_1 {X: Type} :
forall l s : list X, subsequence l s -> subsequence2 l s.
Proof.
intros l s. intro H. destruct H. destruct H. destruct H.
exists (
(repeat false (length x)) ++
(flat_map (fun e => true :: (repeat false (length e))) x0)).
split.
rewrite H0. rewrite app_length. rewrite app_length. rewrite repeat_length.
rewrite Nat.add_cancel_l. rewrite flat_map_length. rewrite flat_map_length.
assert (forall v (u: list X),
length u = length v
-> map (fun e => length (fst e :: snd e)) (combine u v)
= map (fun e => length (true :: repeat false (length e))) v).
intro v. induction v; intro u; intro I.
apply length_zero_iff_nil in I. rewrite I. reflexivity.
destruct u. apply O_S in I. contradiction I.
simpl. rewrite IHv. rewrite repeat_length. reflexivity.
inversion I. reflexivity.
rewrite H1; inversion H; reflexivity. rewrite H0.
assert (forall (u: list X) v w,
filter fst (combine (repeat false (length u) ++ v) (u ++ w))
= filter fst (combine v w)).
intro u. induction u; intros v w. reflexivity. simpl. apply IHu.
assert (forall (v: list (list X)) (u : list X),
length u = length v
-> u = map snd (filter fst (combine
(flat_map (fun e => true:: repeat false (length e)) v)
(flat_map (fun e => fst e :: snd e) (combine u v))))).
intro v. induction v; intro u; intro I.
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.
Theorem subsequence_eq_def_2 {X: Type} :
forall l s : list X, subsequence2 l s -> subsequence3 l s.
Proof.
intros l s. intro H. destruct H. destruct H.
assert (I: forall u (v w: list X),
length u = length w
-> v = map snd (filter fst (combine u w))
-> subsequence3 w v).
intro u. induction u; intros v w; intros I J.
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; 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.
apply subsequence_alt_defs2. assumption.
Qed.
@ -367,23 +165,84 @@ Qed.
(** * Decidability of all definitions
*)
Theorem subsequence2_dec {X: Type}:
Lemma subsequence_dec_alt {X: Type}:
(forall x y : X, {x = y} + {x <> y})
-> forall (l s : list X), { subsequence2 l s } + { ~ subsequence2 l s }.
-> forall (l s : list X), { exists (t: list bool),
length t = length l /\ s = map snd (filter fst (combine t l)) }
+ { ~ 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 subsequence2_nil_r.
right. apply subsequence2_nil_cons_r.
intro l. induction l; intro s. destruct s. left. apply nil_r.
right. apply nil_cons_r.
assert({subsequence2 l s} + {~ subsequence2 l s}). apply IHl. destruct H0.
assert (
{ exists (t: list bool),
length t = length l /\ s = map snd (filter fst (combine t l)) }
+ { ~ exists (t: list bool),
length t = length l /\ s = map snd (filter fst (combine t l)) }).
rewrite <- subsequence2_cons_eq with (a := a) in s0.
apply subsequence2_cons_r in s0. left; assumption.
apply IHl. destruct H0.
destruct s. left. apply subsequence2_nil_r.
rewrite <- cons_eq with (a := a) in e.
apply cons_r in e. left; assumption.
destruct s. left. apply nil_r.
assert ({x=a}+{x<>a}). apply H. destruct H0. rewrite e.
destruct IHl with (s := s); [ left | right ];
rewrite subsequence2_cons_eq; assumption.
rewrite cons_eq; assumption.
right. intro I.
destruct I. destruct H0. destruct x0.
@ -394,33 +253,19 @@ Proof.
Qed.
Theorem subsequence3_dec {X: Type}:
Theorem Subsequence_dec {X: Type}:
(forall x y : X, {x = y} + {x <> y})
-> forall (l s : list X), { subsequence3 l s } + { ~ subsequence3 l s }.
-> 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.
apply subsequence_eq_def_2 in s0. left. assumption.
right. intro I.
apply subsequence_eq_def_3 in I.
apply subsequence_eq_def_1 in I.
apply n in I. contradiction I.
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 ({ subsequence3 l s } + { ~ subsequence3 l s }).
apply subsequence3_dec. assumption. destruct H0.
apply subsequence_eq_def_3 in s0. left. assumption.
right. intro I.
apply subsequence_eq_def_1 in I.
apply subsequence_eq_def_2 in I.
apply n in I. contradiction I.
assert (
{ exists (t: list bool),
length t = length l /\ s = map snd (filter fst (combine t l)) }
+ { ~ exists (t: list bool),
length t = length l /\ s = map snd (filter fst (combine t l)) }).
apply subsequence_dec_alt. assumption. destruct H0.
rewrite <- subsequence_bools in e. left. assumption.
right. intro I. apply subsequence_bools in I. apply n in I. contradiction I.
Qed.