This commit is contained in:
Thomas Baruchel 2023-12-06 10:00:08 +01:00
parent 9ad87a7470
commit a948caaef8

View File

@ -538,17 +538,14 @@ Proof.
Qed. Qed.
Theorem Subsequence_split_2 {X: Type} :
Theorem subsequence_split_2 {X: Type} :
forall (u v w: list X), forall (u v w: list X),
subsequence u (v++w) Subsequence u (v++w)
-> (exists a b, u = a++b /\ (subsequence a v) /\ subsequence b w). -> (exists a b, u = a++b /\ (Subsequence a v) /\ Subsequence b w).
Proof. Proof.
intros u v w. intro H. destruct H. destruct H. destruct H. intros u v w. intro H.
apply Subsequence_flat_map in H.
destruct H. destruct H. destruct H.
exists (x ++ exists (x ++
flat_map (fun e : X * list X => fst e :: snd e) (combine v x0)). flat_map (fun e : X * list X => fst e :: snd e) (combine v x0)).
exists ( exists (
@ -565,70 +562,71 @@ Proof.
simpl. rewrite IHw0. reflexivity. inversion I. reflexivity. simpl. rewrite IHw0. reflexivity. inversion I. reflexivity.
rewrite L. reflexivity. rewrite app_length in H. rewrite H. rewrite L. reflexivity. rewrite app_length in H. rewrite H.
reflexivity. split. reflexivity. split.
exists x. exists (firstn (length v) x0). split.
rewrite firstn_length. rewrite <- H. rewrite app_length. apply Subsequence_flat_map. exists x. exists (firstn (length v) x0).
split. rewrite firstn_length. rewrite <- H. rewrite app_length.
rewrite min_l. reflexivity. apply PeanoNat.Nat.le_add_r. rewrite min_l. reflexivity. apply PeanoNat.Nat.le_add_r.
rewrite combine_firstn_l. reflexivity. rewrite combine_firstn_l. reflexivity.
exists nil. exists (skipn (length v) x0). split. apply Subsequence_flat_map. exists nil. exists (skipn (length v) x0).
rewrite app_length in H. rewrite skipn_length. rewrite <- H. split. rewrite app_length in H. rewrite skipn_length. rewrite <- H.
rewrite PeanoNat.Nat.add_sub_swap. rewrite PeanoNat.Nat.sub_diag. rewrite PeanoNat.Nat.add_sub_swap. rewrite PeanoNat.Nat.sub_diag.
reflexivity. reflexivity. reflexivity. reflexivity. reflexivity. reflexivity.
Qed. Qed.
Theorem subsequence_filter_2 {X: Type} : Theorem Subsequence_filter_2 {X: Type} :
forall (u v: list X) f, forall (u v: list X) f,
subsequence u v -> subsequence (filter f u) (filter f v). Subsequence u v -> Subsequence (filter f u) (filter f v).
Proof. Proof.
intros u v. generalize u. induction v; intros u0 f; intro H. intros u v. generalize u. induction v; intros u0 f; intro H.
apply subsequence_nil_r. apply Subsequence_nil_r.
assert (f a = true \/ f a = false). assert (f a = true \/ f a = false).
destruct (f a); [ left | right ]; reflexivity. destruct H0. destruct (f a); [ left | right ]; reflexivity. destruct H0.
simpl. rewrite H0. simpl. rewrite H0.
replace (a::v) with ([a] ++ v) in H. apply subsequence_split_2 in H. replace (a::v) with ([a] ++ v) in H. apply Subsequence_split_2 in H.
destruct H. destruct H. destruct H. destruct H1. destruct H. destruct H. destruct H. destruct H1.
assert (subsequence ((filter f x) ++ (filter f x0)) assert (Subsequence ((filter f x) ++ (filter f x0))
((filter f [a]) ++ (filter f v))). ((filter f [a]) ++ (filter f v))).
apply subsequence_app. simpl. rewrite H0. apply Subsequence_app. simpl. rewrite H0.
apply subsequence_incl in H1. apply incl_cons_inv in H1. destruct H1. apply Subsequence_incl in H1. apply incl_cons_inv in H1. destruct H1.
assert (In a (filter f x)). apply filter_In. split; assumption. assert (In a (filter f x)). apply filter_In. split; assumption.
apply subsequence_in. assumption. apply IHv. assumption. apply Subsequence_in. assumption. apply IHv. assumption.
rewrite <- filter_app in H3. rewrite <- H in H3. simpl in H3. rewrite <- filter_app in H3. rewrite <- H in H3. simpl in H3.
rewrite H0 in H3. assumption. reflexivity. rewrite H0 in H3. assumption. reflexivity.
simpl. rewrite H0. apply IHv. apply subsequence_cons_r in H. simpl. rewrite H0. apply IHv. apply Subsequence_cons_r in H.
assumption. assumption.
Qed. Qed.
Theorem subsequence_add {X: Type} : Theorem Subsequence_add {X: Type} :
forall (u v w: list X) x, subsequence u v -> Add x u w -> subsequence w v. forall (u v w: list X) x, Subsequence u v -> Add x u w -> Subsequence w v.
Proof. Proof.
intros u v w. generalize u v. intros u v w. generalize u v.
induction w; intros u0 v0 x; intros H I; inversion I. induction w; intros u0 v0 x; intros H I; inversion I.
rewrite <- H2. apply subsequence_cons_l. rewrite <- H3. assumption. rewrite <- H2. apply Subsequence_cons_l. rewrite <- H3. assumption.
assert (J := H). apply subsequence_eq_def_1 in H. rewrite <- H1 in H. assert (J := H). apply Subsequence_bools in H. rewrite <- H1 in H.
rewrite H0 in H. destruct H. destruct H. rewrite H0 in H. destruct H. destruct H.
destruct x1. apply O_S in H. contradiction. destruct b. destruct x1. apply O_S in H. contradiction. destruct b.
rewrite H4. simpl. apply subsequence_double_cons. rewrite H4. simpl. apply Subsequence_double_cons.
apply IHw with (u := l) (x := x). apply IHw with (u := l) (x := x).
apply subsequence_eq_def_3. apply subsequence_eq_def_2. exists x1. apply Subsequence_bools. exists x1.
inversion H. split; reflexivity. assumption. inversion H. split; reflexivity. assumption.
apply subsequence_cons_r with (a:=a). apply Subsequence_cons_r with (a:=a).
rewrite H4. simpl. apply subsequence_double_cons. rewrite H4. simpl. apply Subsequence_double_cons.
apply IHw with (u := l) (x := x). apply IHw with (u := l) (x := x).
apply subsequence_eq_def_3. apply subsequence_eq_def_2. exists x1. apply Subsequence_bools. exists x1.
inversion H. split; reflexivity. assumption. inversion H. split; reflexivity. assumption.
Qed. Qed.
Theorem subsequence_nodup {X: Type} : Theorem Subsequence_nodup {X: Type} :
forall (u v: list X), subsequence u v -> NoDup u -> NoDup v. forall (u v: list X), Subsequence u v -> NoDup u -> NoDup 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. destruct H. destruct H. rewrite H0.
assert (J: forall z (q: list X), assert (J: forall z (q: list X),
@ -654,23 +652,22 @@ Proof.
Qed. Qed.
Theorem subsequence_in_2 {X: Type} : Theorem Subsequence_in_2 {X: Type} :
forall (u v: list X) a, subsequence u v -> In a v -> In a u. forall (u v: list X) a, Subsequence u v -> In a v -> In a u.
Proof. Proof.
intros u v. generalize u. induction v; intros u0 a0; intros H I. intros u v. generalize u. induction v; intros u0 a0; intros H I.
contradiction I. destruct I. contradiction I. destruct I.
apply subsequence_eq_def_1 in H. apply subsequence_eq_def_2 in H.
destruct H. destruct H. destruct H. rewrite H. rewrite H0. destruct H. destruct H. destruct H. rewrite H. rewrite H0.
apply in_elt. apply IHv. apply subsequence_cons_r in H. apply in_elt. apply IHv. apply Subsequence_cons_r in H.
assumption. assumption. assumption. assumption.
Qed. Qed.
Theorem subsequence_not_in {X: Type} : Theorem Subsequence_not_in {X: Type} :
forall (u v: list X) a, subsequence u v -> ~ In a u -> ~ In a v. forall (u v: list X) a, Subsequence u v -> ~ In a u -> ~ In a v.
Proof. Proof.
intros u v. generalize u. induction v; intros u0 a0; intros H I. intros u v. generalize u. induction v; intros u0 a0; intros H I.
easy. apply not_in_cons. split. apply subsequence_incl in H. easy. apply not_in_cons. split. apply Subsequence_incl in H.
apply incl_cons_inv in H. destruct H. apply incl_cons_inv in H. destruct H.
assert (forall z (x y: X), In x z -> ~ In y z -> x <> y). assert (forall z (x y: X), In x z -> ~ In y z -> x <> y).
@ -680,27 +677,27 @@ Proof.
apply IHz. assumption. apply IHz. assumption.
apply not_in_cons in K. destruct K. assumption. apply not_eq_sym. apply not_in_cons in K. destruct K. assumption. apply not_eq_sym.
generalize I. generalize H. apply H1. generalize I. apply IHv. generalize I. generalize H. apply H1. generalize I. apply IHv.
apply subsequence_cons_r in H. assumption. apply Subsequence_cons_r in H. assumption.
Qed. Qed.
Theorem subsequence_as_filter {X: Type} : Theorem Subsequence_as_filter {X: Type} :
forall (u: list X) f, subsequence u (filter f u). forall (u: list X) f, Subsequence u (filter f u).
Proof. Proof.
intros u f. apply subsequence_eq_def_3. apply subsequence_eq_def_2. intros u f. apply Subsequence_bools.
exists (map f u). split. apply map_length. exists (map f u). split. apply map_length.
induction u. reflexivity. simpl. destruct (f a). induction u. reflexivity. simpl. destruct (f a).
simpl. rewrite IHu. reflexivity. assumption. simpl. rewrite IHu. reflexivity. assumption.
Qed. Qed.
Theorem subsequence_as_partition {X: Type} : Theorem Subsequence_as_partition {X: Type} :
forall (u v w: list X) f, forall (u v w: list X) f,
(v, w) = partition f u -> (subsequence u v) /\ (subsequence u w). (v, w) = partition f u -> (Subsequence u v) /\ (Subsequence u w).
Proof. Proof.
intros u v w f. intro H. rewrite partition_as_filter in H. split. intros u v w f. intro H. rewrite partition_as_filter in H. split.
replace v with (fst (v, w)). rewrite H. simpl. replace v with (fst (v, w)). rewrite H. simpl.
apply subsequence_as_filter. reflexivity. apply Subsequence_as_filter. reflexivity.
replace w with (snd (v, w)). rewrite H. simpl. replace w with (snd (v, w)). rewrite H. simpl.
apply subsequence_as_filter. reflexivity. apply Subsequence_as_filter. reflexivity.
Qed. Qed.