2023-10-25 07:22:47 -04:00
|
|
|
Require Import Nat.
|
|
|
|
Require Import PeanoNat.
|
|
|
|
Require Import List.
|
|
|
|
Import ListNotations.
|
|
|
|
|
|
|
|
|
2023-11-01 14:41:12 -04:00
|
|
|
(** * Various definitions
|
2023-11-01 13:24:06 -04:00
|
|
|
|
|
|
|
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.
|
|
|
|
*)
|
|
|
|
|
2023-10-30 11:40:11 -04:00
|
|
|
Definition subsequence {X: Type} (l s : list X) :=
|
|
|
|
exists (l1: list X) (l2 : list (list X)),
|
2023-10-25 07:22:47 -04:00
|
|
|
length s = length l2
|
|
|
|
/\ l = l1 ++ flat_map (fun e => (fst e) :: (snd e)) (combine s l2).
|
|
|
|
|
2023-10-30 11:40:11 -04:00
|
|
|
Definition subsequence2 {X: Type} (l s : list X) :=
|
2023-10-25 07:22:47 -04:00
|
|
|
exists (t: list bool),
|
|
|
|
length t = length l /\ s = map snd (filter fst (combine t l)).
|
|
|
|
|
2023-10-30 12:43:24 -04:00
|
|
|
Fixpoint subsequence3 {X: Type} (l s : list X) : Prop :=
|
|
|
|
match s with
|
|
|
|
| nil => True
|
|
|
|
| hd::tl => exists l1 l2, l = l1 ++ (hd::l2) /\ subsequence3 l2 tl
|
|
|
|
end.
|
|
|
|
|
2023-10-29 16:10:19 -04:00
|
|
|
|
2023-11-01 14:41:12 -04:00
|
|
|
(** * Elementary properties
|
2023-11-01 13:24:06 -04:00
|
|
|
*)
|
|
|
|
|
2023-10-30 12:07:08 -04:00
|
|
|
Theorem subsequence_nil_r {X: Type}: forall (l : list X), subsequence l nil.
|
2023-10-29 16:10:19 -04:00
|
|
|
Proof.
|
2023-10-30 03:18:20 -04:00
|
|
|
intro l. exists l. exists nil. rewrite app_nil_r. split; easy.
|
2023-10-29 16:10:19 -04:00
|
|
|
Qed.
|
|
|
|
|
|
|
|
|
2023-10-30 14:16:04 -04:00
|
|
|
Theorem subsequence2_nil_r {X: Type} : forall (l : list X), subsequence2 l nil.
|
|
|
|
Proof.
|
|
|
|
intro l.
|
|
|
|
exists (repeat false (length l)). rewrite repeat_length.
|
2023-11-01 13:24:06 -04:00
|
|
|
split; try induction l; easy.
|
2023-10-30 14:16:04 -04:00
|
|
|
Qed.
|
|
|
|
|
|
|
|
|
|
|
|
Theorem subsequence3_nil_r {X: Type} : forall (l : list X), subsequence3 l nil.
|
|
|
|
Proof.
|
|
|
|
intro l. reflexivity.
|
|
|
|
Qed.
|
|
|
|
|
|
|
|
|
2023-10-30 12:07:08 -04:00
|
|
|
Theorem subsequence_nil_cons_r {X: Type}: forall (l: list X) (a:X),
|
2023-10-29 16:10:19 -04:00
|
|
|
~ subsequence nil (a::l).
|
|
|
|
Proof.
|
2023-10-31 04:19:23 -04:00
|
|
|
intros l a. intro H.
|
2023-10-29 16:10:19 -04:00
|
|
|
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.
|
2023-11-01 13:24:06 -04:00
|
|
|
apply nil_cons in H0. contradiction H0.
|
2023-10-29 16:10:19 -04:00
|
|
|
apply nil_cons in H0. contradiction H0.
|
|
|
|
Qed.
|
|
|
|
|
|
|
|
|
2023-10-30 12:07:08 -04:00
|
|
|
Theorem subsequence2_nil_cons_r {X: Type}: forall (l: list X) (a:X),
|
2023-10-29 16:10:19 -04:00
|
|
|
~ subsequence2 nil (a::l).
|
|
|
|
Proof.
|
2023-10-31 04:19:23 -04:00
|
|
|
intros l a. intro H. destruct H.
|
2023-10-29 16:10:19 -04:00
|
|
|
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.
|
|
|
|
|
|
|
|
|
2023-10-30 12:43:24 -04:00
|
|
|
Theorem subsequence3_nil_cons_r {X: Type}: forall (l: list X) (a:X),
|
|
|
|
~ subsequence3 nil (a::l).
|
|
|
|
Proof.
|
2023-10-31 04:19:23 -04:00
|
|
|
intros l a. intro H. destruct H. destruct H. destruct H.
|
2023-11-01 13:24:06 -04:00
|
|
|
destruct x; apply nil_cons in H; contradiction H.
|
2023-10-30 12:43:24 -04:00
|
|
|
Qed.
|
|
|
|
|
|
|
|
|
2023-10-30 12:07:08 -04:00
|
|
|
Theorem subsequence_cons_l {X: Type}: forall (l s: list X) (a: X),
|
2023-10-30 05:57:47 -04:00
|
|
|
subsequence l s -> subsequence (a::l) s.
|
|
|
|
Proof.
|
2023-11-01 13:24:06 -04:00
|
|
|
intros l s a. intro H. destruct H. destruct H. destruct H.
|
|
|
|
exists (a::x). exists x0. split. assumption. rewrite H0. reflexivity.
|
2023-10-30 05:57:47 -04:00
|
|
|
Qed.
|
|
|
|
|
|
|
|
|
2023-10-30 12:07:08 -04:00
|
|
|
Theorem subsequence2_cons_l {X: Type} : forall (l s: list X) (a: X),
|
2023-10-30 01:50:55 -04:00
|
|
|
subsequence2 l s -> subsequence2 (a::l) s.
|
|
|
|
Proof.
|
2023-11-01 13:24:06 -04:00
|
|
|
intros l s a. intro H. destruct H. destruct H. exists (false::x).
|
|
|
|
split; try apply eq_S; assumption.
|
2023-10-30 01:50:55 -04:00
|
|
|
Qed.
|
|
|
|
|
|
|
|
|
2023-10-30 12:43:24 -04:00
|
|
|
Theorem subsequence3_cons_l {X: Type} : forall (l s: list X) (a: X),
|
|
|
|
subsequence3 l s -> subsequence3 (a::l) s.
|
|
|
|
Proof.
|
2023-11-01 13:24:06 -04:00
|
|
|
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.
|
2023-10-30 12:43:24 -04:00
|
|
|
Qed.
|
|
|
|
|
|
|
|
|
2023-10-30 12:07:08 -04:00
|
|
|
Theorem subsequence_cons_r {X: Type} : forall (l s: list X) (a: X),
|
2023-10-30 05:57:47 -04:00
|
|
|
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.
|
2023-11-01 13:24:06 -04:00
|
|
|
rewrite <- app_assoc. apply app_inv_head_iff. reflexivity.
|
2023-10-30 05:57:47 -04:00
|
|
|
Qed.
|
|
|
|
|
|
|
|
|
2023-10-30 12:07:08 -04:00
|
|
|
Theorem subsequence2_cons_r {X: Type} : forall (l s: list X) (a: X),
|
2023-10-30 01:50:55 -04:00
|
|
|
subsequence2 l (a::s) -> subsequence2 l s.
|
|
|
|
Proof.
|
|
|
|
intro l. induction l. intros. apply subsequence2_nil_cons_r in H.
|
2023-10-30 03:18:20 -04:00
|
|
|
contradiction H. intros s a0 . intro H. destruct H. destruct H. destruct x.
|
2023-10-30 01:50:55 -04:00
|
|
|
symmetry in H0. apply nil_cons in H0. contradiction H0.
|
|
|
|
destruct b. simpl in H0. inversion H0.
|
2023-10-30 03:18:20 -04:00
|
|
|
exists (false::x). split; try rewrite <- H; reflexivity.
|
2023-11-01 13:24:06 -04:00
|
|
|
apply subsequence2_cons_l. apply IHl with (a := a0).
|
|
|
|
exists x. split; inversion H; easy.
|
2023-10-30 01:50:55 -04:00
|
|
|
Qed.
|
|
|
|
|
|
|
|
|
2023-10-30 12:43:24 -04:00
|
|
|
Theorem subsequence3_cons_r {X: Type} : forall (l s: list X) (a: X),
|
|
|
|
subsequence3 l (a::s) -> subsequence3 l s.
|
|
|
|
Proof.
|
|
|
|
intros l s a. intro H. simpl in H. destruct H. destruct H.
|
|
|
|
destruct s. apply subsequence3_nil_r. destruct H. simpl in H0.
|
|
|
|
destruct H0. destruct H0. destruct H0.
|
|
|
|
exists (x ++ a::x2). exists x3.
|
|
|
|
rewrite H. rewrite H0. split. rewrite <- app_assoc.
|
|
|
|
rewrite app_comm_cons. reflexivity. assumption.
|
|
|
|
Qed.
|
|
|
|
|
|
|
|
|
2023-10-30 12:07:08 -04:00
|
|
|
Theorem subsequence_cons_eq {X: Type} : forall (l1 l2: list X) (a: X),
|
2023-10-30 07:33:00 -04:00
|
|
|
subsequence (a::l1) (a::l2) <-> subsequence l1 l2.
|
|
|
|
Proof.
|
2023-10-31 04:07:36 -04:00
|
|
|
intros l s a. split; intro H; destruct H; destruct H; destruct H.
|
2023-10-30 07:33:00 -04:00
|
|
|
destruct x. destruct x0.
|
|
|
|
apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
|
2023-10-31 04:19:23 -04:00
|
|
|
inversion H0. exists l0. exists x0.
|
2023-10-30 11:40:11 -04:00
|
|
|
inversion H. rewrite H3. split; reflexivity.
|
2023-10-31 04:07:36 -04:00
|
|
|
destruct x0.
|
2023-10-30 07:33:00 -04:00
|
|
|
apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
|
2023-11-01 13:24:06 -04:00
|
|
|
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.
|
2023-10-31 04:07:36 -04:00
|
|
|
exists nil. exists (x::x0). simpl.
|
|
|
|
split; [ rewrite H | rewrite H0 ]; reflexivity.
|
2023-10-30 07:33:00 -04:00
|
|
|
Qed.
|
|
|
|
|
|
|
|
|
2023-10-30 12:07:08 -04:00
|
|
|
Theorem subsequence2_cons_eq {X: Type}: forall (l1 l2: list X) (a: X),
|
2023-10-29 16:10:19 -04:00
|
|
|
subsequence2 (a::l1) (a::l2) <-> subsequence2 l1 l2.
|
|
|
|
Proof.
|
2023-10-31 04:03:37 -04:00
|
|
|
intros l s a. split; intro H; destruct H; destruct H.
|
2023-11-01 13:24:06 -04:00
|
|
|
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.
|
2023-10-30 02:48:09 -04:00
|
|
|
apply subsequence2_cons_r with (a := a). assumption.
|
2023-11-01 13:24:06 -04:00
|
|
|
exists (true :: x). split. apply eq_S. assumption. rewrite H0. reflexivity.
|
2023-10-30 02:51:59 -04:00
|
|
|
Qed.
|
2023-10-30 12:43:24 -04:00
|
|
|
|
|
|
|
|
|
|
|
Theorem subsequence3_cons_eq {X: Type} : forall (l1 l2: list X) (a: X),
|
|
|
|
subsequence3 (a::l1) (a::l2) <-> subsequence3 l1 l2.
|
|
|
|
Proof.
|
2023-10-31 04:07:36 -04:00
|
|
|
intros l s a. split; intro H.
|
2023-10-30 12:43:24 -04:00
|
|
|
destruct H. destruct H. destruct H.
|
|
|
|
destruct x. inversion H. assumption.
|
|
|
|
destruct s. apply subsequence3_nil_r.
|
|
|
|
destruct H0. destruct H0. destruct H0.
|
|
|
|
exists (x1 ++ (a::x3)). exists x4.
|
|
|
|
inversion H. rewrite H0. rewrite <- app_assoc.
|
2023-11-01 13:24:06 -04:00
|
|
|
rewrite app_comm_cons. split; easy.
|
|
|
|
exists nil. exists l. split; easy.
|
2023-10-30 12:43:24 -04:00
|
|
|
Qed.
|
2023-10-30 02:48:09 -04:00
|
|
|
|
|
|
|
|
2023-11-01 14:41:12 -04:00
|
|
|
(** * 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
|
2023-11-01 13:45:52 -04:00
|
|
|
*)
|
|
|
|
|
|
|
|
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.
|
|
|
|
|
2023-11-01 15:55:55 -04:00
|
|
|
rewrite H1; inversion H; reflexivity. rewrite H0.
|
2023-11-01 13:45:52 -04:00
|
|
|
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.
|
2023-11-01 15:55:55 -04:00
|
|
|
simpl. rewrite H1. rewrite <- IHv; inversion I; reflexivity.
|
|
|
|
rewrite H1. rewrite <- H2; inversion H; reflexivity.
|
2023-11-01 13:45:52 -04:00
|
|
|
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.
|
2023-11-01 16:06:13 -04:00
|
|
|
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.
|
2023-11-01 13:45:52 -04:00
|
|
|
apply I with (u := x); assumption.
|
|
|
|
Qed.
|
|
|
|
|
|
|
|
|
|
|
|
Theorem subsequence_eq_def_3 {X: Type} :
|
|
|
|
forall l s : list X, subsequence3 l s -> subsequence l s.
|
|
|
|
Proof.
|
|
|
|
intros l s. generalize l. induction s; intro l0; intro H.
|
|
|
|
apply subsequence_nil_r. destruct H. destruct H. destruct H.
|
|
|
|
apply IHs in H0. destruct H0. destruct H0. destruct H0.
|
|
|
|
exists x. exists (x1:: x2). split. simpl. rewrite H0.
|
|
|
|
reflexivity. rewrite H. rewrite H1. reflexivity.
|
|
|
|
Qed.
|
|
|
|
|
|
|
|
|
2023-11-01 14:41:12 -04:00
|
|
|
(** * Decidability of all definitions
|
2023-11-01 13:24:06 -04:00
|
|
|
*)
|
2023-10-29 16:10:19 -04:00
|
|
|
|
2023-10-30 12:07:08 -04:00
|
|
|
Theorem subsequence2_dec {X: Type}:
|
|
|
|
(forall x y : X, {x = y} + {x <> y})
|
|
|
|
-> forall (l s : list X), { subsequence2 l s } + { ~ subsequence2 l s }.
|
2023-10-29 16:10:19 -04:00
|
|
|
Proof.
|
|
|
|
intro H.
|
2023-10-31 04:19:23 -04:00
|
|
|
intro l. induction l; intro s. destruct s. left. apply subsequence2_nil_r.
|
2023-10-29 16:10:19 -04:00
|
|
|
right. apply subsequence2_nil_cons_r.
|
|
|
|
|
2023-11-01 13:24:06 -04:00
|
|
|
assert({subsequence2 l s} + {~ subsequence2 l s}). apply IHl. destruct H0.
|
2023-10-29 16:10:19 -04:00
|
|
|
|
2023-10-30 05:30:22 -04:00
|
|
|
rewrite <- subsequence2_cons_eq with (a := a) in s0.
|
2023-11-01 16:42:31 -04:00
|
|
|
apply subsequence2_cons_r in s0. left; assumption.
|
2023-10-29 16:10:19 -04:00
|
|
|
|
2023-10-30 05:30:22 -04:00
|
|
|
destruct s. left. apply subsequence2_nil_r.
|
2023-10-30 12:07:08 -04:00
|
|
|
assert ({x=a}+{x<>a}). apply H. destruct H0. rewrite e.
|
2023-10-31 04:19:23 -04:00
|
|
|
destruct IHl with (s := s); [ left | right ];
|
|
|
|
rewrite subsequence2_cons_eq; assumption.
|
2023-10-30 05:30:22 -04:00
|
|
|
|
2023-10-31 04:19:23 -04:00
|
|
|
right. intro I.
|
2023-10-30 12:07:08 -04:00
|
|
|
destruct I. destruct H0. destruct x0.
|
2023-10-30 05:30:22 -04:00
|
|
|
symmetry in H1. apply nil_cons in H1. contradiction H1.
|
|
|
|
destruct b.
|
2023-11-01 16:40:10 -04:00
|
|
|
inversion H1. rewrite H3 in n0. easy.
|
|
|
|
apply n. exists x0; split; inversion H0; easy.
|
2023-10-30 05:30:22 -04:00
|
|
|
Qed.
|
2023-10-29 16:10:19 -04:00
|
|
|
|
|
|
|
|
2023-10-30 14:16:04 -04:00
|
|
|
Theorem subsequence3_dec {X: Type}:
|
|
|
|
(forall x y : X, {x = y} + {x <> y})
|
|
|
|
-> forall (l s : list X), { subsequence3 l s } + { ~ subsequence3 l s }.
|
|
|
|
Proof.
|
2023-11-01 13:45:52 -04:00
|
|
|
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.
|
2023-11-01 14:13:41 -04:00
|
|
|
right. intro I.
|
2023-11-01 13:45:52 -04:00
|
|
|
apply subsequence_eq_def_3 in I.
|
|
|
|
apply subsequence_eq_def_1 in I.
|
|
|
|
apply n in I. contradiction I.
|
2023-10-30 07:57:00 -04:00
|
|
|
Qed.
|
2023-10-25 07:22:47 -04:00
|
|
|
|
|
|
|
|
2023-10-31 04:03:37 -04:00
|
|
|
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.
|
2023-11-01 13:45:52 -04:00
|
|
|
assert ({ subsequence3 l s } + { ~ subsequence3 l s }).
|
|
|
|
apply subsequence3_dec. assumption. destruct H0.
|
|
|
|
apply subsequence_eq_def_3 in s0. left. assumption.
|
2023-11-01 14:13:41 -04:00
|
|
|
right. intro I.
|
2023-11-01 13:45:52 -04:00
|
|
|
apply subsequence_eq_def_1 in I.
|
|
|
|
apply subsequence_eq_def_2 in I.
|
|
|
|
apply n in I. contradiction I.
|
2023-10-30 14:34:21 -04:00
|
|
|
Qed.
|
2023-10-30 14:16:04 -04:00
|
|
|
|
|
|
|
|
2023-11-01 14:41:12 -04:00
|
|
|
(** * Various general properties
|
2023-11-01 13:24:06 -04:00
|
|
|
*)
|
|
|
|
|
2023-11-01 14:09:31 -04:00
|
|
|
Theorem subsequence_app {X: Type} :
|
2023-10-31 09:43:53 -04:00
|
|
|
forall l1 s1 l2 s2 : list X,
|
2023-11-01 14:09:31 -04:00
|
|
|
subsequence l1 s1 -> subsequence l2 s2 -> subsequence (l1++l2) (s1++s2).
|
2023-10-31 09:43:53 -04:00
|
|
|
Proof.
|
|
|
|
intros l1 s1 l2 s2. intros H I.
|
2023-11-01 14:09:31 -04:00
|
|
|
apply subsequence_eq_def_3. apply subsequence_eq_def_2.
|
|
|
|
apply subsequence_eq_def_1 in H.
|
|
|
|
apply subsequence_eq_def_1 in I.
|
2023-10-31 09:43:53 -04:00
|
|
|
destruct H. destruct I. exists (x++x0). destruct H. destruct H0.
|
|
|
|
split. rewrite app_length. rewrite app_length.
|
|
|
|
rewrite H. rewrite H0. reflexivity.
|
|
|
|
rewrite H1. rewrite H2.
|
|
|
|
|
|
|
|
assert (J: forall (t : list bool) (u : list X) (v: list bool) (w : list X),
|
|
|
|
length t = length u
|
|
|
|
-> combine (t++v) (u++w) = (combine t u) ++ (combine v w)).
|
|
|
|
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.
|
2023-11-01 13:24:06 -04:00
|
|
|
destruct u0. apply PeanoNat.Nat.neq_succ_0 in K. contradiction K.
|
2023-10-31 09:43:53 -04:00
|
|
|
simpl. rewrite IHt. reflexivity. inversion K. reflexivity.
|
|
|
|
|
|
|
|
rewrite J. rewrite filter_app. rewrite map_app. reflexivity.
|
|
|
|
assumption.
|
|
|
|
Qed.
|
|
|
|
|
|
|
|
|
2023-10-31 14:31:38 -04:00
|
|
|
Theorem subsequence_trans {X: Type} :
|
|
|
|
forall (l1 l2 l3: list X),
|
2023-11-01 14:09:31 -04:00
|
|
|
subsequence l1 l2 -> subsequence l2 l3 -> subsequence l1 l3.
|
2023-10-31 14:31:38 -04:00
|
|
|
Proof.
|
|
|
|
intros l1 l2 l3. intros H I.
|
2023-11-01 14:09:31 -04:00
|
|
|
apply subsequence_eq_def_3. apply subsequence_eq_def_2.
|
|
|
|
apply subsequence_eq_def_1 in I.
|
2023-10-31 14:31:38 -04:00
|
|
|
destruct H. destruct H. destruct H. destruct I. destruct H1.
|
|
|
|
exists (
|
|
|
|
(repeat false (length x)) ++
|
|
|
|
(flat_map (fun e => (fst e) :: (repeat false (length (snd e))))
|
|
|
|
(combine x1 x0))).
|
|
|
|
split.
|
|
|
|
|
|
|
|
rewrite app_length. rewrite repeat_length.
|
|
|
|
rewrite H0. rewrite app_length. rewrite Nat.add_cancel_l.
|
|
|
|
rewrite flat_map_length. rewrite flat_map_length.
|
|
|
|
assert (forall (u: list X) (v: list (list X)),
|
|
|
|
length u = length v
|
|
|
|
-> list_sum (map (fun z => length (fst z :: snd z))
|
|
|
|
(combine u v))
|
|
|
|
= 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.
|
2023-11-01 13:24:06 -04:00
|
|
|
destruct u0. apply O_S in I. contradiction I.
|
2023-10-31 14:31:38 -04:00
|
|
|
simpl. rewrite IHv. reflexivity. inversion I. reflexivity.
|
|
|
|
rewrite H3.
|
|
|
|
assert (forall (u: list bool) (v: list (list X)),
|
|
|
|
length u = length v
|
|
|
|
-> list_sum (map (fun z => length (fst z :: repeat false (length (snd z))))
|
|
|
|
(combine u v))
|
|
|
|
= list_sum (map (fun z => S (length z)) v)).
|
|
|
|
intros u v. generalize u.
|
|
|
|
induction v; intro u0; intro I; destruct u0. reflexivity.
|
|
|
|
apply PeanoNat.Nat.neq_succ_0 in I. contradiction I.
|
2023-11-01 13:24:06 -04:00
|
|
|
apply O_S in I. contradiction I.
|
2023-10-31 14:31:38 -04:00
|
|
|
simpl. rewrite IHv. rewrite repeat_length. reflexivity.
|
|
|
|
inversion I. reflexivity. rewrite H4. reflexivity.
|
|
|
|
rewrite H1. rewrite H. reflexivity. assumption.
|
|
|
|
|
|
|
|
assert (K: forall (w v: list X) u,
|
|
|
|
filter fst (combine ((repeat false (length w)) ++ u)
|
|
|
|
(w ++ v)) = filter fst (combine u v)).
|
|
|
|
intro w0. induction w0. reflexivity. apply IHw0.
|
|
|
|
rewrite H2. rewrite H0.
|
|
|
|
assert (forall (u v: list X) (w: list bool),
|
|
|
|
map snd (filter fst (combine ((repeat false (length u)) ++ w) (u ++ v)))
|
|
|
|
= map snd (filter fst (combine w v))).
|
|
|
|
intro u. induction u; intros v w. reflexivity.
|
|
|
|
apply IHu. rewrite H3.
|
|
|
|
assert (forall (u: list bool) (v: list X) (w: list (list X)),
|
|
|
|
length u = length w
|
|
|
|
-> length u = length v
|
|
|
|
-> filter fst (combine
|
|
|
|
(flat_map
|
|
|
|
(fun e => fst e:: (repeat false (length (snd e))))
|
|
|
|
(combine u w))
|
|
|
|
(flat_map (fun e => fst e :: snd e) (combine v w)))
|
|
|
|
= filter fst (combine u v)).
|
|
|
|
intros u v w. generalize u. generalize v.
|
|
|
|
induction w; intros v0 u0; intros I J.
|
2023-11-01 13:24:06 -04:00
|
|
|
apply length_zero_iff_nil in I. rewrite I. reflexivity.
|
2023-10-31 14:31:38 -04:00
|
|
|
destruct u0. reflexivity. destruct v0.
|
2023-11-01 13:24:06 -04:00
|
|
|
apply PeanoNat.Nat.neq_succ_0 in J; contradiction J.
|
2023-11-01 16:08:36 -04:00
|
|
|
destruct b; simpl; rewrite K; rewrite IHw;
|
|
|
|
inversion I; inversion J; reflexivity.
|
2023-11-01 13:24:06 -04:00
|
|
|
rewrite H4; try rewrite H1; try rewrite H; reflexivity.
|
2023-10-31 14:31:38 -04:00
|
|
|
Qed.
|
2023-11-01 17:51:16 -04:00
|
|
|
|
|
|
|
|
|
|
|
Lemma subsequence_length {X: Type} :
|
|
|
|
forall (u v: list X), subsequence u v -> length v <= length u.
|
|
|
|
Proof.
|
|
|
|
intros u v. generalize u. induction v; intro u0; intro H. apply Nat.le_0_l.
|
|
|
|
apply subsequence_eq_def_1 in H. apply subsequence_eq_def_2 in H.
|
|
|
|
destruct H. destruct H. destruct H. apply subsequence_eq_def_3 in H0.
|
|
|
|
apply IHv in H0. simpl. apply Nat.le_succ_l. rewrite H.
|
|
|
|
rewrite app_length. apply Nat.lt_lt_add_l.
|
|
|
|
rewrite <- Nat.le_succ_l. simpl. rewrite <- Nat.succ_le_mono.
|
|
|
|
assumption.
|
|
|
|
Qed.
|
|
|
|
|
|
|
|
|
|
|
|
Theorem subsequence_id {X: Type} :
|
|
|
|
forall (u v: list X),
|
|
|
|
subsequence u v -> subsequence v u -> u = v.
|
|
|
|
Proof.
|
|
|
|
intro u. induction u; intro v; intros H I;
|
|
|
|
apply subsequence_eq_def_1 in H; apply subsequence_eq_def_1 in I.
|
|
|
|
|
|
|
|
destruct v. reflexivity.
|
|
|
|
apply subsequence2_nil_cons_r in H. contradiction H.
|
|
|
|
destruct v. apply subsequence2_nil_cons_r in I. contradiction I.
|
|
|
|
|
|
|
|
destruct H. destruct H. destruct I. destruct H1.
|
|
|
|
destruct x0. apply O_S in H. contradiction H.
|
|
|
|
destruct x1. apply O_S in H1. contradiction H1.
|
|
|
|
destruct b; destruct b0.
|
|
|
|
|
|
|
|
assert (subsequence2 u v). exists x0.
|
|
|
|
split; inversion H; inversion H0; reflexivity.
|
|
|
|
assert (subsequence2 v u). exists x1.
|
|
|
|
split; inversion H1; inversion H2; reflexivity.
|
|
|
|
apply subsequence_eq_def_2 in H3; apply subsequence_eq_def_3 in H3.
|
|
|
|
apply subsequence_eq_def_2 in H4; apply subsequence_eq_def_3 in H4.
|
|
|
|
apply IHu in H4. rewrite H4. inversion H0. reflexivity. assumption.
|
|
|
|
|
|
|
|
assert (subsequence2 u v). exists x0.
|
|
|
|
split; inversion H; inversion H0; reflexivity.
|
|
|
|
assert (subsequence2 v (a::u)). exists x1.
|
|
|
|
split; inversion H1; inversion H2; reflexivity.
|
|
|
|
assert (subsequence u (a::u)). apply subsequence_trans with (l2 := v);
|
|
|
|
apply subsequence_eq_def_3; apply subsequence_eq_def_2; assumption.
|
|
|
|
apply subsequence_length in H5. apply Nat.nle_succ_diag_l in H5.
|
|
|
|
contradiction H5.
|
|
|
|
|
|
|
|
assert (subsequence2 u (x::v)). exists x0.
|
|
|
|
split; inversion H; inversion H0; reflexivity.
|
|
|
|
assert (subsequence2 v u). exists x1.
|
|
|
|
split; inversion H1; inversion H2; reflexivity.
|
|
|
|
assert (subsequence v (x::v)). apply subsequence_trans with (l2 := u);
|
|
|
|
apply subsequence_eq_def_3; apply subsequence_eq_def_2; assumption.
|
|
|
|
apply subsequence_length in H5. apply Nat.nle_succ_diag_l in H5.
|
|
|
|
contradiction H5.
|
|
|
|
|
|
|
|
assert (subsequence2 u (x::v)). exists x0.
|
|
|
|
split; inversion H; inversion H0; reflexivity.
|
|
|
|
assert (subsequence2 v (a::u)). exists x1.
|
|
|
|
split; inversion H1; inversion H2; reflexivity.
|
|
|
|
apply subsequence2_cons_r in H3. apply subsequence2_cons_r in H4.
|
|
|
|
apply subsequence_eq_def_2 in H3. apply subsequence_eq_def_2 in H4.
|
|
|
|
apply subsequence_eq_def_3 in H3. apply subsequence_eq_def_3 in H4.
|
|
|
|
apply IHu in H4. rewrite H4 in H0. rewrite H4 in H.
|
|
|
|
simpl in H0. assert (subsequence2 v (x::v)). exists x0.
|
|
|
|
split. inversion H. reflexivity. assumption.
|
|
|
|
apply subsequence_eq_def_2 in H5. apply subsequence_eq_def_3 in H5.
|
|
|
|
apply subsequence_length in H5. apply Nat.nle_succ_diag_l in H5.
|
|
|
|
contradiction H5. assumption.
|
|
|
|
Qed.
|
|
|
|
|
|
|
|
|
|
|
|
|
2023-10-31 14:31:38 -04:00
|
|
|
|
|
|
|
|
2023-11-01 14:41:12 -04:00
|
|
|
(** * Tests
|
|
|
|
*)
|
2023-10-31 09:43:53 -04:00
|
|
|
|
2023-10-25 07:22:47 -04:00
|
|
|
Example test1: subsequence [1;2;3;4;5] [1;3;5].
|
|
|
|
Proof.
|
|
|
|
unfold subsequence.
|
|
|
|
exists [].
|
|
|
|
exists [[2];[4];[]]. simpl. easy.
|
|
|
|
Qed.
|
|
|
|
|
|
|
|
Example test2: subsequence [1;2;3;4;5] [2;4].
|
|
|
|
Proof.
|
|
|
|
unfold subsequence.
|
|
|
|
exists [1].
|
|
|
|
exists [[3];[5]]. simpl. easy.
|
|
|
|
Qed.
|
2023-10-30 12:07:08 -04:00
|
|
|
|
|
|
|
Example test3: subsequence [1;2;3;4;5] [1;3;5].
|
|
|
|
Proof.
|
2023-11-01 13:45:52 -04:00
|
|
|
apply subsequence_eq_def_3. apply subsequence_eq_def_2.
|
2023-10-30 12:11:08 -04:00
|
|
|
exists [true; false; true; false; true].
|
|
|
|
split; reflexivity.
|
2023-11-01 13:31:41 -04:00
|
|
|
Qed.
|