From 68869f5e114ae0bdf36badee2f2abf86457d7a21 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Wed, 1 Nov 2023 18:24:06 +0100 Subject: [PATCH] Update --- src/subsequences.v | 287 ++++++++++++++++++++++++++++++++------------- 1 file changed, 208 insertions(+), 79 deletions(-) diff --git a/src/subsequences.v b/src/subsequences.v index 104db7c..02c0970 100644 --- a/src/subsequences.v +++ b/src/subsequences.v @@ -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 + *)