Require Import Classical.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Notation set X := (X -> Prop).
Notation relation X := (X -> X -> Prop).
Notation "p '<<=' q" := (forall x, p x -> q x) (at level 70).
Notation "p '===' q" := (forall x, p x <-> q x) (at level 70).
Notation "p << q" := (p <<= q /\ ~ q === p) (at level 70).
Notation "p :|: q" := (fun x : _ => p x \/ q x) (at level 70).
Notation complement p := (fun x => ~ p x).
Notation set0 := (fun _ => False).
Notation set1 x := (fun z => z = x).
Notation setT := (fun _ => True).

Section Predicates.
  Variable (X : Type).
  Implicit Types (p q : set X) (F G : set X -> Prop).

  Definition inhab p := ex p.
  Definition single p := exists2 x, p x & forall y, p y -> y = x.
  Definition cmp p q := p <<= q \/ q <<= p.
  Definition linears F := forall p q, F p -> F q -> cmp p q.
  Definition Union F x := exists2 p, F p & p x.
  Definition Inter F x := forall p, F p -> p x.
  Definition unique p := forall x y, p x -> p y -> x = y.
  Definition setU1 p x := fun z => p z \/ z = x.
  Definition incl p q := p <<= q.

  Lemma sub_refl p : incl p p.
  Proof. firstorder. Qed.

  Lemma set_eq p q : p <<= q -> q <<= p -> p === q.
  Proof. firstorder. Qed.

  Lemma sub_linear F G : G <<= F -> linears F -> linears G.
  Proof. firstorder. Qed.

  Lemma sub_trans p q r : p <<= q -> q <<= r -> p <<= r.
  Proof. firstorder. Qed.

  Lemma eq_sub p q : p = q -> p === q.
  Proof. intros; subst; firstorder. Qed.

  Lemma sub_union F p : F p -> p <<= Union F.
  Proof. firstorder. Qed.

End Predicates.

Definition least X (R : relation X) x p := p x /\ forall y, p y -> R x y.

Section OrderOn.
  Variables (X : Type) (p : set X) (R : relation X).

  Definition refl_on := forall x, p x -> R x x.

  Definition trans_on :=
    forall x y z, p x -> p y -> p z -> R x y -> R y z -> R x z.

  Definition anti_on :=
    forall x y, p x -> p y -> R x y -> R y x -> x = y.

  Definition linear_on :=
    forall x y, p x -> p y -> R x y \/ R y x.

  Definition ELE_on :=
    forall q : set X, q <<= p -> inhab q -> exists x, least R x q.

  Lemma ELE_linear : ELE_on -> linear_on.
  Proof.
    intros A x y px py.
    destruct (A (fun z => z = x \/ z = y)) as [z [[B|B] C]].
    - intuition; subst; firstorder.
    - exists x; tauto.
    - subst; eauto.
    - subst; eauto.
  Qed.

  Fact linear_refl : linear_on -> refl_on.
  Proof. intros A x px. now destruct (A x x). Qed.

  Definition po_on := refl_on /\ trans_on /\ anti_on.

  Definition lo_on := po_on /\ linear_on.

  Definition wo_on := po_on /\ ELE_on.

End OrderOn.

Lemma po_sub (X : Type) (R : relation X) (p q : set X) :
  p <<= q -> po_on q R -> po_on p R.
Proof. firstorder. Qed.

Lemma wo_sub (X : Type) (R : relation X) (p q : set X) :
  p <<= q -> wo_on q R -> wo_on p R.
Proof. firstorder. Qed.

Definition injective X Y (f : X -> Y) :=
  forall x y, f x = f y -> x = y.

Definition into X Y p q (f : X -> Y) := forall x, p x -> q (f x).

Lemma transfer_on X Y (f : X -> Y) (p : set X) (q : set Y) (R : relation Y) :
  injective f -> into p q f -> wo_on q R -> wo_on p (fun x y => R (f x) (f y)).
Proof.
  intros inj_f into_f (po_onR & eleR).
  repeat split; try solve [firstorder].
  intros F in_p [x Fx].
    pose (F' y := exists2 x, F x & f x = y).
    destruct (eleR F') as [z [Fz Lz]].
    + intros y [z z1 z2]. subst. auto.
    + now exists (f x); exists x.
    + destruct Fz. exists x0. split; trivial.
      intros y py. rewrite H0. apply Lz.
      now exists y.
Qed.

Section Chains.
  Variables (X : Type) (R : relation X).
  Definition chain p := linear_on p R.

  Lemma chainU F :
    linears F -> (forall p, F p -> chain p) -> chain (Union F).
  Proof.
    intros lin_F chain_F x y [p Fp px] [q Fq qx].
    destruct (lin_F _ _ Fp Fq).
    + unfold chain in chain_F. apply (chain_F q); firstorder.
    + unfold chain in chain_F. apply (chain_F p); firstorder.
  Qed.
End Chains.

Record ExtType :=
  { ext_sort :> Type ;
    set_ext (p q : set ext_sort) : p === q -> p = q }.

Section ExtTypeFacts.
  Variables (X : ExtType).
  Implicit Types (p q : set X) (x : X) (F G : set (set X)).

  Lemma set_eqx p q : p <<= q -> q <<= p -> p = q.
  Proof. intros A B. now apply set_ext,set_eq. Qed.

  Lemma unique_eq1 p x : unique p -> p x -> p = set1 x.
  Proof. intros u_p px. now apply set_ext; intuition; subst. Qed.

  Lemma setU0 p : p :|: set0 = p.
  Proof. apply set_ext; firstorder. Qed.

  Lemma inter_eq F G : F === G -> Inter F = Inter G.
  Proof. intros H. apply set_ext. firstorder. Qed.

  Lemma inter1 p : Inter (set1 p) = p.
  Proof. apply set_ext, set_eq;[firstorder|intros x px y E]. now subst. Qed.

  Lemma inter_full F : inhab F -> (forall x, Inter F x) -> F === set1 setT.
  Proof.
    intros inh_F H. apply set_eq.
    - intros p Fp. apply set_ext. firstorder.
    - intros p E. subst. destruct inh_F as [p Fp].
      destruct (classic (exists x, ~ p x)) as [[x npx]|A].
      + firstorder.
      + cutrewrite (setT = p);[assumption|].
        apply set_ext. firstorder.
  Qed.

  Lemma po_incl (F : set (set X)) : po_on F (@incl X).
  Proof.
    repeat split; try firstorder.
    intros p q ? ? ? ?. now apply set_ext,set_eq.
  Qed.

End ExtTypeFacts.

Record ExtChoiceType :=
  { sort :> ExtType ;
    gamma : set sort -> set sort ;
    gammaP1 (p : set sort) : gamma p <<= p ;
    gammaP2 (p : set sort) : inhab p -> single (gamma p) }.

Section ExtChoiceFacts.
  Variable (X : ExtChoiceType).
  Implicit Types (p q : set X).

  Lemma inhab_gamma p : inhab p -> inhab (gamma p).
  Proof. intros H. apply gammaP2 in H. firstorder. Qed.

  Lemma gamma0Vx p :
    gamma p = set0 \/ exists2 x, p x & gamma p = set1 x.
  Proof.
    destruct (classic (inhab p)).
    - right. destruct (gammaP2 H). exists x. now apply gammaP1.
      apply set_ext; intuition. now subst.
    - left. apply set_ext. intuition. apply H. exists x. now apply gammaP1.
  Qed.

  Lemma gamma_unique p : unique (gamma p).
  Proof.
    intros x y gpx gpy. edestruct (gammaP2 (ex_intro _ _ (gammaP1 gpy))) as [z _ e].
    now rewrite (e x gpx), (e y gpy).
  Qed.
End ExtChoiceFacts.