Update
This commit is contained in:
parent
91ec8856d2
commit
88e20199e7
@ -359,16 +359,11 @@ Proof.
|
|||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
|
Theorem Subsequence_length_eq {X: Type} :
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
Theorem subsequence_length_eq {X: Type} :
|
|
||||||
forall (u v: list X),
|
forall (u v: list X),
|
||||||
subsequence u v -> length u = length v -> u = v.
|
Subsequence u v -> length u = length v -> u = v.
|
||||||
Proof.
|
Proof.
|
||||||
intros u v. intros H I. apply subsequence_eq_def_1 in H.
|
intros u v. intros H I. apply Subsequence_bools in H.
|
||||||
destruct H. destruct H. rewrite H0 in I.
|
destruct H. destruct H. rewrite H0 in I.
|
||||||
rewrite map_length in I.
|
rewrite map_length in I.
|
||||||
replace (length u) with (length (combine x u)) in I.
|
replace (length u) with (length (combine x u)) in I.
|
||||||
@ -386,20 +381,25 @@ Proof.
|
|||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
Theorem subsequence_in {X: Type} :
|
Theorem Subsequence_in {X: Type} :
|
||||||
forall (u: list X) a, In a u <-> subsequence u [a].
|
forall (u: list X) a, In a u <-> Subsequence u [a].
|
||||||
Proof.
|
Proof.
|
||||||
intros u a. split.
|
intros u a. rewrite Subsequence_flat_map. split.
|
||||||
induction u; intro H. apply in_nil in H. contradiction.
|
induction u; intro H. apply in_nil in H. contradiction.
|
||||||
destruct H. rewrite H. exists nil. exists [u]. split. reflexivity.
|
destruct H. rewrite H. exists nil. exists [u]. split. reflexivity.
|
||||||
simpl. rewrite app_nil_r. reflexivity. apply subsequence_cons_l.
|
simpl. rewrite app_nil_r. reflexivity.
|
||||||
apply IHu. assumption.
|
rewrite <- Subsequence_flat_map. apply Subsequence_cons_l.
|
||||||
|
apply Subsequence_flat_map. apply IHu. assumption.
|
||||||
intro H. destruct H. destruct H. destruct H. rewrite H0. apply in_or_app.
|
intro H. destruct H. destruct H. destruct H. rewrite H0. apply in_or_app.
|
||||||
right. destruct x0. apply PeanoNat.Nat.neq_succ_0 in H. contradiction.
|
right. destruct x0. apply PeanoNat.Nat.neq_succ_0 in H. contradiction.
|
||||||
left. reflexivity.
|
left. reflexivity.
|
||||||
Qed.
|
Qed.
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
Theorem subsequence_rev {X: Type} :
|
Theorem subsequence_rev {X: Type} :
|
||||||
forall (u v: list X), subsequence u v <-> subsequence (rev u) (rev v).
|
forall (u v: list X), subsequence u v <-> subsequence (rev u) (rev v).
|
||||||
Proof.
|
Proof.
|
||||||
|
Loading…
Reference in New Issue
Block a user