Update
This commit is contained in:
parent
9325baf42b
commit
81f0311165
@ -183,16 +183,6 @@ Proof.
|
||||
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.
|
||||
|
||||
@ -213,74 +203,6 @@ Proof.
|
||||
Qed.
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
(*
|
||||
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 x y : Type, {x = y} + {x <> y})
|
||||
-> (forall l s, subsequence l s <-> subsequence2 l s).
|
||||
|
Loading…
Reference in New Issue
Block a user