(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


Require Import IZF_logic.
Require Import IZF_base.

Definition PRED := forall X : Typ1, Rel X -> X -> Prop.

Definition Compat (P : PRED) : Prop :=
  forall (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 =>
  forall E : Prop,
  (forall x x' : X,
   eq (opt X) z (some X x) -> eq (opt X) z' (some X x') -> A x' x -> E) ->
  (forall 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 :
 forall (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 :
 forall (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 :
 forall (X : Typ1) (A : Rel X) (a : X) (P : PRED),
 deloc X A (opt X) (SELECT X A a P) (some X).

Proof.
(* Goal: forall (X : Typ1) (A : Rel X) (a : X) (P : PRED), deloc X A (opt X) (SELECT X A a P) (some X) *)
intros X A a P; unfold deloc in |- *; apply and_intro.
(* Deloc 1 *)
(* Goal: forall (x x' : X) (_ : A x' x), SELECT X A a P (some X x') (some X x) *)
(* Goal: forall (x : X) (y' : opt X) (_ : SELECT X A a P y' (some X x)), ex2 X (fun x' : X => A x' x) (fun x' : X => eq (opt X) y' (some X x')) *)
exact (SELECT_in X A a P).
(* Deloc 2 (case distinction *)
(* Goal: forall (x : X) (y' : opt X) (_ : SELECT X A a P y' (some X x)), ex2 X (fun x' : X => A x' x) (fun x' : X => eq (opt X) y' (some X x')) *)
intros x z' H; apply H; clear H.
(* Deloc 2, case 1 *)
(* Goal: forall (x0 x' : X) (_ : eq (opt X) (some X x) (some X x0)) (_ : eq (opt X) z' (some X x')) (_ : A x' x0), ex2 X (fun x'0 : X => A x'0 x) (fun x'0 : X => eq (opt X) z' (some X x'0)) *)
(* Goal: forall (x' : X) (_ : eq (opt X) z' (some X x')) (_ : eq (opt X) (some X x) (none X)) (_ : A x' a) (_ : P X A x'), ex2 X (fun x'0 : X => A x'0 x) (fun x'0 : X => eq (opt X) z' (some X x'0)) *)
intros x0 x' H1 H2 H3; apply ex2_intro with x'.
(* Goal: A x' x *)
(* Goal: eq (opt X) z' (some X x') *)
(* Goal: forall (x' : X) (_ : eq (opt X) z' (some X x')) (_ : eq (opt X) (some X x) (none X)) (_ : A x' a) (_ : P X A x'), ex2 X (fun x'0 : X => A x'0 x) (fun x'0 : X => eq (opt X) z' (some X x'0)) *)
apply (eq_sym _ _ _ (eq_some_some X x x0 H1)); assumption.
(* Goal: P X A x' *)
assumption.
(* Deloc 2, case 2 (absurd) *)
(* Goal: forall (x' : X) (_ : eq (opt X) z' (some X x')) (_ : eq (opt X) (some X x) (none X)) (_ : A x' a) (_ : P X A x'), ex2 X (fun x'0 : X => A x'0 x) (fun x'0 : X => eq (opt X) z' (some X x'0)) *)
intros x' H1 H2 H3 H4; apply (eq_some_none X x H2).
Qed.

Lemma SELECT_eqv :
 forall (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.
(* Goal: forall (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) *)
intros X A a P x; apply EQV_deloc; apply SELECT_deloc.
Qed.

Lemma selection_intro :
 forall (X : Typ1) (A : Rel X) (a : X) (P : PRED),
 Compat P ->
 forall (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.
(* Goal: forall (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) *)
intros X A a P H1 Y B b H H2; apply H; clear H; intros x' H3 H4.
(* Goal: ELT Y B b (opt X) (SELECT X A a P) (none X) *)
apply ELT_intro with (some X x').
(* Goal: SELECT X A a P (some X x') (none X) *)
(* Goal: EQV Y B b (opt X) (SELECT X A a P) (some X x') *)
apply SELECT_rt; [ assumption | exact (H1 _ _ _ _ _ _ H4 H2) ].
(* Goal: EQV Y B b (opt X) (SELECT X A a P) (some X x') *)
apply EQV_trans with X A x'; [ assumption | apply SELECT_eqv ].
Qed.

Lemma selection_elim :
 forall (X : Typ1) (A : Rel X) (a : X) (P : PRED),
 Compat P ->
 forall (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.
(* Goal: forall (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) *)
intros X A a P H1 Y B b H; apply H; clear H.
(* Goal: forall (b' : opt X) (_ : SELECT X A a P b' (none X)) (_ : EQV Y B b (opt X) (SELECT X A a P) b'), and (ELT Y B b X A a) (P Y B b) *)
intros z' H H2; apply H; clear H.
(* Case 1 (absurd) *)
(* Goal: forall (x x' : X) (_ : eq (opt X) (none X) (some X x)) (_ : eq (opt X) z' (some X x')) (_ : A x' x), and (ELT Y B b X A a) (P Y B b) *)
(* Goal: forall (x' : X) (_ : eq (opt X) z' (some X x')) (_ : eq (opt X) (none X) (none X)) (_ : A x' a) (_ : P X A x'), and (ELT Y B b X A a) (P Y B b) *)
intros x x' H3 H4 H5; apply (eq_none_some X x H3).
(* Case 2 *)
(* Goal: forall (x' : X) (_ : eq (opt X) z' (some X x')) (_ : eq (opt X) (none X) (none X)) (_ : A x' a) (_ : P X A x'), and (ELT Y B b X A a) (P Y B b) *)
intros x' H3 H4 H5 H6; apply and_intro.
(* Case 2, first conclusion *)
(* Goal: P X A x' *)
apply ELT_intro with x'. assumption.
(* Goal: P X A x' *)
apply EQV_trans with (opt X) (SELECT X A a P) z'. assumption.
(* Goal: EQV (opt X) (SELECT X A a P) z' X A x' *)
(* Goal: P Y B b *)
apply (eq_sym _ _ _ H3); apply EQV_sym; apply SELECT_eqv.
(* Case 2, second conclusion *)
(* Goal: P Y B b *)
apply H1 with X A x'.
(* Goal: EQV X A x' Y B b *)
(* Goal: P X A x' *)
apply EQV_trans with (opt X) (SELECT X A a P) z'.
(* Goal: EQV X A x' (opt X) (SELECT X A a P) z' *)
(* Goal: EQV (opt X) (SELECT X A a P) z' Y B b *)
(* Goal: P X A x' *)
apply (eq_sym _ _ _ H3); apply SELECT_eqv.
(* Goal: P X A x' *)
apply EQV_sym; assumption. assumption.
Qed.

Theorem selection :
 forall (X : Typ1) (A : Rel X) (a : X) (P : PRED),
 Compat P ->
 forall (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.
(* Goal: forall (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)) *)
intros X A a P H1 Y B b; unfold iff in |- *; apply and_intro.
(* Goal: P X A x' *)
intro; apply selection_elim; assumption.
(* Goal: P X A x' *)
intro H; apply H; intros; apply selection_intro; assumption.
Qed.