From 7f8adb16401bf126e7f8c61ce43d01bab3ad7374 Mon Sep 17 00:00:00 2001 From: Thomas Baruchel Date: Tue, 5 Dec 2023 23:06:31 +0100 Subject: [PATCH] Update --- src/subsequences2.v | 317 +++++++++++--------------------------------- 1 file changed, 81 insertions(+), 236 deletions(-) diff --git a/src/subsequences2.v b/src/subsequences2.v index 4f3bd14..df35813 100644 --- a/src/subsequences2.v +++ b/src/subsequences2.v @@ -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.