# Library CFG.Lists

Instance eq_dec_prod X Y (Dx : eq_dec X) (Dy : eq_dec Y) :

eq_dec (X × Y).

Proof.

intros [x y] [x' y'].

decide (x = x') ; decide (y = y') ; try (right ; intros H ; inv H ; tauto).

left. f_equal ; auto.

Defined.

Instance filter_prod_dec X Y {D : eq_dec X} (x : X) :

∀ (e : X × Y) , dec ((fun e : X × Y ⇒ match e with (xe, _) ⇒ x = xe end) e).

Proof.

intros [xe _]. auto.

Defined.

Instance splitList_dec X (D : eq_dec X) (xs ys : list X) : dec (∃ zs, xs = ys ++ zs).

Proof.

revert xs.

induction ys as [| s ys IHv]; intros xs.

- left. ∃ xs. auto.

- destruct xs as [|s' xs].

+ right. intros [zs H]. inv H.

+ decide (s = s') as [DS | DS].

× rewrite DS.

destruct (IHv xs) as [IH | IH].

{ left. destruct IH as [zs IH]. ∃ zs. rewrite IH. auto. }

{ right. intros [zs H]. simpl in H.

apply IH. ∃ zs. now inv H. }

× right. intros [zs H]. inv H. tauto.

Defined.

Fixpoint slists (X : Type) (p : X → Prop) (pdec : ∀ x, dec (p x)) (xs : list X) : list (list X) :=

match xs with

| [] ⇒ [[]]

| s::xs' ⇒

let

ys := slists pdec xs'

in let

zs := map (cons s) ys

in

if decision (p s) then ys ++ zs else zs

end.

Arguments slists {X} p {pdec} xs.

Inductive slist (X : Type) (p : X → Prop) {pdec : ∀ x, dec (p x)} : list X → list X → Prop :=

| subnil : slist nil nil

| subconsp s ys xs: p s → slist ys xs → slist ys (s :: xs)

| subcons s ys xs : slist ys xs → slist (s :: ys) (s :: xs).

Arguments slist {X} p {pdec} ys xs.

Hint Constructors slist.

Lemma slists_slist (X : Type) (xs ys : list X) (p : X → Prop) (D : ∀ x, dec (p x)) :

ys el slists p xs ↔ slist p ys xs.

Proof with (apply in_map_iff in H ; destruct H as [ys' [H0 H1]] ; subst ; auto).

split.

- revert ys.

induction xs as [| s xs' IHu] ; intros ys H ; simpl in H.

+ destruct H as [H | H] ; [ rewrite <- H ; constructor | tauto ].

+ decide (p s) ; [ apply in_app_iff in H ; destruct H as [H | H] | ] ; auto...

- induction 1 as [| s ys xs H H0 IH | s ys xs H IH] ; simpl ; auto.

× decide (p s) ; firstorder.

× assert (H1: ∃ ys', s::ys' = s::ys ∧ ys' el (slists p xs)) by firstorder.

rewrite <- in_map_iff in H1.

decide (p s) ; [ apply in_app_iff | ] ; auto.

Qed.

Lemma slist_id (X : Type) (xs : list X) (p : X → Prop) {pdec : ∀ x, dec (p x)} :

slist p xs xs.

Proof.

induction xs ; auto.

Qed.

Lemma slist_trans (X : Type) (xs ys zs : list X) (p : X → Prop) {pdec : ∀ x, dec (p x)} :

slist p zs ys → slist p ys xs → slist p zs xs.

Proof with (remember (s :: xs) as zs ; induction H2 ; [congruence | | inv Heqzs ] ; auto).

intros H1. revert xs.

induction H1 as [| s ys xs H H0 IH | s ys xs H IH] ; intros xs' H2 ; try now auto ; auto...

Qed.

Lemma slist_append (X : Type) (xs1 xs2 ys1 ys2 : list X) (p : X → Prop) {pdec : ∀ x, dec (p x)} :

slist p ys1 xs1 → slist p ys2 xs2 → slist p (ys1 ++ ys2) (xs1 ++ xs2).

Proof.

induction 1 ; simpl ; auto.

Qed.

Lemma slist_equiv_pred (X : Type) (xs ys : list X) (p : X → Prop) {pdec : ∀ x, dec (p x)} (p' : X → Prop) {pdec' : ∀ x, dec (p' x)}:

(∀ x, p x ↔ p' x) → slist p xs ys → slist p' xs ys.

Proof.

induction 2 ; auto.

constructor 2 ; firstorder.

Qed.

Lemma slist_inv (X : Type) (xs ys : list X) (p : X → Prop) {pdec : ∀ x, dec (p x)} :

slist p ys xs → (∀ s, s el ys → p s) → ∀ s, s el xs → p s.

Proof with (destruct E as [E | E] ; try rewrite <- E ; auto).

intros H0 H1 s E.

induction H0 ; auto...

Qed.

Lemma slist_split (X : Type) (xs ys : list X) (p : X → Prop) {pdec : ∀ x, dec (p x)} :

slist p ys xs → ∀ xs1 xs2, xs = xs1 ++ xs2 → ∃ ys1 ys2, slist p ys1 xs1 ∧ slist p ys2 xs2 ∧ ys = ys1 ++ ys2.

Proof with (repeat split ; auto ; try inv IH0 ; auto).

induction 1 as [ | s ys xs H H0 IH | s ys xs H IH] ; intros xs1 xs2 U.

- ∃ [], [].

symmetry in U.

apply app_eq_nil in U ; destruct U as [H1 U].

rewrite H1, U. repeat split ; auto.

- destruct xs1, xs2 ; simpl in U ; (try now inv U) ; injection U ; intros U0 U1 ; subst.

+ destruct (IH [] xs2 eq_refl) as [ys1 [ys2 [IH0 [IH1 IH2]]]]. ∃ ys1, ys2...

+ destruct (IH xs1 [] eq_refl) as [ys1 [ys2 [IH0 [IH1 IH2]]]]. ∃ ys1, ys2...

+ destruct (IH xs1 (x0 :: xs2) eq_refl) as [ys1 [ys2 [IH0 [IH1 IH2]]]]. ∃ ys1, ys2...

- destruct xs1, xs2 ; simpl in U ; (try now inv U) ; injection U ; intros U0 U1 ; subst.

+ destruct (IH [] xs2 eq_refl) as [ys1 [ys2 [IH0 [IH1 IH2]]]]. ∃ ys1, (x :: ys2)...

+ destruct (IH xs1 [] eq_refl) as [ys1 [ys2 [IH0 [IH1 IH2]]]]. ∃ (x :: ys1), ys2...

+ destruct (IH xs1 (x0 :: xs2) eq_refl) as [ys1 [ys2 [IH0 [IH1 IH2]]]]. ∃ (x :: ys1), ys2...

Qed.

Lemma slist_subsumes X (p : X → Prop) {D : ∀ x, dec (p x)} xs ys :

slist p xs ys → xs <<= ys.

Proof.

induction 1 ; auto.

Qed.

Lemma slist_length X (p : X → Prop) {D : ∀ x, dec (p x)} (xs ys : list X) :

slist p xs ys → |xs| ≤ |ys|.

Proof.

induction 1 ; simpl ; omega.

Qed.

Lemma slist_pred X (p p' : X → Prop) {D : ∀ x, dec (p' x)} (xs ys : list X) :

slist p' xs ys → (∀ y, y el ys → p y) → ∀ x, x el xs → p x.

Proof.

intros Ss P.

induction Ss ; intros x' E ; auto.

destruct E as [E | E] ; auto.

rewrite <- E. now apply P.

Qed.

Definition segment X (xs ys : list X) := ∃ xs1 xs2, xs = xs1 ++ ys ++ xs2.

Fixpoint segms X (D : eq_dec X) (xs : list X) :=

match xs with

[] ⇒ [ [] ]

| s :: xs ⇒

let

Ss :=segms D xs

in

map (cons s) (filter (fun ys ⇒ ∃ zs, xs = ys ++ zs) Ss) ++ Ss

end.

Arguments segms {X} {D} xs.

Lemma segment_nil X {D : eq_dec X} (xs : list X) :

segment xs [].

Proof.

∃ xs, []. now rewrite app_nil_r.

Qed.

Lemma segment_refl X {D : eq_dec X} (xs : list X) :

segment xs xs.

Proof.

∃ [], []. rewrite app_nil_r. auto.

Qed.

Lemma segment_trans X {D : eq_dec X} (xs ys zs : list X) :

segment ys zs → segment xs ys → segment xs zs.

Proof.

intros [w1 [w2 H0]] [ys1 [ys2 H1]].

∃ (ys1 ++ w1), (w2 ++ ys2). rewrite H1, H0.

now repeat rewrite <- app_assoc.

Qed.

Lemma segms_corr1 X {D : eq_dec X} (xs ys : list X) :

segment xs ys → ys el segms xs.

Proof.

revert ys.

induction xs as [| s xs IHxs] ; intros ys [ys1 [ys2 H]].

- simpl. symmetry in H.

apply app_eq_nil in H.

destruct H as [H0 H]. apply app_eq_nil in H.

destruct H as [H1 H2]. subst. auto.

- destruct ys1 as [| sys1 ys1] ; simpl in H.

+ destruct ys as [| sys ys] ; simpl in H.

{ simpl. apply in_or_app. right. apply IHxs. now apply segment_nil. }

{ injection H ; intros H0 H1 ; subst.

simpl. apply in_or_app. left. apply in_map_iff.

∃ ys. split ; auto. apply in_filter_iff. split.

- apply IHxs. ∃ [], ys2. auto.

- now (∃ ys2). }

+ injection H ; intros H0 H1 ; subst.

simpl. apply in_or_app. right. apply IHxs.

now (∃ ys1, ys2).

Qed.

Lemma segms_corr2 X {D : eq_dec X} (xs ys : list X) :

ys el segms xs → segment xs ys.

Proof.

intros H.

induction xs as [| s xs IHxs] ; simpl in H.

- destruct H as [H | H] ; [subst | tauto].

now (∃ [], []).

- apply in_app_iff in H.

destruct H as [H | H].

+ apply in_map_iff in H. destruct H as [x [H0 H1]].

apply in_filter_iff in H1. destruct H1 as [H1 [zs H2]].

rewrite <- H0, H2 in ×.

∃ [], zs. auto.

+ destruct (IHxs H) as [x [z IH]].

∃ (s :: x), z. rewrite IH. auto.

Qed.

Lemma segms_corr X {D : eq_dec X} (xs ys : list X) :

ys el segms xs ↔ segment xs ys.

Proof.

split ; intros Ss ; [eapply segms_corr2 | eapply segms_corr1] ; eauto.

Qed.

Fixpoint product X Y Z (f : X → Y → Z) (xs : list X) (ys : list Y) : list Z :=

match xs with

[] ⇒ []

| s :: xs ⇒ map (f s) ys ++ product f xs ys

end.

Lemma prod_corr1 X Y Z (f : X → Y → Z) (xs : list X) (ys : list Y) (z : Z) :

z el product f xs ys → ∃ sxs sys, f sxs sys = z ∧ sxs el xs ∧ sys el ys.

Proof.

intros H.

induction xs as [| s xs IHxs ] ; simpl in H ; try tauto.

apply in_app_iff in H.

destruct H as [H | H].

- apply in_map_iff in H.

destruct H as [x [H0 H1]].

∃ s, x. repeat split ; auto.

- destruct (IHxs H) as [sxs [sys [H0 [H1 H2]]]].

∃ sxs, sys. auto.

Qed.

Lemma prod_corr2 X Y Z (f : X → Y → Z) (xs : list X) (ys : list Y) (z : Z) :

(∃ sxs sys, f sxs sys = z ∧ sxs el xs ∧ sys el ys) → z el product f xs ys.

Proof.

intros [sxs [sys [H0 [H1 H2]]]].

induction xs as [| s xs IHxs ] ; try now inv H1.

simpl. apply in_app_iff.

destruct H1 as [H1 | H1].

- rewrite H1 in ×. left. apply in_map_iff. ∃ sys. auto.

- right. auto.

Qed.

Lemma prod_corr X Y Z (f : X → Y → Z) (xs : list X) (ys : list Y) (z : Z) :

z el product f xs ys ↔ ∃ sxs sys, f sxs sys = z ∧ sxs el xs ∧ sys el ys.

Proof.

split ; [apply prod_corr1 | apply prod_corr2].

Qed.

Fixpoint fsts X Y (xs : list (X × Y)) :=

match xs with

[] ⇒ []

| (x, y) :: xs ⇒ x :: fsts xs

end.

Lemma fsts_split X Y (xs ys : list (X × Y)) :

fsts (xs ++ ys) = fsts xs ++ fsts ys.

Proof.

induction xs as [| [s1 s2] xs IHxs] ; simpl ; auto.

now rewrite IHxs.

Qed.

Fixpoint snds X Y (xs : list (X × Y)) :=

match xs with

[] ⇒ []

| (x, y) :: xs ⇒ y :: snds xs

end.

Lemma snds_split X Y (xs ys : list (X × Y)) :

snds (xs ++ ys) = snds xs ++ snds ys.

Proof.

induction xs as [| [s1 s2] xs IHxs] ; simpl ; auto.

now rewrite IHxs.

Qed.

match xs with

[] ⇒ []

| (x, y) :: xs ⇒ x :: fsts xs

end.

Lemma fsts_split X Y (xs ys : list (X × Y)) :

fsts (xs ++ ys) = fsts xs ++ fsts ys.

Proof.

induction xs as [| [s1 s2] xs IHxs] ; simpl ; auto.

now rewrite IHxs.

Qed.

Fixpoint snds X Y (xs : list (X × Y)) :=

match xs with

[] ⇒ []

| (x, y) :: xs ⇒ y :: snds xs

end.

Lemma snds_split X Y (xs ys : list (X × Y)) :

snds (xs ++ ys) = snds xs ++ snds ys.

Proof.

induction xs as [| [s1 s2] xs IHxs] ; simpl ; auto.

now rewrite IHxs.

Qed.

Fixpoint concat X (xs : list (list X)) :=

match xs with

[] ⇒ []

| ys :: xs ⇒ ys ++ (concat xs)

end.

Lemma concat_split X (xs ys : list (list X)) :

concat (xs ++ ys) = concat xs ++ concat ys.

Proof.

induction xs ; simpl ; [| rewrite IHxs] ; auto using app_assoc.

Qed.

match xs with

[] ⇒ []

| ys :: xs ⇒ ys ++ (concat xs)

end.

Lemma concat_split X (xs ys : list (list X)) :

concat (xs ++ ys) = concat xs ++ concat ys.

Proof.

induction xs ; simpl ; [| rewrite IHxs] ; auto using app_assoc.

Qed.

Fixpoint substL X {D : eq_dec X} (xs : list X) (y : X) (ys : list X) :=

match xs with

[] ⇒ []

| x :: xs ⇒ if decision (x = y) then ys ++ substL xs y ys else x :: substL xs y ys

end.

Lemma substL_split X {D : eq_dec X} (xs1 xs2 : list X) (y : X) (ys : list X) :

substL (xs1 ++ xs2) y ys = substL xs1 y ys ++ substL xs2 y ys.

Proof.

induction xs1 as [| sxs1 xs1 IHxs1] ; simpl ; try (decide (sxs1 = y) ; rewrite IHxs1) ; auto using app_assoc.

Qed.

Lemma substL_skip X {D : eq_dec X} (xs : list X) (y : X) (ys : list X) :

¬ y el xs → substL xs y ys = xs.

Proof.

intros U.

induction xs as [| x xs IHxs] ; simpl in × ; auto.

decide (x = y) as [D0 | D0].

- exfalso. apply U ; auto.

- f_equal. apply IHxs.

intros H. apply U. auto.

Qed.

Lemma substL_length_unit X {D : eq_dec X} (xs : list X) (x x' : X) :

(|xs|) = | substL xs x [x'] |.

Proof.

induction xs as [| y xr IHxr] ; simpl ; try decide (y = x) ; simpl ; auto.

Qed.

Lemma substL_undo X {D : eq_dec X} (xs : list X) (x x' : X) :

¬ x' el xs → substL (substL xs x [x']) x' [x] = xs.

Proof.

intros H.

induction xs as [| y xr IHxr] ; simpl ; auto.

simpl. decide (y = x) as [D0 | D0] ; subst ; simpl.

- decide (x' = x') ; try tauto. f_equal. auto.

- decide (y = x') ; subst.

+ exfalso. now apply H.

+ f_equal. auto.

Qed.

match xs with

[] ⇒ []

| x :: xs ⇒ if decision (x = y) then ys ++ substL xs y ys else x :: substL xs y ys

end.

Lemma substL_split X {D : eq_dec X} (xs1 xs2 : list X) (y : X) (ys : list X) :

substL (xs1 ++ xs2) y ys = substL xs1 y ys ++ substL xs2 y ys.

Proof.

induction xs1 as [| sxs1 xs1 IHxs1] ; simpl ; try (decide (sxs1 = y) ; rewrite IHxs1) ; auto using app_assoc.

Qed.

Lemma substL_skip X {D : eq_dec X} (xs : list X) (y : X) (ys : list X) :

¬ y el xs → substL xs y ys = xs.

Proof.

intros U.

induction xs as [| x xs IHxs] ; simpl in × ; auto.

decide (x = y) as [D0 | D0].

- exfalso. apply U ; auto.

- f_equal. apply IHxs.

intros H. apply U. auto.

Qed.

Lemma substL_length_unit X {D : eq_dec X} (xs : list X) (x x' : X) :

(|xs|) = | substL xs x [x'] |.

Proof.

induction xs as [| y xr IHxr] ; simpl ; try decide (y = x) ; simpl ; auto.

Qed.

Lemma substL_undo X {D : eq_dec X} (xs : list X) (x x' : X) :

¬ x' el xs → substL (substL xs x [x']) x' [x] = xs.

Proof.

intros H.

induction xs as [| y xr IHxr] ; simpl ; auto.

simpl. decide (y = x) as [D0 | D0] ; subst ; simpl.

- decide (x' = x') ; try tauto. f_equal. auto.

- decide (y = x') ; subst.

+ exfalso. now apply H.

+ f_equal. auto.

Qed.