Update
This commit is contained in:
parent
8e9e85bd71
commit
5db7822d3c
@ -62,7 +62,7 @@ Proof.
|
|||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
Lemma subsequence_alt_defs {X: Type} :
|
Lemma Subsequence_alt_defs {X: Type} :
|
||||||
forall l s : list X,
|
forall l s : list X,
|
||||||
(exists (l1: list X) (l2 : list (list X)),
|
(exists (l1: list X) (l2 : list (list X)),
|
||||||
length s = length l2
|
length s = length l2
|
||||||
@ -109,7 +109,7 @@ Proof.
|
|||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
Lemma subsequence_alt_defs2 {X: Type} :
|
Lemma Subsequence_alt_defs2 {X: Type} :
|
||||||
forall l s : list X,
|
forall l s : list X,
|
||||||
(exists (t: list bool),
|
(exists (t: list bool),
|
||||||
length t = length l /\ s = map snd (filter fst (combine t l)))
|
length t = length l /\ s = map snd (filter fst (combine t l)))
|
||||||
@ -134,7 +134,7 @@ Proof.
|
|||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
Theorem subsequence_flat_map {X: Type} :
|
Theorem Subsequence_flat_map {X: Type} :
|
||||||
forall l s : list X, Subsequence l s
|
forall l s : list X, Subsequence l s
|
||||||
<-> exists (l1: list X) (l2 : list (list X)),
|
<-> exists (l1: list X) (l2 : list (list X)),
|
||||||
length s = length l2
|
length s = length l2
|
||||||
@ -145,19 +145,19 @@ Proof.
|
|||||||
reflexivity. destruct H. destruct H. destruct H. apply IHs in H0.
|
reflexivity. destruct H. destruct H. destruct H. apply IHs in H0.
|
||||||
destruct H0. destruct H0. destruct H0. exists x. exists (x1::x2).
|
destruct H0. destruct H0. destruct H0. exists x. exists (x1::x2).
|
||||||
split; simpl; [rewrite H0 | rewrite <- H1]; easy.
|
split; simpl; [rewrite H0 | rewrite <- H1]; easy.
|
||||||
intro. apply subsequence_alt_defs in H. apply subsequence_alt_defs2.
|
intro. apply Subsequence_alt_defs in H. apply Subsequence_alt_defs2.
|
||||||
assumption.
|
assumption.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
Theorem subsequence_bools {X: Type} :
|
Theorem Subsequence_bools {X: Type} :
|
||||||
forall l s : list X, Subsequence l s
|
forall l s : list X, Subsequence l s
|
||||||
<-> (exists (t: list bool),
|
<-> (exists (t: list bool),
|
||||||
length t = length l /\ s = map snd (filter fst (combine t l))).
|
length t = length l /\ s = map snd (filter fst (combine t l))).
|
||||||
Proof.
|
Proof.
|
||||||
intros l s. split; intro. apply subsequence_alt_defs.
|
intros l s. split; intro. apply Subsequence_alt_defs.
|
||||||
apply subsequence_flat_map. assumption.
|
apply Subsequence_flat_map. assumption.
|
||||||
apply subsequence_alt_defs2. assumption.
|
apply Subsequence_alt_defs2. assumption.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
@ -172,19 +172,19 @@ Proof.
|
|||||||
apply IHl. destruct H0.
|
apply IHl. destruct H0.
|
||||||
|
|
||||||
rewrite <- Subsequence_cons_eq with (a := a) in s0.
|
rewrite <- Subsequence_cons_eq with (a := a) in s0.
|
||||||
apply Subsequence_cons_r in s0. rewrite subsequence_bools in s0.
|
apply Subsequence_cons_r in s0. rewrite Subsequence_bools in s0.
|
||||||
left. rewrite subsequence_bools. assumption.
|
left. rewrite Subsequence_bools. assumption.
|
||||||
|
|
||||||
destruct s. left. apply Subsequence_nil_r.
|
destruct s. left. apply Subsequence_nil_r.
|
||||||
assert ({x=a}+{x<>a}). apply H. destruct H0. rewrite e.
|
assert ({x=a}+{x<>a}). apply H. destruct H0. rewrite e.
|
||||||
destruct IHl with (s := s); [ left | right ];
|
destruct IHl with (s := s); [ left | right ];
|
||||||
rewrite Subsequence_cons_eq. assumption. assumption.
|
rewrite Subsequence_cons_eq. assumption. assumption.
|
||||||
|
|
||||||
right. intro I. rewrite subsequence_bools in I.
|
right. intro I. rewrite Subsequence_bools in I.
|
||||||
destruct I. destruct H0. destruct x0.
|
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. inversion H1. rewrite H3 in n0. easy.
|
destruct b. inversion H1. rewrite H3 in n0. easy.
|
||||||
apply n. rewrite subsequence_bools. exists x0; split; inversion H0; easy.
|
apply n. rewrite Subsequence_bools. exists x0; split; inversion H0; easy.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user