This commit is contained in:
Thomas Baruchel 2023-11-01 18:24:06 +01:00
parent 378bb79288
commit 68869f5e11

View File

@ -4,6 +4,13 @@ Require Import List.
Import ListNotations.
(** * Various definitions of a subsequences
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
@ -20,6 +27,10 @@ Fixpoint subsequence3 {X: Type} (l s : list X) : Prop :=
end.
(**
Identical elementary properties of all definitions of a subsequence.
*)
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.
@ -30,8 +41,7 @@ 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. easy.
induction l. reflexivity. simpl. assumption.
split; try induction l; easy.
Qed.
@ -48,7 +58,7 @@ Proof.
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.
simpl in H0. apply nil_cons in H0. contradiction H0.
apply nil_cons in H0. contradiction H0.
apply nil_cons in H0. contradiction H0.
Qed.
@ -67,39 +77,32 @@ Theorem subsequence3_nil_cons_r {X: Type}: forall (l: list X) (a:X),
~ subsequence3 nil (a::l).
Proof.
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.
destruct x; apply nil_cons in H; contradiction H.
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.
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. simpl. apply eq_S. assumption.
simpl. assumption.
intros l s a. intro H. destruct H. destruct H. exists (false::x).
split; try apply eq_S; assumption.
Qed.
Theorem subsequence3_cons_l {X: Type} : forall (l s: list X) (a: X),
subsequence3 l s -> subsequence3 (a::l) s.
Proof.
intros l s a. intro H.
destruct s. apply subsequence3_nil_r.
destruct H. destruct H. destruct H.
exists (a::x0). exists x1. rewrite H.
split. reflexivity. assumption.
intros l s a. intro H. destruct s. apply subsequence3_nil_r.
destruct H. destruct H. destruct H. exists (a::x0). exists x1. rewrite H.
split; easy.
Qed.
@ -109,7 +112,7 @@ 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.
rewrite <- app_assoc. apply app_inv_head_iff. reflexivity.
Qed.
@ -121,9 +124,8 @@ Proof.
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.
simpl in H0. apply subsequence2_cons_l. apply IHl with (a := a0).
exists (x). split. inversion H.
reflexivity. assumption.
apply subsequence2_cons_l. apply IHl with (a := a0).
exists x. split; inversion H; easy.
Qed.
@ -149,10 +151,9 @@ Proof.
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 (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.
@ -162,13 +163,12 @@ 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. rewrite H2. reflexivity.
inversion H0. reflexivity. simpl in H0. inversion H.
assert (subsequence2 l (a::s)). exists x. split; assumption.
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.
exists (true :: x). split. apply eq_S. assumption. rewrite H0. reflexivity.
Qed.
@ -182,38 +182,14 @@ Proof.
destruct H0. destruct H0. destruct H0.
exists (x1 ++ (a::x3)). exists x4.
inversion H. rewrite H0. rewrite <- app_assoc.
rewrite app_comm_cons. split. reflexivity. assumption.
exists nil. exists l. split. reflexivity. assumption.
rewrite app_comm_cons. split; easy.
exists nil. exists l. split; easy.
Qed.
(*
assert (forall (l s: list Type) t,
s = map snd (filter fst (combine t l))
-> length t = length l
-> count_occ Bool.bool_dec t true = length s).
intros l s t.
generalize l s. induction t. intros l0 s0. intros J K.
simpl in J. rewrite J. reflexivity.
intros l0 s0. intros J K.
destruct a. destruct s0. destruct l0.
apply Nat.neq_succ_0 in K. contradiction K.
apply nil_cons in J. contradiction J. simpl. apply eq_S.
destruct l0.
apply Nat.neq_succ_0 in K. contradiction K.
apply IHt with (l := l0). inversion J. rewrite <- H1.
reflexivity. inversion K. reflexivity.
simpl. destruct l0.
apply Nat.neq_succ_0 in K. contradiction K.
apply IHt with (l := l0). inversion J. simpl.
reflexivity. inversion K. reflexivity.
*)
(**
Decidability and equivalence of all definitions of a subsequence.
*)
Theorem subsequence2_dec {X: Type}:
(forall x y : X, {x = y} + {x <> y})
@ -223,8 +199,7 @@ Proof.
intro l. induction l; intro s. destruct s. left. apply subsequence2_nil_r.
right. apply subsequence2_nil_cons_r.
assert({subsequence2 l s} + {~ subsequence2 l s}). apply IHl.
destruct H0.
assert({subsequence2 l s} + {~ subsequence2 l s}). apply IHl. destruct H0.
rewrite <- subsequence2_cons_eq with (a := a) in s0.
apply subsequence2_cons_r in s0. left. assumption.
@ -240,8 +215,8 @@ Proof.
destruct b.
inversion H1. rewrite H3 in n0. contradiction n0. reflexivity.
assert (subsequence2 l (x::s)). exists x0. split.
inversion H0. reflexivity. assumption. apply n in H2. contradiction H2.
assert (subsequence2 l (x::s)). exists x0. split; inversion H0; easy.
apply n in H2. contradiction H2.
Qed.
@ -336,7 +311,6 @@ Proof.
intro s. destruct s. split; intro H. apply subsequence3_nil_r.
apply subsequence_nil_r.
assert ({a=x} + {a<>x}). apply I. destruct H.
rewrite e. rewrite subsequence3_cons_eq. rewrite <- IHl.
rewrite subsequence_cons_eq. split; intro; assumption.
@ -358,6 +332,10 @@ Proof.
Qed.
(**
Various general properties of a subsequence.
*)
Theorem subsequence2_app {X: Type} :
forall l1 s1 l2 s2 : list X,
subsequence2 l1 s1 -> subsequence2 l2 s2 -> subsequence2 (l1++l2) (s1++s2).
@ -374,7 +352,7 @@ Proof.
intros t u v w. generalize u. induction t; intro u0; intro K.
replace u0 with (nil : list X). reflexivity.
destruct u0. reflexivity. apply O_S in K. contradiction K.
destruct u0. symmetry in K. apply O_S in K. contradiction K.
destruct u0. apply PeanoNat.Nat.neq_succ_0 in K. contradiction K.
simpl. rewrite IHt. reflexivity. inversion K. reflexivity.
rewrite J. rewrite filter_app. rewrite map_app. reflexivity.
@ -404,8 +382,7 @@ Proof.
= list_sum (map (fun z => S (length z)) v)).
intros u v. generalize u. induction v; intro u0; intro I.
apply length_zero_iff_nil in I. rewrite I. reflexivity.
destruct u0.
symmetry in I. apply PeanoNat.Nat.neq_succ_0 in I. contradiction I.
destruct u0. apply O_S in I. contradiction I.
simpl. rewrite IHv. reflexivity. inversion I. reflexivity.
rewrite H3.
assert (forall (u: list bool) (v: list (list X)),
@ -416,7 +393,7 @@ Proof.
intros u v. generalize u.
induction v; intro u0; intro I; destruct u0. reflexivity.
apply PeanoNat.Nat.neq_succ_0 in I. contradiction I.
symmetry in I. apply PeanoNat.Nat.neq_succ_0 in I. contradiction I.
apply O_S in I. contradiction I.
simpl. rewrite IHv. rewrite repeat_length. reflexivity.
inversion I. reflexivity. rewrite H4. reflexivity.
rewrite H1. rewrite H. reflexivity. assumption.
@ -442,17 +419,13 @@ Proof.
= filter fst (combine u v)).
intros u v w. generalize u. generalize v.
induction w; intros v0 u0; intros I J.
apply length_zero_iff_nil in I. rewrite I in J. rewrite I.
symmetry in J. apply length_zero_iff_nil in J. rewrite J.
reflexivity.
apply length_zero_iff_nil in I. rewrite I. reflexivity.
destruct u0. reflexivity. destruct v0.
apply PeanoNat.Nat.neq_succ_0 in J. contradiction J.
apply PeanoNat.Nat.neq_succ_0 in J; contradiction J.
destruct b; simpl; rewrite K; rewrite IHw.
reflexivity. inversion I. reflexivity. inversion J. reflexivity.
reflexivity. inversion I. reflexivity. inversion J. reflexivity.
rewrite H4. reflexivity.
rewrite H1. rewrite H. reflexivity.
rewrite H1. reflexivity.
reflexivity. inversion I; reflexivity. inversion J; reflexivity.
reflexivity. inversion I; reflexivity. inversion J; reflexivity.
rewrite H4; try rewrite H1; try rewrite H; reflexivity.
Qed.
@ -478,3 +451,159 @@ Proof.
split; reflexivity.
apply Nat.eq_dec.
Qed.
Theorem subsequence0_eq_def_2 {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. reflexivity. 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. reflexivity. inversion I.
reflexivity. rewrite H1. rewrite <- H2. reflexivity.
inversion H. reflexivity.
Qed.
Theorem subsequence0_eq_def_3 {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. reflexivity. inversion J. rewrite <- H5. assumption.
inversion I. reflexivity. simpl in J.
assert (subsequence3 w (x0::v)). apply IHu.
inversion I. reflexivity. assumption.
apply subsequence3_cons_l. assumption.
apply I with (u := x); assumption.
Qed.
(*
destruct H. destruct H.
(* z contient la position des booléens dans x *)
pose (z := map snd (filter fst (combine x (seq 0 (length x))))).
destruct s. exists l. exists nil. rewrite app_nil_r. split; easy.
assert (0 < length z). unfold z. rewrite map_length.
assert (forall v (u: list X) (w: list nat),
length u = length v -> length u = length w
-> length (filter fst (combine v w))
= length (map snd (filter fst (combine v u)))).
intro v. induction v; intros u w; intros I J. reflexivity.
destruct w. apply length_zero_iff_nil in J. rewrite J in I.
apply O_S in I. contradiction I.
destruct u. apply O_S in J. contradiction J.
destruct a; simpl. apply eq_S. apply IHv.
inversion I. reflexivity. inversion J. reflexivity.
apply IHv.
inversion I. reflexivity. inversion J. reflexivity.
assert (length (x0::s) = length (map snd (filter fst (combine x l)))).
rewrite H0. reflexivity. rewrite <- H1 with (w := seq 0 (length x)) in H2.
rewrite <- H2. apply Nat.lt_0_succ. inversion H. reflexivity.
rewrite H. rewrite seq_length. reflexivity.
exists (firstn (hd 0 z) l).
(* z2 contient la position du true suivant *)
pose (z2 := (skipn 1 z) ++ [ length l ]).
(* z3 contient la longueur de chaque bloc true; false; false; ... *)
pose (z3 := map (fun e => (snd e) - (fst e)) (combine z z2)).
exists (map (fun e => firstn ((snd e) -1) (skipn (S (fst e)) l))
(combine z z3)).
assert (length (x0::s) = length z). unfold z. rewrite H0.
rewrite map_length. rewrite map_length. rewrite H.
assert (forall u (v: list X) (w: list nat),
length v = length w
-> length (filter fst (combine u v))
= length (filter fst (combine u w))).
intro u. induction u; intros v w; intro I. reflexivity.
destruct v. symmetry in I. apply length_zero_iff_nil in I.
rewrite I. reflexivity. destruct w. apply Nat.neq_succ_0 in I.
contradiction I. destruct a; simpl; rewrite IHu with (w := w).
inversion I; reflexivity. inversion I; reflexivity. reflexivity.
inversion I; reflexivity. rewrite H2 with (w := seq 0 (length l)).
reflexivity. rewrite seq_length. reflexivity.
unfold z3. unfold z2. split. destruct z. apply Nat.nlt_0_r in H1.
contradiction H1.
rewrite map_length. rewrite combine_length. rewrite map_length.
rewrite combine_length. rewrite app_length. rewrite Nat.add_1_r.
simpl. apply eq_S. rewrite Nat.min_id. rewrite Nat.min_id.
inversion H2. reflexivity. unfold z. rewrite H0.
assert (forall (u: list bool) (v: list X),
length u = length v
-> v =
firstn (hd 0 (map snd (filter fst (combine u (seq 0 (length u)))))) v ++
flat_map (fun e : X * list X => fst e :: snd e)
(combine (map snd (filter fst (combine u v)))
(map (fun e : nat * nat => firstn (snd e - 1) (skipn (S (fst e)) v))
(combine (map snd (filter fst (combine u (seq 0 (length u)))))
(map (fun e : nat * nat => snd e - fst e)
(combine (map snd (filter fst (combine u (seq 0 (length u)))))
(skipn 1
(map snd (filter fst (combine u (seq 0 (length u))))) ++
[length v]))))))).
intro u. induction u; intro v; intro I.
symmetry in I. apply length_zero_iff_nil in I. assumption.
destruct v. rewrite app_nil_r. rewrite firstn_nil. reflexivity.
destruct a.
replace
(map snd (filter fst (combine (true :: u) (seq 0 (length (true :: u))))))
with
*)