From Coq Require Import QArith Qcanon.
From stdpp Require Import numbers ssreflect.

#[global] Instance Qp_to_Qc_inj : Inj eq eq Qp_to_Qc.
Proof. intros ??. apply Qp.to_Qc_inj_iff. Qed.

#[local] Instance Q_eq_dec : EqDecision Q.
Proof. solve_decision. Qed.

#[global] Instance Qcanon_this_inj : Inj eq eq Qcanon.this.
Proof.
  move => [q1 Hq1] [q2 Hq2] /= Hq; subst q2.
  by rewrite (proof_irrel Hq2 Hq1).
Qed.

#[local] Instance Qc_eq_dec_alt : EqDecision Qc.
Proof.
  refine (λ q1 q2, cast_if (decide (this q1 = this q2))).
  all: abstract naive_solver.
Defined.
Print Qcanon.Qc_eq_dec.
Print Qeq_dec.

(*
Arguments Qcanon.Qc_eq_dec (x y)%Qc_scope
Qp_to_Qc: Qp → Qc
this: Qc → Q
Qcanon.Qc_eq_dec =
λ x y : Qc,
  let s := Qeq_dec x y in
  match s with
  | left a => (λ H : x == y, left (Qc_is_canon x y H)) a
  | right b =>
      (λ H : ¬ x == y,
         right
           ((λ H0 : x = y,
               match
                 H (eq_ind_r (λ x0 : Qc, x0 == y) (Qeq_refl y) H0)
                 return False
               with
               end)
              : x ≠ y)) b
  end
     : ∀ x y : Qc, {x = y} + {x ≠ y}

Arguments Qcanon.Qc_eq_dec (x y)%Qc_scope
Qeq_dec =
λ x y : Q,
  BinInt.Z.eq_dec (Qnum x * Z.pos (Qden y)) (Qnum y * Z.pos (Qden x))
     : ∀ x y : Q, {x == y} + {¬ x == y}

Arguments Qeq_dec (x y)%Q_scope
*)