Update
This commit is contained in:
parent
f5c5c7928e
commit
7c41d5c354
|
@ -23,13 +23,13 @@ Definition subsequence3 (l s : list Type) :=
|
||||||
exists f, s = fst (partition f l).
|
exists f, s = fst (partition f l).
|
||||||
*)
|
*)
|
||||||
|
|
||||||
Theorem subsequence_nil_r : forall (l : list Type), subsequence l nil.
|
Theorem subsequence_nil_r {X: Type}: forall (l : list X), subsequence l nil.
|
||||||
Proof.
|
Proof.
|
||||||
intro l. exists l. exists nil. rewrite app_nil_r. split; easy.
|
intro l. exists l. exists nil. rewrite app_nil_r. split; easy.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
Theorem subsequence_nil_cons_r : forall (l: list Type) (a:Type),
|
Theorem subsequence_nil_cons_r {X: Type}: forall (l: list X) (a:X),
|
||||||
~ subsequence nil (a::l).
|
~ subsequence nil (a::l).
|
||||||
Proof.
|
Proof.
|
||||||
intros l a. unfold not. intro H.
|
intros l a. unfold not. intro H.
|
||||||
|
@ -41,7 +41,7 @@ Proof.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
Theorem subsequence2_nil_r : forall (l : list Type), subsequence2 l nil.
|
Theorem subsequence2_nil_r {X: Type} : forall (l : list X), subsequence2 l nil.
|
||||||
Proof.
|
Proof.
|
||||||
intro l.
|
intro l.
|
||||||
exists (repeat false (length l)). rewrite repeat_length.
|
exists (repeat false (length l)). rewrite repeat_length.
|
||||||
|
@ -50,7 +50,7 @@ Proof.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
Theorem subsequence2_nil_cons_r : forall (l: list Type) (a:Type),
|
Theorem subsequence2_nil_cons_r {X: Type}: forall (l: list X) (a:X),
|
||||||
~ subsequence2 nil (a::l).
|
~ subsequence2 nil (a::l).
|
||||||
Proof.
|
Proof.
|
||||||
intros l a. unfold not. intro H. destruct H.
|
intros l a. unfold not. intro H. destruct H.
|
||||||
|
@ -60,7 +60,7 @@ Proof.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
Theorem subsequence_cons_l : forall (l s: list Type) (a: Type),
|
Theorem subsequence_cons_l {X: Type}: forall (l s: list X) (a: X),
|
||||||
subsequence l s -> subsequence (a::l) s.
|
subsequence l s -> subsequence (a::l) s.
|
||||||
Proof.
|
Proof.
|
||||||
intros l s a. intro H.
|
intros l s a. intro H.
|
||||||
|
@ -70,7 +70,7 @@ Proof.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
Theorem subsequence2_cons_l : forall (l s: list Type) (a: Type),
|
Theorem subsequence2_cons_l {X: Type} : forall (l s: list X) (a: X),
|
||||||
subsequence2 l s -> subsequence2 (a::l) s.
|
subsequence2 l s -> subsequence2 (a::l) s.
|
||||||
Proof.
|
Proof.
|
||||||
intros l s a. intro H.
|
intros l s a. intro H.
|
||||||
|
@ -80,7 +80,7 @@ Proof.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
Theorem subsequence_cons_r : forall (l s: list Type) (a: Type),
|
Theorem subsequence_cons_r {X: Type} : forall (l s: list X) (a: X),
|
||||||
subsequence l (a::s) -> subsequence l s.
|
subsequence l (a::s) -> subsequence l s.
|
||||||
Proof.
|
Proof.
|
||||||
intros l s a. intro H. destruct H. destruct H. destruct H.
|
intros l s a. intro H. destruct H. destruct H. destruct H.
|
||||||
|
@ -90,7 +90,7 @@ Proof.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
Theorem subsequence2_cons_r : forall (l s: list Type) (a: Type),
|
Theorem subsequence2_cons_r {X: Type} : forall (l s: list X) (a: X),
|
||||||
subsequence2 l (a::s) -> subsequence2 l s.
|
subsequence2 l (a::s) -> subsequence2 l s.
|
||||||
Proof.
|
Proof.
|
||||||
intro l. induction l. intros. apply subsequence2_nil_cons_r in H.
|
intro l. induction l. intros. apply subsequence2_nil_cons_r in H.
|
||||||
|
@ -104,7 +104,7 @@ Proof.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
Theorem subsequence_cons_eq : forall (l1 l2: list Type) (a: Type),
|
Theorem subsequence_cons_eq {X: Type} : forall (l1 l2: list X) (a: X),
|
||||||
subsequence (a::l1) (a::l2) <-> subsequence l1 l2.
|
subsequence (a::l1) (a::l2) <-> subsequence l1 l2.
|
||||||
Proof.
|
Proof.
|
||||||
intros l s a. split. intro H.
|
intros l s a. split. intro H.
|
||||||
|
@ -115,7 +115,7 @@ Proof.
|
||||||
inversion H. rewrite H3. split; reflexivity.
|
inversion H. rewrite H3. split; reflexivity.
|
||||||
destruct x0. simpl in H0.
|
destruct x0. simpl in H0.
|
||||||
apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
|
apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
|
||||||
exists (x ++ (a::l0)). exists x0. inversion H. rewrite H2. split. reflexivity.
|
exists (x1 ++ (a::l0)). exists x0. inversion H. rewrite H2. split. reflexivity.
|
||||||
inversion H0. rewrite <- app_assoc. apply app_inv_head_iff.
|
inversion H0. rewrite <- app_assoc. apply app_inv_head_iff.
|
||||||
rewrite app_comm_cons. reflexivity.
|
rewrite app_comm_cons. reflexivity.
|
||||||
|
|
||||||
|
@ -125,7 +125,7 @@ Proof.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
Theorem subsequence2_cons_eq : forall (l1 l2: list Type) (a: Type),
|
Theorem subsequence2_cons_eq {X: Type}: forall (l1 l2: list X) (a: X),
|
||||||
subsequence2 (a::l1) (a::l2) <-> subsequence2 l1 l2.
|
subsequence2 (a::l1) (a::l2) <-> subsequence2 l1 l2.
|
||||||
Proof.
|
Proof.
|
||||||
intros l s a. split. intro H. unfold subsequence2 in H.
|
intros l s a. split. intro H. unfold subsequence2 in H.
|
||||||
|
@ -167,9 +167,9 @@ Qed.
|
||||||
*)
|
*)
|
||||||
|
|
||||||
|
|
||||||
Theorem subsequence2_dec :
|
Theorem subsequence2_dec {X: Type}:
|
||||||
(forall x y : Type, {x = y} + {x <> y})
|
(forall x y : X, {x = y} + {x <> y})
|
||||||
-> forall (l s : list Type), { subsequence2 l s } + { ~ subsequence2 l s }.
|
-> forall (l s : list X), { subsequence2 l s } + { ~ subsequence2 l s }.
|
||||||
Proof.
|
Proof.
|
||||||
intro H.
|
intro H.
|
||||||
intros l. induction l. intro s. destruct s. left. apply subsequence2_nil_r.
|
intros l. induction l. intro s. destruct s. left. apply subsequence2_nil_r.
|
||||||
|
@ -182,25 +182,25 @@ Proof.
|
||||||
apply subsequence2_cons_r in s0. left. assumption.
|
apply subsequence2_cons_r in s0. left. assumption.
|
||||||
|
|
||||||
destruct s. left. apply subsequence2_nil_r.
|
destruct s. left. apply subsequence2_nil_r.
|
||||||
assert ({T=a}+{T<>a}). apply H. destruct H0. rewrite e.
|
assert ({x=a}+{x<>a}). apply H. destruct H0. rewrite e.
|
||||||
destruct IHl with (s := s).
|
destruct IHl with (s := s).
|
||||||
left. rewrite subsequence2_cons_eq. assumption.
|
left. rewrite subsequence2_cons_eq. assumption.
|
||||||
right. rewrite subsequence2_cons_eq. assumption.
|
right. rewrite subsequence2_cons_eq. assumption.
|
||||||
|
|
||||||
right. unfold not in n. unfold not. intro I.
|
right. unfold not in n. unfold not. intro I.
|
||||||
destruct I. destruct H0. destruct x.
|
destruct I. destruct H0. destruct x0.
|
||||||
symmetry in H1. apply nil_cons in H1. contradiction H1.
|
symmetry in H1. apply nil_cons in H1. contradiction H1.
|
||||||
destruct b.
|
destruct b.
|
||||||
inversion H1. rewrite H3 in n0. contradiction n0. reflexivity.
|
inversion H1. rewrite H3 in n0. contradiction n0. reflexivity.
|
||||||
|
|
||||||
assert (subsequence2 l (T::s)). exists x. split.
|
assert (subsequence2 l (x::s)). exists x0. split.
|
||||||
inversion H0. reflexivity. assumption. apply n in H2. contradiction H2.
|
inversion H0. reflexivity. assumption. apply n in H2. contradiction H2.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
Theorem subsequence_eq_def :
|
Theorem subsequence_eq_def {X: Type} :
|
||||||
(forall x y : Type, {x = y} + {x <> y})
|
(forall (x y : X), {x = y} + {x <> y})
|
||||||
-> (forall l s : list Type, subsequence l s <-> subsequence2 l s).
|
-> (forall l s : list X, subsequence l s <-> subsequence2 l s).
|
||||||
Proof.
|
Proof.
|
||||||
intro I. intro l. induction l.
|
intro I. intro l. induction l.
|
||||||
(* first part of the induction *)
|
(* first part of the induction *)
|
||||||
|
@ -218,7 +218,7 @@ Proof.
|
||||||
symmetry in H2. apply nil_cons in H2. contradiction H2.
|
symmetry in H2. apply nil_cons in H2. contradiction H2.
|
||||||
exists nil. exists nil. destruct s. simpl. easy.
|
exists nil. exists nil. destruct s. simpl. easy.
|
||||||
destruct H. destruct H.
|
destruct H. destruct H.
|
||||||
assert (x = nil). destruct x. reflexivity. simpl in H.
|
assert (x0 = nil). destruct x0. reflexivity. simpl in H.
|
||||||
apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
|
apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
|
||||||
rewrite H1 in H0. simpl in H0.
|
rewrite H1 in H0. simpl in H0.
|
||||||
symmetry in H0. apply nil_cons in H0. contradiction H0.
|
symmetry in H0. apply nil_cons in H0. contradiction H0.
|
||||||
|
@ -227,38 +227,38 @@ Proof.
|
||||||
exists (repeat false (S (length l))). rewrite repeat_length.
|
exists (repeat false (S (length l))). rewrite repeat_length.
|
||||||
split. easy. simpl.
|
split. easy. simpl.
|
||||||
assert (forall u,
|
assert (forall u,
|
||||||
(nil: list Type)
|
(nil: list X)
|
||||||
= map snd (filter fst (combine (repeat false (length u)) u))).
|
= map snd (filter fst (combine (repeat false (length u)) u))).
|
||||||
intro u. induction u. reflexivity. simpl. assumption. apply H0.
|
intro u. induction u. reflexivity. simpl. assumption. apply H0.
|
||||||
exists (a::l). exists (nil). simpl. split; try rewrite app_nil_r; reflexivity.
|
exists (a::l). exists (nil). simpl. split; try rewrite app_nil_r; reflexivity.
|
||||||
(* deux cas : a = n ou non *)
|
(* deux cas : a = n ou non *)
|
||||||
assert ({a=T} + {a<>T}). apply I. destruct H.
|
assert ({a=x} + {a<>x}). apply I. destruct H.
|
||||||
rewrite e. rewrite subsequence2_cons_eq. rewrite <- IHl.
|
rewrite e. rewrite subsequence2_cons_eq. rewrite <- IHl.
|
||||||
rewrite subsequence_cons_eq. split; intro; assumption.
|
rewrite subsequence_cons_eq. split; intro; assumption.
|
||||||
|
|
||||||
split; intro H. apply subsequence2_cons_l. apply IHl.
|
split; intro H. apply subsequence2_cons_l. apply IHl.
|
||||||
destruct H. destruct H. destruct H.
|
destruct H. destruct H. destruct H.
|
||||||
destruct x. destruct x0.
|
destruct x0. destruct x1.
|
||||||
apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
|
apply PeanoNat.Nat.neq_succ_0 in H. contradiction H.
|
||||||
simpl in H0. inversion H0. rewrite H2 in n. contradiction n.
|
simpl in H0. inversion H0. rewrite H2 in n. contradiction n.
|
||||||
reflexivity. inversion H0.
|
reflexivity. inversion H0.
|
||||||
exists x. exists x0. split. assumption.
|
exists x2. exists x1. split. assumption.
|
||||||
reflexivity.
|
reflexivity.
|
||||||
|
|
||||||
apply subsequence_cons_l. apply IHl.
|
apply subsequence_cons_l. apply IHl.
|
||||||
destruct H. destruct H.
|
destruct H. destruct H.
|
||||||
destruct x. simpl in H0.
|
destruct x0. simpl in H0.
|
||||||
symmetry in H0. apply nil_cons in H0. contradiction H0.
|
symmetry in H0. apply nil_cons in H0. contradiction H0.
|
||||||
destruct b. simpl in H0. inversion H0. rewrite H2 in n.
|
destruct b. simpl in H0. inversion H0. rewrite H2 in n.
|
||||||
contradiction n. reflexivity.
|
contradiction n. reflexivity.
|
||||||
exists x. inversion H. inversion H0.
|
exists x0. inversion H. inversion H0.
|
||||||
split; reflexivity.
|
split; reflexivity.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
Theorem subsequence_dec :
|
Theorem subsequence_dec {X: Type}:
|
||||||
(forall x y : Type, {x = y} + {x <> y})
|
(forall x y : X, {x = y} + {x <> y})
|
||||||
-> forall (l s : list Type), { subsequence l s } + { ~ subsequence l s }.
|
-> forall (l s : list X), { subsequence l s } + { ~ subsequence l s }.
|
||||||
Proof.
|
Proof.
|
||||||
intro H. intros l s.
|
intro H. intros l s.
|
||||||
assert ({ subsequence2 l s } + { ~ subsequence2 l s }).
|
assert ({ subsequence2 l s } + { ~ subsequence2 l s }).
|
||||||
|
@ -285,3 +285,7 @@ Proof.
|
||||||
exists [1].
|
exists [1].
|
||||||
exists [[3];[5]]. simpl. easy.
|
exists [[3];[5]]. simpl. easy.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
Example test3: subsequence [1;2;3;4;5] [1;3;5].
|
||||||
|
Proof.
|
||||||
|
rewrite subsequence_eq_def.
|
||||||
|
|
Loading…
Reference in New Issue
Block a user