Stream: Coq users

Topic: Syntactic equality on Qc

view this post on Zulip Paolo Giarrusso (Aug 28 2023 at 19:28):

It seems that comparing canonical rationals (Qcanon.Qc_eq_dec) can exploit canonicity to run use syntactic equality (proof below) — but instead, it uses Qeq_dec which will multiply numerator and denominator — and AFAICT, that's slower. Even stdpp inherits this behavior (cc @Robbert Krebbers ). Am I missing something?

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.
  move => [q1 Hq1] [q2 Hq2] /= Hq; subst q2.
  by rewrite (proof_irrel Hq2 Hq1).

#[local] Instance Qc_eq_dec_alt : EqDecision Qc.
  refine  q1 q2, cast_if (decide (this q1 = this q2))).
  all: abstract naive_solver.
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,
           ((λ H0 : x = y,
                 H (eq_ind_r (λ x0 : Qc, x0 == y) (Qeq_refl y) H0)
                 return False
              : x ≠ y)) b
     : ∀ 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

view this post on Zulip Jason Gross (Aug 29 2023 at 05:44):

Seems like low-hanging-fruit improvement to me

view this post on Zulip Robbert Krebbers (Aug 29 2023 at 06:37):

Good catch. You could make an MR in Coq-stdlib to fix this? If you want this to be fixed urgently in std++, please make a std++ MR to work around it.

Last updated: Jun 22 2024 at 16:02 UTC