Global Set Implicit Arguments.
Global Unset Strict Implicit.

Require Export Setoid Morphisms.

Axiom PE : forall P Q, P <-> Q -> P = Q.
Axiom FE : forall X Y (f g : X -> Y), (forall x, f x = g x) -> f = g.
Axiom XM : forall P, P \/ ~ P.

Lemma predicate_ext X (p q : X -> Prop) :
  (forall x, p x <-> q x) -> p = q.
Proof.
  intros H. apply FE. intros x. apply PE, H.
Qed.

Lemma PI (P : Prop) (H H' : P) :
  H = H'.
Proof.
  assert (P = True) as ->.
  - apply PE. tauto.
  - destruct H, H'. reflexivity.
Qed.

Definition pi1 := proj1_sig.
Definition pi2 := proj2_sig.

Lemma exist_eq X (p : X -> Prop) (x y : X) Hx Hy :
  x = y -> exist p x Hx = exist p y Hy.
Proof.
  intros ->. now rewrite (PI Hx Hy).
Qed.

Lemma exist_pi1 X (p : X -> Prop) (x y : sig p) :
  pi1 x = pi1 y -> x = y.
Proof.
  destruct x as [x Hx], y as [y Hy]. apply exist_eq.
Qed.

Lemma exist_eta X (p : X -> Prop) (x : sig p) :
  exist p (pi1 x) (pi2 x) = x.
Proof.
  now destruct x.
Qed.

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

Definition inject X Y :=
  exists (f : X -> Y), injective f.

Definition total_rel (X Y : Type) (R : X -> Y -> Prop) :=
  forall x, exists y, R x y.

Definition surjective_rel (X Y : Type) (R : X -> Y -> Prop) :=
  forall y, exists x, R x y.

Definition functional_rel X Y (R : X -> Y -> Prop) :=
  forall x y y', R x y -> R x y' -> y = y'.

Definition injective_rel X Y (R : X -> Y -> Prop) :=
  forall y x x', R x y -> R x' y -> x = x'.

Definition inject_rel X Y :=
  exists (R : X -> Y -> Prop), total_rel R /\ functional_rel R /\ injective_rel R.

Lemma inject_inject_rel X Y :
  inject X Y -> inject_rel X Y.
Proof.
  intros [f Hf]. exists (fun x y => y = f x). repeat split.
  - intros x. now exists (f x).
  - intros x y y' -> ->. reflexivity.
  - intros x x' y -> H. now apply Hf.
Qed.

(* The following aliases are needed to make setoid rewriting work. *)

Definition sum' : Type -> Type -> Type := sum.
Notation "X + Y" := (sum' X Y) : type_scope.

Definition prod' : Type -> Type -> Type := prod.
Notation "X * Y" := (prod' X Y) : type_scope.

Open Scope type_scope.

Lemma inject_refl X :
  inject X X.
Proof.
  exists (fun x => x). congruence.
Qed.

Lemma inject_trans X Y Z :
  inject X Y -> inject Y Z -> inject X Z.
Proof.
  intros [f Hf] [g Hg]. exists (fun x => g (f x)).
  now intros x x' H % Hg % Hf.
Qed.

Lemma inject_sum X Y X' Y' :
  inject X X' -> inject Y Y' -> inject (X + Y) (X' + Y').
Proof.
  intros [f Hf] [g Hg].
  exists (fun z => match z with inl x => inl (f x) | inr y => inr (g y) end).
  intros [x|y] [x'|y'] [=]; f_equal; eauto.
Qed.

Lemma inject_prod X Y X' Y' :
  inject X X' -> inject Y Y' -> inject (X * Y) (X' * Y').
Proof.
  intros [f Hf] [g Hg].
  exists (fun z : X * Y => let (x, y) := z in (f x, g y)).
  intros [x y] [x' y'] [=]. f_equal; eauto.
Qed.

Lemma inject_power_morph X Y :
  inject X Y -> inject (X -> Prop) (Y -> Prop).
Proof.
  intros [f Hf].
  exists (fun p => fun y => exists x, p x /\ y = f x).
  intros p q H. apply predicate_ext. intros x; split; intros Hx.
  - assert (Hp : exists x', p x' /\ f x = f x') by now exists x.
    pattern (f x) in Hp. rewrite H in Hp. now destruct Hp as [x'[Hq <- % Hf]].
  - assert (Hq : exists x', q x' /\ f x = f x') by now exists x.
    pattern (f x) in Hq. rewrite <- H in Hq. now destruct Hq as [x'[Hp <- % Hf]].
Qed.

Lemma inject_subtype X (p : X -> Prop) :
  inject (sig p) X.
Proof.
  exists (@pi1 X p). intros x y. apply exist_pi1.
Qed.

Lemma inject_power X :
  inject X (X -> Prop).
Proof.
  exists (fun x => eq x). now intros x x' ->.
Qed.

Fixpoint powit X n :=
  match n with
  | 0 => X
  | S n => powit (X -> Prop) n
  end.

Lemma powit_shift X n :
  powit (X -> Prop) n = (powit X n -> Prop).
Proof.
  induction n in X |- *; firstorder congruence.
Qed.

Lemma inject_powit X n :
  inject X (powit X n).
Proof.
  induction n.
  - apply inject_refl.
  - eapply inject_trans; try apply IHn. cbn. rewrite powit_shift. apply inject_power.
Qed.

Notation upair x y :=
  (fun z => z = x \/ z = y).

Definition opair X (x y : X) :=
  fun p => p = eq x \/ p = upair x y.

Lemma opair_inj1 X (x y x' y' : X) :
  opair x y = opair x' y' -> x = x'.
Proof.
  intros Hxy. assert (H : opair x y (eq x)) by now left.
  rewrite Hxy in H. destruct H as [H|H].
  - rewrite H. reflexivity.
  - rewrite H. now left.
Qed.

Lemma opair_inj2 X (x y x' y' : X) :
  opair x y = opair x' y' -> y = y'.
Proof.
  intros Hxy. assert (y = x' \/ y = y') as [->| ->]; trivial.
  - assert (H : opair x y (upair x y)) by now right.
    rewrite Hxy in H. destruct H as [H|H].
    + left. symmetry. rewrite <- H. now right.
    + pattern y. rewrite <- H. now right.
  - assert (x = x') as -> by now apply opair_inj1 in Hxy.
    assert (H : opair x' y' (upair x' y')) by now right.
    rewrite <- Hxy in H. destruct H as [H|H].
    + rewrite <- H. now right.
    + enough (H' : upair x' x' y') by now destruct H'.
      pattern y'. rewrite <- H. now right.
Qed.

Lemma inject_prod_power X :
  inject (X * X) (powit X 2).
Proof.
  exists (fun c : X * X => let (x, y) := c in opair x y).
  intros [x y] [x' y'] H. f_equal.
  - apply (opair_inj1 H).
  - apply (opair_inj2 H).
Qed.

Definition infinite X :=
  inject nat X.

Lemma infinite_inject X Y :
  infinite X -> inject X Y -> infinite Y.
Proof.
  apply inject_trans.
Qed.

Lemma infinite_powit X n :
  infinite X -> infinite (powit X n).
Proof.
  intros H. eapply infinite_inject; try apply H. apply inject_powit.
Qed.

Definition inverse X Y (f : X -> Y) (g : Y -> X) :=
  (forall x, g (f x) = x) /\ (forall y, f (g y) = y).

Definition biject (X Y : Type) :=
  exists (f : X -> Y) (g : Y -> X), inverse f g.

Lemma biject_refl X :
  biject X X.
Proof.
  exists (fun x => x), (fun x => x). split; reflexivity.
Qed.

Lemma biject_sym X Y :
  biject X Y -> biject Y X.
Proof.
  intros (f & g & H). exists g, f. split; apply H.
Qed.

Lemma biject_trans X Y Z :
  biject X Y -> biject Y Z -> biject X Z.
Proof.
  intros (f & f' & H1 & H2) (g & g' & H3 & H4).
  exists (fun x => g (f x)), (fun z => f' (g' z)). split.
  - intros x. rewrite H3. apply H1.
  - intros z. rewrite H2. apply H4.
Qed.

Instance biject_equiv :
  Equivalence biject.
Proof.
  split.
  - intros X. apply biject_refl.
  - intros X Y. apply biject_sym.
  - intros X Y Z. apply biject_trans.
Qed.

Instance biject_sum :
  Proper (biject ==> biject ==> biject) sum'.
Proof.
  intros X X' (f & f' & H1 & H2) Y Y' (g & g' & H3 & H4).
  exists (fun z => match z with inl x => inl (f x) | inr y => inr (g y) end).
  exists (fun z => match z with inl x => inl (f' x) | inr y => inr (g' y) end).
  split; intros []; congruence.
Qed.

Instance biject_prod :
  Proper (biject ==> biject ==> biject) prod'.
Proof.
  intros X X' (f & f' & H1 & H2) Y Y' (g & g' & H3 & H4).
  exists (fun z : X * Y => let (x, y) := z in (f x, g y)).
  exists (fun z : X' * Y' => let (x, y) := z in (f' x, g' y)).
  split; intros []; congruence.
Qed.

Instance biject_power :
  Proper (biject ==> biject) (fun X => X -> Prop).
Proof.
  intros X Y (f & g & Hgf & Hfg).
  exists (fun p => fun y => exists x, p x /\ y = f x).
  exists (fun p => fun x => exists y, p y /\ x = g y).
  split; intros p; apply FE; intros z; apply PE; firstorder eauto; congruence.
Qed.

Lemma biject_inject X Y :
  biject X Y -> inject X Y.
Proof.
  intros (f & g & Hgf & Hfg). exists f.
  intros x x' H. now rewrite <- (Hgf x), <- (Hgf x'), H.
Qed.

Definition incl X (p q : X -> Prop) :=
  forall x, p x -> q x.

Notation "p <<= q" := (incl p q) (at level 70).

Lemma incl_refl X (p : X -> Prop) :
  p <<= p.
Proof.
  unfold incl. tauto.
Qed.

Lemma incl_trans X (p q r : X -> Prop) :
  p <<= q -> q <<= r -> p <<= r.
Proof.
  unfold incl. intuition.
Qed.

Lemma incl_antisym X (p q : X -> Prop) :
  p <<= q -> q <<= p -> p = q.
Proof.
  intros H1 H2. apply FE. intros x. apply PE. firstorder.
Qed.

Structure WO X (R : X -> X -> Prop) : Prop :=
  {
    WO_refl : forall x, R x x;
    WO_trans : forall x y z, R x y -> R y z -> R x z;
    WO_antisym : forall x y, R x y -> R y x -> x = y;
    WO_wf : forall p, ex p -> (exists x, p x /\ forall y, p y -> R x y);
  }.

Definition WO_type X :=
  exists R, @WO X R.

Lemma WO_transport X Y :
  inject X Y -> WO_type Y -> WO_type X.
Proof.
  intros [f Hf] [R [HR1 HR2 HR3 HR4]]. exists (fun x x' => R (f x) (f x')). split.
  - intros x. apply HR1.
  - intros x y z. apply HR2.
  - intros x y H1 H2. now apply Hf, HR3.
  - intros p [x Hx]. destruct (HR4 (fun y => exists x, y = f x /\ p x)) as [y[[x'[-> H1]] H2]].
    + exists (f x), x. split; trivial.
    + exists x'. split; trivial. intros z Hz. apply H2. now exists z.
Qed.

Lemma WO_lin X R :
  @WO X R -> forall x y, R x y \/ R y x.
Proof.
  intros H x y.
    destruct (@WO_wf _ _ H (fun z => z = x \/ z = y)) as (z & [->| ->] & Hz).
    - exists x. now left.
    - left. apply Hz. now right.
    - right. apply Hz. now left.
Qed.

(* The following notions are placeholders to align the paper that will be instantiated later. *)

Definition relation_embedding X Y (R : X -> X -> Prop) (S : Y -> Y -> Prop) (f : X -> Y) :=
  forall x x', R x x' <-> S (f x) (f x').

Definition relation_embeddable X Y (R : X -> X -> Prop) (S : Y -> Y -> Prop) :=
  exists f, relation_embedding R S f.

Lemma relation_embedding_refl X (R : X -> X -> Prop) :
  relation_embeddable R R.
Proof.
  exists (fun x => x). firstorder.
Qed.

Lemma relation_embedding_trans X Y Z (R : X -> X -> Prop) (S : Y -> Y -> Prop) (T : Z -> Z -> Prop) :
  relation_embeddable R S -> relation_embeddable S T -> relation_embeddable R T.
Proof.
  intros [f Hf] [g Hg]. exists (fun x => g (f x)). intros x x'. rewrite (Hf x x'). apply Hg.
Qed.

Definition relation_isomorphism X Y (R : X -> X -> Prop) (S : Y -> Y -> Prop) (f : X -> Y) :=
  relation_embedding R S f /\ exists g, inverse f g.

Definition relation_isomorphic X Y (R : X -> X -> Prop) (S : Y -> Y -> Prop) :=
  exists f, relation_isomorphism R S f.

Lemma relation_isomorphism_refl X (R : X -> X -> Prop) :
  relation_isomorphic R R.
Proof.
  exists (fun x => x). firstorder. exists (fun x => x). firstorder.
Qed.

Lemma relation_isomorphism_sym X Y (R : X -> X -> Prop) (S : Y -> Y -> Prop) :
  relation_isomorphic R S -> relation_isomorphic S R.
Proof.
  intros (f & Hf & g & Hfg). exists g. split.
  - intros y y'. rewrite <- (proj2 Hfg y), <- (proj2 Hfg y') at 1. symmetry. apply Hf.
  - exists f. split; apply Hfg.
Qed.

Lemma relation_isomorphic_trans X Y Z (R : X -> X -> Prop) (S : Y -> Y -> Prop) (T : Z -> Z -> Prop) :
  relation_isomorphic R S -> relation_isomorphic S T -> relation_isomorphic R T.
Proof.
  intros (f & Hf & f' & Hf') (g & Hg & g' & Hg'). exists (fun x => g (f x)). split.
  - intros x x'. rewrite (Hf x x'). apply Hg.
  - exists (fun z => f' (g' z)). split.
    + intros x. now rewrite (proj1 Hg'), (proj1 Hf').
    + intros z. now rewrite (proj2 Hf'), (proj2 Hg').
Qed.