Stream: Coq users

Topic: Syntactic equality on Qc

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.
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
*)
``````

Jason Gross (Aug 29 2023 at 05:44):

Seems like low-hanging-fruit improvement to me

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