Library withpem

Require Import prelude.
Require Import withlpo.
Require Import hlemmas.
Require Import Arith.


Section CB.

  Variable PEM : forall A, hprop A -> A + ¬ A.

  Lemma decrange : forall A B : Type, forall f : A -> B, hset B -> injective f -> forall b, decidable (range f b).
    intros.
    apply PEM.
    apply range_hprop; assumption.
  Qed.

  Lemma lpo_true : lpo.
    apply lpo_iff_lpo_min.
    unfold lpo_min.
    intro f.
    match goal with
     [|- (?a + _)%type ] => destruct (PEM a)
    end.
    - apply Sigma_hprop.
      + intros ? ? [? ?] [? ?].
        destruct (lt_eq_lt_dec a a') as [ [ | ] | ].
        * exfalso; rewrite e2 in e; [inversion e|].
          apply Nat.ltb_lt in l; assumption.
        * assumption.
        * exfalso; rewrite e0 in e1; [inversion e1|].
          apply Nat.ltb_lt in l; assumption.
      + intros. apply prod_hprop.
        * apply bool_hset.
        * do 2 (apply forall_hprop; intros); apply bool_hset.
    - left; assumption.
    - right.
      intros; case_eq (f k); auto; intros.
      exfalso.
      apply f0.
      clear PEM f0.
      revert f H.
      induction k; intros.
      + exists 0; split; auto.
        intros ? p; apply Nat.ltb_lt in p; inversion p.
      + destruct (IHk (fun z => f (S z)) H) as [? [? ?]].
        case_eq (f 0).
        * intros; exists 0; split; auto; intros ? p; apply Nat.ltb_lt in p; inversion p.
        * intros; exists (S x); split; auto.
          intros [|]; auto.
  Qed.

  Section CB.

    Variable A B : Type.
    Variable Aset : hset A.
    Variable Bset : hset B.
    Variable f : A -> B.
    Variable g : B -> A.

    Variable f_inj : injective f.
    Variable g_inj : injective g.

    Theorem CB : Σ r : A -> B, isomorphism r.
      apply CB with f g; auto.
      + apply lpo_true.
      + apply decrange; auto.
      + apply decrange; auto.
    Qed.

  End CB.

End CB.