# Library Kildall.lists.pred_list

Section pred_list.

Require Export Peano_dec.
Require Export relations.
Require Export List.

Variable A : Set.
Variable P : A->Prop.
Hypothesis eq_A_dec : forall (a a' : A), {a = a'} + {a <> a'}.

Inductive pred_list : Set :=
| pred_nil : pred_list
| pred_cons : forall (a:A), (P a)->pred_list->pred_list.

Fixpoint pred_list_add_element (l : pred_list) (a:A) {struct l} :
(P a)->(pred_list):=
match l return (P a)->(pred_list) with
| (pred_nil) => fun C : (P a) => (pred_cons a C pred_nil)
| (pred_cons h C t) =>
match (eq_A_dec a h) with
| (left _) => fun Ca : P a=>pred_cons h C t
| (right _) => fun Ca : P a=>
(pred_cons h C (pred_list_add_element t a Ca))
end
end.

Fixpoint pred_list_belong (l : pred_list) (a : A) {struct l} : Prop :=
match l with
| (pred_nil) => False
| (pred_cons h C t) => a=h \/ pred_list_belong t a
end.

Notation "a 'INp' l" := (pred_list_belong l a) (at level 50).

Fixpoint pred_list_remove (l : pred_list) (a : A) {struct l} : pred_list :=
match l with
| pred_nil => pred_nil
| pred_cons h C t =>
match (eq_A_dec a h) with
| left _ => t
| right _ => pred_cons h C (pred_list_remove t a)
end
end.

Notation "l '\' a" := (pred_list_remove l a) (at level 50).

Fixpoint pred_length (l : pred_list) {struct l} : nat :=
match l with
| pred_nil => 0
| pred_cons _ _ t => S (pred_length t)
end.

Definition lt_pred_length (l l' : pred_list) : Prop :=
pred_length l < pred_length l'.

Inductive pred_pointwise (r:relation A): pred_list -> pred_list -> Prop :=
| pred_pointwise_nil : pred_pointwise r pred_nil pred_nil
| pred_pointwise_cons : forall (a a' : A) (C : P a) (C' : P a') (l l' : pred_list),
(r a a')->pred_pointwise r l l'->pred_pointwise r (pred_cons a C l) (pred_cons a' C' l').

Fixpoint pred_list_to_list (l : pred_list) : list A :=
match l with
| pred_nil => nil
| pred_cons h C t => h :: (pred_list_to_list t)
end.

Fact list_to_pred_list_convert_hyp : forall (h : A) (t : list A)
(H : forall (a:A), In a (h::t) -> P a),
forall (a : A), In a t -> P a.
Proof.
intros; apply H; trivial; try right; trivial.
Qed.

Fixpoint list_to_pred_list (l : list A) : (forall (a:A), In a l -> P a) -> pred_list :=
match l return ((forall (a:A), In a l -> P a) -> pred_list) with
| nil => fun (H : forall (a:A), In a nil -> P a) => pred_nil
| h :: t => fun (H : forall (a:A), In a (h::t) -> P a) =>
pred_cons h (H h (in_eq h t)) (list_to_pred_list t (list_to_pred_list_convert_hyp h t H))
end.

Lemma list_to_pred_list_to_list : forall (l : list A) (H : forall (a : A), In a l -> P a),
pred_list_to_list (list_to_pred_list l H) = l.
Proof.
induction l; simpl.
trivial.
intro H.
rewrite (IHl (list_to_pred_list_convert_hyp a l H)).
trivial.
Qed.

Lemma list_to_pred_list_length : forall (l : list A) (H : forall (a : A), In a l -> P a),
pred_length (list_to_pred_list l H) = length l.
Proof.
induction l; simpl.
trivial.
intro H.
apply eq_S.
apply IHl.
Qed.

Lemma pred_list_to_list_length : forall (l : pred_list),
length (pred_list_to_list l) = pred_length l.
Proof.
induction l; simpl.
trivial.
apply eq_S; apply IHl.
Qed.

Lemma pred_list_to_list_belong : forall (l : pred_list) (a : A),
a INp l -> In a (pred_list_to_list l).
Proof.
induction l as [ | h C t IHl] ; intro a; simpl.
trivial.
intro H; elim H; clear H; intro H.
left; symmetry; assumption.
right; apply IHl; assumption.
Qed.

Lemma belong_pred_list_to_list : forall (l : pred_list) (a : A),
In a (pred_list_to_list l) -> a INp l .
Proof.
induction l as [ | h C t IHl]; intro a; simpl.
trivial.
intro H; elim H; clear H; intro H.
left; symmetry; assumption.
right; apply IHl; assumption.
Qed.

Lemma list_to_pred_list_belong : forall (l : list A)
(H : forall (a : A), In a l -> P a) (a : A),
In a l -> a INp (list_to_pred_list l H).
Proof.
induction l as [ | h t IHl]; intros H a; simpl.
trivial.
intro H'; elim H'; clear H'; intro H'.
left; symmetry; assumption.
right; apply IHl; assumption.
Qed.

Lemma belong_list_to_pred_list : forall (l : list A)
(H : forall (a : A), In a l -> P a) (a : A),
a INp (list_to_pred_list l H) -> In a l.
Proof.
induction l as [ | h t IHl]; intros H a; simpl.
trivial.
intro H'; elim H'; clear H'; intro H'.
left; symmetry; assumption.
right; apply (IHl (list_to_pred_list_convert_hyp h t H)); assumption.
Qed.

Lemma pred_list_belong_remove : forall (l : pred_list) (a a' : A),
a INp l -> a<>a' -> a INp (l \ a').
Proof.
induction l as [ | h C t IHl]; simpl; intros a a' a_in_l a_neq_a'.
trivial.
elim (eq_A_dec a' h); intro case_a'_h.
elim a_in_l; clear a_in_l; intro a_in_l; trivial.
elim a_neq_a'; subst a; symmetry; assumption.
elim a_in_l; clear a_in_l; intro a_in_l; trivial.
left; assumption.
right; apply IHl; assumption.
Qed.

Lemma pred_list_belong_dec : forall (l : pred_list) (a : A),
{a INp l} + {~ (a INp l)}.
Proof.
intros l a.
induction l as [ | h C t IHl].
simpl; right.
unfold not; trivial.
simpl.
elim (eq_A_dec a h); intro comp.
left; left; assumption.
case IHl; intro comp'.
left; right; assumption.
right.
intro H.
apply comp'.
elim H.
intro H'; elim (comp H').
trivial.
Qed.

Lemma pred_list_get_witness : forall (l : pred_list) (a : A),
a INp l -> P a.
Proof.
induction l as [ | h C t IHl].
simpl.
intros a H; inversion H.
intros a H.
simpl in H.
elim H.
intro H'.
rewrite H'; assumption.
exact (IHl a).
Qed.

Lemma pred_list_belong_add : forall (l : pred_list) (a a' : A) (C : P a),
a' INp l-> a' INp (pred_list_add_element l a C).
Proof.
induction l as [ | h C t IHl]; simpl; intros a a' Ca H.
inversion H.
elim (eq_A_dec a h); intro comp_a_h.
simpl; assumption.
simpl; elim H; clear H; intro H.
left; assumption.
right.
apply IHl.
assumption.
Qed.

Lemma pred_list_belong_rem : forall (l : pred_list) (a a' : A) (C : P a),
a' INp (pred_list_add_element l a C) -> a<>a' -> a' INp l.
Proof.
induction l as [ | h C t IHl]; simpl; intros a a' Ca.
intros a'_in_la a_neq_a'; elim a'_in_la; auto.
elim (eq_A_dec a h); intro comp_a_h.
intros a'_in_la a_neq_a'; elim a'_in_la; intro H; [left | right]; trivial.
intros a'_in_la a_neq_a'; elim a'_in_la.
left; trivial.
right; apply IHl with a Ca; trivial.
Qed.

Lemma pred_list_add_already_there : forall (l : pred_list) (a : A) (C C' : P a),
Proof.
induction l as [ | h C t IHl]; simpl; intros a Ca Ca'.
elim (eq_A_dec a a); intro comp; [simpl | elim comp]; trivial.
elim (eq_A_dec a h); intro comp_a_h.
subst h; simpl; elim (eq_A_dec a a); intro comp; [simpl | elim comp]; trivial.
simpl; elim (eq_A_dec h a); intro comp_h_a.
subst; elim comp_a_h; trivial.
elim (eq_A_dec a h); intro comp.
rewrite (IHl a Ca Ca'); trivial.
Qed.

Lemma pred_list_belong_added : forall (l : pred_list) (a : A) (C : P a),
a INp (pred_list_add_element l a C).
Proof.
induction l as [ | h C t IHl]; simpl.
left; trivial.
intros a Ca; elim (eq_A_dec a h); intro comp; simpl.
left; trivial.
right; apply IHl.
Qed.

forall (l : pred_list) (a' a'' : A) (C' : P a') (C'' : P a''),
Proof.
induction l; intros a' a'' C' C''; simpl.
elim (eq_A_dec a' a''); intro comp.
simpl.
elim (eq_A_dec a'' a''); intro comp'.
trivial.
elim comp'; trivial.
simpl.
elim (eq_A_dec a'' a''); intro comp'.
trivial.
elim comp'; trivial.
elim (eq_A_dec a'' a); intro comp.
simpl.
elim (eq_A_dec a' a); intro comp'; simpl.
elim (eq_A_dec a'' a); intro comp''; [trivial | contradiction].
elim (eq_A_dec a'' a); intro comp''; [trivial | contradiction].
simpl.
elim (eq_A_dec a' a); intro comp'; simpl.
elim (eq_A_dec a'' a); intro comp''.
trivial.
elim (eq_A_dec a'' a); intro comp''; [contradiction | simpl].
rewrite (IHl a' a'' C' C''); trivial.
Qed.

Lemma list_from_pred_convertion : forall (l : list A) (dl : pred_list),
l = pred_list_to_list dl -> (forall (a : A), In a l -> P a).
Proof.
intros l dl; generalize l; clear l; induction dl; simpl; intros l Heq e Hin.
subst l; inversion Hin.
subst l; elim Hin; clear Hin; intro Hin.
subst e; assumption.
apply (IHdl (pred_list_to_list dl)); trivial.
Qed.

End pred_list.

Implicit Arguments pred_nil [A].
Implicit Arguments pred_cons [A].
Implicit Arguments pred_list_belong [A P].
Implicit Arguments pred_list_to_list [A P].
Implicit Arguments list_to_pred_list [A P].
Implicit Arguments pred_list_belong_dec [A P].
Implicit Arguments pred_list_get_witness [A P].
Implicit Arguments pred_list_belong_rem [A P].
Implicit Arguments pred_list_remove [A P].
Implicit Arguments pred_length [A P].
Implicit Arguments lt_pred_length [A P].

Notation "a 'INp' l" := (pred_list_belong l a) (at level 50).

Notation "l '\' a" := (pred_list_remove l a) (at level 50).

Section pred_list_equivalence.

Variable A : Set.

Definition pred_list_equiv (P Q : A->Prop) (l : pred_list A P) (l' : pred_list A Q) : Prop :=
pred_list_to_list l = pred_list_to_list l'.

Notation "l '=p=' m" := (pred_list_equiv _ _ l m) (at level 50).

Lemma pred_list_equiv_refl : forall (P : A-> Prop) (l : pred_list A P), l =p= l.
Proof.
unfold pred_list_equiv; trivial.
Qed.

Lemma pred_list_equiv_trans : forall (P Q R : A->Prop)
(lp : pred_list A P) (lq : pred_list A Q) (lr : pred_list A R),
lp =p= lq -> lq =p= lr -> lp =p= lr.
Proof.
unfold pred_list_equiv; intros P Q R lp lq lr Hpq Hqr.
rewrite Hpq; assumption.
Qed.

Lemma pred_list_equiv_sym : forall (P Q : A->Prop) (lp : pred_list A P) (lq : pred_list A Q),
lp =p= lq -> lq =p= lp.
Proof.
unfold pred_list_equiv; intros; symmetry; assumption.
Qed.

Lemma pred_list_equiv_split : forall (P Q : A->Prop) (a a' : A)
(lp : pred_list A P) (lq : pred_list A Q) (C : P a) (C' : Q a'),
(pred_cons P a C lp) =p= (pred_cons Q a' C' lq) -> a = a' /\ lp =p= lq.
Proof.
intros P Q a a' lp lq C C'.
unfold pred_list_equiv.
simpl; intro H.
inversion H.
split; trivial.
Qed.

Lemma pred_list_split_equiv : forall (P Q : A->Prop) (a a' : A)
(lp : pred_list A P) (lq : pred_list A Q) (C : P a) (C' : Q a'),
a = a' /\ (lp =p= lq) -> (pred_cons P a C lp) =p= (pred_cons Q a' C' lq).
Proof.
intros P Q a a' lp lq C C'.
unfold pred_list_equiv.
simpl; intro H.
inversion_clear H as [H1 H2].
rewrite H1; rewrite H2; trivial.
Qed.

Lemma pred_list_equiv_belong : forall (P Q : A->Prop) (a : A)
(lp : pred_list A P) (lq : pred_list A Q),
lp =p= lq -> a INp lp -> a INp lq.
Proof.
intros P Q a l l' Heq Hinl.
cut (In a (pred_list_to_list l')).
apply belong_pred_list_to_list.
unfold pred_list_equiv in Heq.
rewrite <- Heq.
apply pred_list_to_list_belong.
assumption.
Qed.

End pred_list_equivalence.

Implicit Arguments pred_list_equiv [A P Q].
Implicit Arguments pred_list_equiv_refl [A P].
Implicit Arguments pred_list_equiv_trans [A P Q R].
Implicit Arguments pred_list_equiv_sym [A P Q].
Implicit Arguments pred_list_equiv_split [A P Q].
Implicit Arguments pred_list_split_equiv [A P Q].
Implicit Arguments pred_list_equiv_belong [A P Q].

Notation "l '=p=' m" := (pred_list_equiv l m) (at level 50).

Section pred_list_convertion.

Variable A : Set.
Variables P Q : A->Prop.

Hypothesis eq_A_dec : forall (a a' : A), {a=a'} + {a<>a'}.

Lemma hyp_belong_convert : forall (l : pred_list A P)
(H : forall (a : A), a INp l -> Q a) (a : A),
In a (pred_list_to_list l) -> Q a.
Proof.
intros l H a Hin.
apply (H a).
induction l as [ | h C t IHl]; simpl; trivial.
elim Hin; [left | right].
symmetry; assumption.
apply IHl.
intros a' a'_in_t; apply (H a').
right; assumption.
assumption.
Qed.

Definition pred_list_convert (l : pred_list A P)
(H : forall (a : A), a INp l -> Q a) : pred_list A Q :=
list_to_pred_list (pred_list_to_list l) (hyp_belong_convert l H).

Lemma pred_list_convert_equiv : forall (l : pred_list A P)
(H : forall (a : A), a INp l -> Q a),
l =p= (pred_list_convert l H).
Proof.
unfold pred_list_equiv; unfold pred_list_convert.
intros l H.
rewrite (list_to_pred_list_to_list A Q (pred_list_to_list l) (hyp_belong_convert l H)); trivial.
Qed.

Lemma pred_list_convert_length : forall (l : pred_list A P)
(H : forall (a : A), a INp l -> Q a),
pred_length l = pred_length (pred_list_convert l H).
Proof.
unfold pred_list_equiv; unfold pred_list_convert.
intros l H.
transitivity (length (pred_list_to_list l)).
symmetry; apply pred_list_to_list_length.
symmetry; apply list_to_pred_list_length.
Qed.

Lemma pred_list_belong_convert : forall (a :A) (l : pred_list A P)
(H : forall (a : A), a INp l -> Q a),
a INp l -> a INp (pred_list_convert l H).
Proof.
unfold pred_list_convert.
intros a l H Hbelong.
cut (In a (pred_list_to_list l)).
apply list_to_pred_list_belong.
apply pred_list_to_list_belong.
assumption.
Qed.

Lemma pred_list_convert_belong : forall (a : A) (l : pred_list A P)
(H : forall (a : A), a INp l -> Q a),
a INp (pred_list_convert l H) -> a INp l.
Proof.
unfold pred_list_convert.
intros a l H Hbelong.
cut (In a (pred_list_to_list l)).
apply belong_pred_list_to_list.
apply (belong_list_to_pred_list A Q (pred_list_to_list l) (hyp_belong_convert l H)).
assumption.
Qed.

End pred_list_convertion.

Implicit Arguments pred_list_convert [A P Q].
Implicit Arguments pred_list_convert_equiv [A P Q].
Implicit Arguments pred_list_convert_length [A P Q].
Implicit Arguments pred_list_belong_convert [A P Q].
Implicit Arguments pred_list_convert_belong [A P Q].