Lean quotients in Coq.

Quotient.v

Axiom quot : forall {A}, (A -> A -> Prop) -> Type.

Axiom quot_mk : forall {A} (R : A -> A -> Prop), A -> quot R.

Axiom quot_lift : forall {A B} {R : A -> A -> Prop} (f : A -> B),
  (forall a1 a2, R a1 a2 -> f a1 = f a2) -> quot R -> B.

Axiom quot_sound : forall {A} {R : A -> A -> Prop} {a1 a2},
  R a1 a2 -> quot_mk R a1 = quot_mk R a2.

Module Int.
  Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope.
  Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope.

  Local Open Scope pair_scope.
  Definition int := (nat * nat)%type.
  Definition eq n m := n#1 + m#2 = n#2 + m#1.
  Definition succ (n : int) := (S n#1, n#2).
  Definition pred (n : int) := (n#1, S n#2).
  Definition neg (n : int) := (n#2, n#1).
  Definition add n m := (n#1 + m#1, n#2 + m#2).
  Definition sub n m := (n#1 + m#2, n#2 + m#1).
  Definition mul n m := (n#1 * m#1 + n#2 * m#2, n#1 * m#2 + n#2 * m#1).
  Local Close Scope pair_scope.
End Int.

Definition int := quot Int.eq.

Definition int_mk := quot_mk Int.eq.

Theorem succ_proof : forall n m,
  Int.eq n m -> int_mk (Int.succ n) = int_mk (Int.succ m).
Proof.
  unfold Int.eq.
  intros.
  apply quot_sound.
  simpl.
  rewrite <- plus_n_Sm.
  auto.
Qed.

Definition succ := quot_lift (fun n => quot_mk _ (Int.succ n)) succ_proof.

Theorem pred_proof : forall n m,
  Int.eq n m -> int_mk (Int.pred n) = int_mk (Int.pred m).
Proof.
  unfold Int.eq.
  intros.
  apply quot_sound.
  simpl.
  rewrite <- plus_n_Sm.
  auto.
Qed.

Definition pred := quot_lift (fun n => quot_mk _ (Int.pred n)) pred_proof.

Theorem neg_proof : forall n m,
  Int.eq n m -> int_mk (Int.neg n) = int_mk (Int.neg m).
Proof. unfold Int.eq. intros. apply quot_sound. auto. Qed.

Definition neg := quot_lift (fun n => quot_mk _ (Int.neg n)) neg_proof.