320 lines
9.7 KiB
Coq
320 lines
9.7 KiB
Coq
Require Import Nat.
|
|
Require Import PeanoNat.
|
|
Require Import List.
|
|
Import ListNotations.
|
|
|
|
Require Import Lia.
|
|
|
|
|
|
Definition subsequence (l s : list Type) :=
|
|
exists (l1: list Type) (l2 : list (list Type)),
|
|
length s = length l2
|
|
/\ l = l1 ++ flat_map (fun e => (fst e) :: (snd e)) (combine s l2).
|
|
|
|
Definition subsequence2 (l s : list Type) :=
|
|
exists (t: list bool),
|
|
length t = length l /\ s = map snd (filter fst (combine t l)).
|
|
|
|
(*
|
|
TODO: problème, les éléments de l ne sont pas uniques ; or
|
|
il doit pouvoir y avoir des différences dans la décision de les
|
|
prendre ou non
|
|
Definition subsequence3 (l s : list Type) :=
|
|
exists f, s = fst (partition f l).
|
|
*)
|
|
|
|
Theorem subsequence_nil_r : forall (l : list Type), subsequence l nil.
|
|
Proof.
|
|
intro l. exists l. exists nil. rewrite app_nil_r. split; easy.
|
|
Qed.
|
|
|
|
|
|
Theorem subsequence_nil_cons_r : forall (l: list Type) (a:Type),
|
|
~ subsequence nil (a::l).
|
|
Proof.
|
|
intros l a. unfold not. 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.
|
|
simpl in H0. apply nil_cons in H0. contradiction H0.
|
|
apply nil_cons in H0. contradiction H0.
|
|
Qed.
|
|
|
|
|
|
Theorem subsequence2_nil_r : forall (l : list Type), subsequence2 l nil.
|
|
Proof.
|
|
intro l.
|
|
exists (repeat false (length l)). rewrite repeat_length.
|
|
split. easy.
|
|
induction l. reflexivity. simpl. assumption.
|
|
Qed.
|
|
|
|
|
|
Theorem subsequence2_nil_cons_r : forall (l: list Type) (a:Type),
|
|
~ subsequence2 nil (a::l).
|
|
Proof.
|
|
intros l a. unfold not. 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 subsequence2_cons_l : forall (l s: list Type) (a: Type),
|
|
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.
|
|
Qed.
|
|
|
|
|
|
Theorem subsequence2_cons_r : forall (l s: list Type) (a: Type),
|
|
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.
|
|
simpl in H0. apply subsequence2_cons_l. apply IHl with (a := a0).
|
|
unfold subsequence2. exists (x). split. inversion H.
|
|
reflexivity. assumption.
|
|
Qed.
|
|
|
|
|
|
Theorem subsequence2_cons_eq : forall (l1 l2: list Type) (a: Type),
|
|
subsequence2 (a::l1) (a::l2) <-> subsequence2 l1 l2.
|
|
Proof.
|
|
intros l s a. split. intro H. unfold subsequence2 in H.
|
|
destruct H. destruct H. destruct x. inversion H0.
|
|
destruct b. exists (x). split. inversion H. reflexivity. simpl in H0.
|
|
inversion H0. reflexivity. simpl in H0. inversion H.
|
|
assert (subsequence2 l (a::s)). exists x. split; assumption.
|
|
apply subsequence2_cons_r with (a := a). assumption.
|
|
intro H. destruct H. destruct H. exists (true :: x).
|
|
split. simpl. apply eq_S. assumption. simpl. rewrite H0. reflexivity.
|
|
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.
|
|
*)
|
|
|
|
|
|
|
|
Theorem subsequence2_dec :
|
|
(forall x y : Type, {x = y} + {x <> y})
|
|
-> forall (l s : list Type), { subsequence2 l s } + { ~ subsequence2 l s }.
|
|
Proof.
|
|
intro H.
|
|
intros l. induction l. intro s. destruct s. left. apply subsequence2_nil_r.
|
|
right. apply subsequence2_nil_cons_r.
|
|
|
|
intro s. assert({subsequence2 l s} + {~ subsequence2 l s}). apply IHl.
|
|
destruct H0.
|
|
|
|
(*
|
|
left. destruct s0.
|
|
destruct H0. exists (false::x). split. simpl. rewrite H0. reflexivity.
|
|
simpl. assumption.
|
|
|
|
destruct s. left. apply subsequence2_nil_r.
|
|
assert ({T=a}+{T<>a}). apply H. destruct H0.
|
|
rewrite e.
|
|
*)
|
|
|
|
rewrite <- subsequence2_cons_eq with (a := a) in s0.
|
|
apply subsequence2_cons_r in s0. left. assumption.
|
|
|
|
destruct s. left. apply subsequence2_nil_r.
|
|
assert ({T=a}+{T<>a}). apply H. destruct H0. rewrite e.
|
|
destruct IHl with (s := s).
|
|
left. rewrite subsequence2_cons_eq. assumption.
|
|
right. rewrite subsequence2_cons_eq. assumption.
|
|
|
|
right. unfold not in n. unfold not. intro I.
|
|
destruct I. destruct H0. destruct x.
|
|
symmetry in H1. apply nil_cons in H1. contradiction H1.
|
|
destruct b.
|
|
inversion H1. rewrite H3 in n0. contradiction n0. reflexivity.
|
|
|
|
assert (subsequence2 l (T::s)). exists x. split.
|
|
inversion H0. reflexivity. assumption. apply n in H2. contradiction H2.
|
|
Qed.
|
|
|
|
|
|
Theorem subsequence2_dec :
|
|
(forall x y : Type, {x = y} + {x <> y})
|
|
-> forall (l s : list Type), { subsequence2 l s } + { ~ subsequence2 l s }.
|
|
Proof.
|
|
intro H.
|
|
intros l s. generalize l. induction s. left. apply subsequence2_nil_r.
|
|
intro l0. destruct l0. right. apply subsequence2_nil_cons_r.
|
|
assert ({ subsequence2 l0 s } + { ~ subsequence2 l0 s }). apply IHs.
|
|
assert ({T=a}+{T<>a}). apply H. destruct H0; destruct H1.
|
|
left. unfold subsequence2. unfold subsequence2 in s0. destruct s0.
|
|
destruct H0. exists (true::x). simpl. rewrite H0. split. reflexivity.
|
|
rewrite e. rewrite H1. reflexivity.
|
|
|
|
(*
|
|
assert ({In a l0}+{~ In a l0}). apply In_dec. assumption.
|
|
destruct H0. apply In_split in i. destruct i.
|
|
*)
|
|
|
|
|
|
|
|
|
|
Theorem subsequence_dec : forall (l s : list Type),
|
|
{ subsequence l s } + { ~ subsequence l s }.
|
|
Proof.
|
|
intros l s. generalize l. induction s. left. apply subsequence_nil_r.
|
|
intro l0. destruct l0. right. apply subsequence_nil_cons_r.
|
|
|
|
|
|
|
|
intros l s. induction s. left. apply subsequence_nil_r.
|
|
destruct l. right. apply subsequence_nil_cons_r.
|
|
|
|
|
|
|
|
unfold subsequence2. destruct s. simpl.
|
|
left. exists nil. easy. right.
|
|
|
|
unfold not. intro H. destruct H. destruct H.
|
|
rewrite combine_nil in H0.
|
|
symmetry in H0. apply nil_cons in H0. assumption.
|
|
|
|
destruct IHl. left. unfold subsequence2. assert (H := s0).
|
|
unfold subsequence2 in H. destruct H. destruct H.
|
|
exists (false::x). split. simpl. apply eq_S. assumption.
|
|
assumption.
|
|
|
|
(* destructurer s puis tester les deux cas : a = (car s) ou non *)
|
|
destruct s. left. unfold subsequence2.
|
|
|
|
|
|
|
|
|
|
Theorem subsequence_dec : forall (l s : list nat),
|
|
{ subsequence2 l s } + { ~ subsequence2 l s }.
|
|
Proof.
|
|
intros l s. induction l.
|
|
unfold subsequence2. destruct s. simpl.
|
|
left. exists nil. easy. right.
|
|
|
|
unfold not. intro H. destruct H. destruct H.
|
|
rewrite combine_nil in H0.
|
|
symmetry in H0. apply nil_cons in H0. assumption.
|
|
|
|
destruct IHl. left. unfold subsequence2. assert (H := s0).
|
|
unfold subsequence2 in H. destruct H. destruct H.
|
|
exists (false::x). split. simpl. apply eq_S. assumption.
|
|
assumption.
|
|
|
|
(* destructurer s puis tester les deux cas : a = (car s) ou non *)
|
|
destruct s. left. unfold subsequence2.
|
|
|
|
exists (repeat false (S (length l))). rewrite repeat_length.
|
|
split. easy. simpl.
|
|
assert (forall u,
|
|
(nil: list nat)
|
|
= map snd (filter fst (combine (repeat false (length u)) u))).
|
|
intro u. induction u. reflexivity. simpl. assumption. apply H.
|
|
|
|
assert ({a=n0}+{a<>n0}). apply PeanoNat.Nat.eq_dec. destruct H.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Theorem subsequence_eq_def : forall l s, subsequence l s <-> subsequence2 l s.
|
|
Proof.
|
|
intro l. induction l.
|
|
(* first part of the induction *)
|
|
intro s. unfold subsequence. unfold subsequence2.
|
|
split. exists nil. split. reflexivity. simpl.
|
|
destruct H. destruct H. destruct H.
|
|
assert (x = nil). destruct x. reflexivity. simpl in H0.
|
|
apply nil_cons in H0. contradiction H0. rewrite H1 in H0.
|
|
simpl in H0. assert (combine s x0 = nil).
|
|
destruct (combine s x0). reflexivity. simpl in H0.
|
|
apply nil_cons in H0. contradiction H0.
|
|
destruct x0. destruct s. reflexivity. simpl in H.
|
|
apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
|
|
destruct s. reflexivity. simpl in H2.
|
|
symmetry in H2. apply nil_cons in H2. contradiction H2.
|
|
exists nil. exists nil. destruct s. simpl. easy.
|
|
destruct H. destruct H.
|
|
assert (x = nil). destruct x. reflexivity. simpl in H.
|
|
apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
|
|
rewrite H1 in H0. simpl in H0.
|
|
symmetry in H0. apply nil_cons in H0. contradiction H0.
|
|
(* second part of the induction *)
|
|
intro s. destruct s. unfold subsequence. unfold subsequence2. split.
|
|
exists (repeat false (S (length l))). rewrite repeat_length.
|
|
split. easy. simpl.
|
|
assert (forall u,
|
|
(nil: list Type)
|
|
= map snd (filter fst (combine (repeat false (length u)) u))).
|
|
intro u. induction u. reflexivity. simpl. assumption. apply H0.
|
|
exists (a::l). exists (nil). simpl. split; try rewrite app_nil_r; reflexivity.
|
|
|
|
(* deux cas : a = n ou non *)
|
|
assert ({a=n} + {a<>n}). apply PeanoNat.Nat.eq_dec. destruct H.
|
|
unfold subsequence. unfold subsequence2. split.
|
|
|
|
|
|
|
|
|
|
|
|
destruct H. destruct H. destruct H.
|
|
assert (x0 = nil). symmetry in H. apply length_zero_iff_nil in H.
|
|
assumption. rewrite H1 in H0. simpl in H0.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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.
|