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.