Global Set Implicit Arguments.
Global Unset Strict Implicit.
Global Unset Printing Records.
Global Unset Printing Implicit Defensive.
Global Set Regular Subst Tactic.
Hint Extern 4 => exact _. (* make auto use type class inference *)
Require Export Setoid Morphisms.

(* exists-style notation for Sigma-types *)
Notation "'Sigma' x .. y , p" :=
  (sigT (fun x => .. (sigT (fun y => p)) ..))
    (at level 200, x binder, right associativity,
     format "'[' 'Sigma' '/ ' x .. y , '/ ' p ']'")
  : type_scope.

Ltac inv A := inversion A; subst; try clear A.

Class dec (P : Prop) := decision: {P} + {~ P}.
Arguments decision P {dec}.

Tactic Notation "decide" constr(p) "as" simple_intropattern(i) :=
  destruct (decision p) as i.

Fact dec_trans P Q :
  P <-> Q -> dec P -> dec Q.
Proof.
  unfold dec. tauto.
Qed.

Arguments dec_trans P {Q} _ _.

Fact dec_eq_sym X (x y : X) :
  dec (x = y) -> dec (y = x).
Proof.
  unfold dec. intuition.
Qed.

Fact dec_DM_or P Q :
  dec P -> ~ (P \/ Q) <-> ~P /\ ~Q.
Proof.
  unfold dec. tauto.
Qed.

Instance True_dec :
  dec True.
Proof.
  unfold dec; auto.
Qed.

Instance False_dec :
  dec False.
Proof.
  unfold dec; auto.
Qed.

Instance impl_dec (P Q : Prop) :
  dec P -> dec Q -> dec (P -> Q).
Proof.
  unfold dec; tauto.
Qed.

Instance and_dec (P Q : Prop) :
  dec P -> dec Q -> dec (P /\ Q).
Proof.
  unfold dec; tauto.
Qed.

Instance or_dec (P Q : Prop) :
  dec P -> dec Q -> dec (P \/ Q).
Proof.
  unfold dec; tauto.
Qed.

Instance not_dec (P : Prop) :
  dec P -> dec (~P).
Proof.
  unfold not. auto.
Qed.

Instance iff_dec (P Q : Prop) :
  dec P -> dec Q -> dec (P <-> Q).
Proof.
  unfold iff. auto.
Qed.

Notation "'eq_dec' X" := (forall x y : X, dec (x=y)) (at level 70).

Structure eqType := EqType {
  eqType_X :> Type;
  eqType_dec : eq_dec eqType_X }.

Arguments EqType X {_} : rename.
Existing Instance eqType_dec.

Structure decPred X := DecPred {
  decPred_p :> X -> Prop;
  decPred_dec x : dec (decPred_p x) }.

Arguments DecPred {X} p {_} : rename.
Existing Instance decPred_dec.

Section Pure.
  Variable X : Type.
  Variable p : decPred X.

  Definition pure x := if decision (p x) then True else False.

  Lemma pure_equiv x :
    pure x <-> p x.
  Proof.
    unfold pure. decide (p x) as [A|A]; tauto.
  Qed.

  Lemma pure_pir x :
    forall A B : pure x, A = B.
  Proof.
    unfold pure. intros A B. decide (p x) as [C|C].
    - now destruct A, B.
    - destruct A.
  Qed.
End Pure.

Section Subtype.
  Variable A : eqType.
  Variable f : A -> A.
  Variable f_idem : forall a, f (f a) = f a.

  Let fp := DecPred (fun a => f a = a).
  Let X := sig (pure fp).
  Let I := @proj1_sig A (pure fp).

  Let S : A -> X.
    intros a. exists (f a). hnf.
    decide (fp (f a)) as [B|B].
    - auto.
    - apply B, f_idem.
  Defined.

  Let I_injective x y :
    I x = I y <-> x = y.
  Proof.
    split.
    - destruct x as (a,B), y as (b,C). cbn.
      intros <-. f_equal. apply pure_pir.
    - congruence.
  Qed.

  Let X_eq_dec : eq_dec X.
  Proof.
    intros x y.
    apply (dec_trans (I x = I y)).
    now apply I_injective. auto.
  Qed.

  Lemma sub_norm :
    Sigma (X: eqType) (S: A -> X) (I: X -> A),
    (forall x, S (I x) = x) /\ (forall a, I (S a) = f a).
  Proof.
    exists (@EqType X X_eq_dec), S, I. split.
    - intros x. apply I_injective. cbn.
      destruct x as (a&B). cbn.
      apply pure_equiv in B. exact B.
    - intros a. reflexivity.
  Qed.

End Subtype.

Fact right_inverse A X (f : A -> X) (g : X -> A) x y :
  (forall x, f (g x) = x) -> g x = g y <-> x = y.
Proof.
  intuition congruence.
Qed.