Stream: Hierarchy Builder devs & users

Topic: Redundant Canonical Projections


view this post on Zulip Josh Cohen (Feb 15 2024 at 22:05):

Hi, I am not an experienced user of Hierarchy Builder, so I be missing something, but is there a way to get the following example to succeed without any warnings? If the second HB.instance is commented out, eqP cannot be applied. If it is not commented out, it gives warnings that redundant canonical projections are ignored, but the proof works.

Require Export Coq.Strings.String.
From HB Require Import structures.
From mathcomp Require Import all_ssreflect.

Definition foo : Set := string.

HB.instance Definition _ := hasDecEq.Build string String.eqb_spec.
(*Gives "redundant-canonical-projection" *)
(*HB.instance Definition _ := hasDecEq.Build foo String.eqb_spec.*)

Lemma test (x y: list foo) : reflect (x = y) (x == y).
Proof.
  (*Succeeds if the above is uncommented, fails when commented*)
  apply eqP.
Qed.

One method to fix this is to define new _eqb and _eqb_spec functions, but this does not seem ideal:

Definition bar : Set := string.
Definition bar_eqb (x y: bar) : bool := String.eqb x y.
Definition bar_eqb_spec (x y: bar) : reflect (x = y) (bar_eqb x y) :=
  String.eqb_spec x y.

HB.instance Definition _ := hasDecEq.Build bar bar_eqb_spec.

Lemma test2 (x y: list bar) : reflect (x = y) (x == y).
Proof.
  apply eqP.
Qed.

view this post on Zulip Quentin VERMANDE (Feb 16 2024 at 06:01):

You are using vanilla Coq's apply. apply: eqP, apply/eqP, the exact variants and exact eqP all succeed.
Vanilla Coq tactics and ssreflect ones use different unification algorithms, so my guess is that the former does not unfold foo when failing to find an eqType instance for it, so that it can retry with string. However, it is surprising that list makes a difference. I am also not sure why the last instance does not trigger a warning.


Last updated: Apr 21 2024 at 01:02 UTC