Update
This commit is contained in:
parent
951e3cb244
commit
ab46174c21
@ -25,15 +25,14 @@ Definition subsequence3 (l s : list Type) :=
|
||||
|
||||
Theorem subsequence_nil_r : forall (l : list Type), subsequence l nil.
|
||||
Proof.
|
||||
intro l. unfold subsequence. exists l. exists nil. rewrite app_nil_r.
|
||||
split; easy.
|
||||
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 subsequence. unfold not. intro H.
|
||||
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.
|
||||
@ -44,7 +43,7 @@ Qed.
|
||||
|
||||
Theorem subsequence2_nil_r : forall (l : list Type), subsequence2 l nil.
|
||||
Proof.
|
||||
intro l. unfold subsequence2.
|
||||
intro l.
|
||||
exists (repeat false (length l)). rewrite repeat_length.
|
||||
split. easy.
|
||||
induction l. reflexivity. simpl. assumption.
|
||||
@ -54,7 +53,7 @@ Qed.
|
||||
Theorem subsequence2_nil_cons_r : forall (l: list Type) (a:Type),
|
||||
~ subsequence2 nil (a::l).
|
||||
Proof.
|
||||
intros l a. unfold subsequence2. unfold not. intro H. destruct H.
|
||||
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.
|
||||
@ -64,7 +63,7 @@ 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. unfold subsequence2 in H.
|
||||
intros l s a. intro H.
|
||||
destruct H. destruct H. exists (false::x).
|
||||
split. simpl. apply eq_S. assumption.
|
||||
simpl. assumption.
|
||||
@ -75,14 +74,11 @@ 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. unfold subsequence2 in H.
|
||||
destruct H. destruct H. destruct x.
|
||||
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.
|
||||
unfold subsequence2. exists (false::x).
|
||||
split; try rewrite <- H; reflexivity.
|
||||
simpl in H0.
|
||||
apply subsequence2_cons_l. apply IHl with (a := a0).
|
||||
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.
|
||||
@ -93,8 +89,7 @@ Theorem subsequence2_cons_eq : forall (l1 l2: list Type) (a: Type),
|
||||
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.
|
||||
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.
|
||||
|
Loading…
Reference in New Issue
Block a user