# Library IZF.IZF_select

Require Import IZF_logic.
Require Import IZF_base.

Definition PRED := X : Typ1, Rel X X Prop.

Definition Compat (P : PRED) : Prop :=
(X : Typ1) (A : Rel X) (a : X) (Y : Typ1) (B : Rel Y) (b : Y),
EQV X A a Y B b P X A a P Y B b.

Definition SELECT (X : Typ1) (A : Rel X) (a : X) (P : PRED) :
Rel (opt X) :=
fun z' z : opt X
E : Prop,
( x x' : X,
eq (opt X) z (some X x) eq (opt X) z' (some X x') A x' x E)
( x' : X,
eq (opt X) z' (some X x')
eq (opt X) z (none X) A x' a P X A x' E) E.

Lemma SELECT_in :
(X : Typ1) (A : Rel X) (a : X) (P : PRED) (x x' : X),
A x' x SELECT X A a P (some X x') (some X x).

Proof
fun X A a P x x' H E e _
e x x' (eq_refl (opt X) (some X x)) (eq_refl (opt X) (some X x')) H.

Lemma SELECT_rt :
(X : Typ1) (A : Rel X) (a : X) (P : PRED) (x' : X),
A x' a P X A x' SELECT X A a P (some X x') (none X).

Proof
fun X A a P x' H1 H2 E _ e
e x' (eq_refl (opt X) (some X x')) (eq_refl (opt X) (none X)) H1 H2.

Lemma SELECT_deloc :
(X : Typ1) (A : Rel X) (a : X) (P : PRED),
deloc X A (opt X) (SELECT X A a P) (some X).

Proof.
intros X A a P; unfold deloc in |- *; apply and_intro.
exact (SELECT_in X A a P).
intros x z' H; apply H; clear H.
intros x0 x' H1 H2 H3; apply ex2_intro with x'.
apply (eq_sym _ _ _ (eq_some_some X x x0 H1)); assumption.
assumption.
intros x' H1 H2 H3 H4; apply (eq_some_none X x H2).
Qed.

Lemma SELECT_eqv :
(X : Typ1) (A : Rel X) (a : X) (P : PRED) (x : X),
EQV X A x (opt X) (SELECT X A a P) (some X x).

Proof.
intros X A a P x; apply EQV_deloc; apply SELECT_deloc.
Qed.

Lemma selection_intro :
(X : Typ1) (A : Rel X) (a : X) (P : PRED),
Compat P
(Y : Typ1) (B : Rel Y) (b : Y),
ELT Y B b X A a P Y B b ELT Y B b (opt X) (SELECT X A a P) (none X).

Proof.
intros X A a P H1 Y B b H H2; apply H; clear H; intros x' H3 H4.
apply ELT_intro with (some X x').
apply SELECT_rt; [ assumption | exact (H1 _ _ _ _ _ _ H4 H2) ].
apply EQV_trans with X A x'; [ assumption | apply SELECT_eqv ].
Qed.

Lemma selection_elim :
(X : Typ1) (A : Rel X) (a : X) (P : PRED),
Compat P
(Y : Typ1) (B : Rel Y) (b : Y),
ELT Y B b (opt X) (SELECT X A a P) (none X)
and (ELT Y B b X A a) (P Y B b).

Proof.
intros X A a P H1 Y B b H; apply H; clear H.
intros z' H H2; apply H; clear H.
intros x x' H3 H4 H5; apply (eq_none_some X x H3).
intros x' H3 H4 H5 H6; apply and_intro.
apply ELT_intro with x'. assumption.
apply EQV_trans with (opt X) (SELECT X A a P) z'. assumption.
apply (eq_sym _ _ _ H3); apply EQV_sym; apply SELECT_eqv.
apply H1 with X A x'.
apply EQV_trans with (opt X) (SELECT X A a P) z'.
apply (eq_sym _ _ _ H3); apply SELECT_eqv.
apply EQV_sym; assumption. assumption.
Qed.

Theorem selection :
(X : Typ1) (A : Rel X) (a : X) (P : PRED),
Compat P
(Y : Typ1) (B : Rel Y) (b : Y),
iff (ELT Y B b (opt X) (SELECT X A a P) (none X))
(and (ELT Y B b X A a) (P Y B b)).

Proof.
intros X A a P H1 Y B b; unfold iff in |- *; apply and_intro.
intro; apply selection_elim; assumption.
intro H; apply H; intros; apply selection_intro; assumption.
Qed.