The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

Is there a way to get typeclass resolution to fail quickly?  For example, if the search encounters

  Proper (le ==> _ ==> impl) le

it should fail immediately, because instantiating the _ with any reflexive relation yields a contradiction, and instantiating it with any irreflexive relation yields a slow failure on searching for a ProperProxy (in setoid_rewriting).  But I can't seem to get this to happen; typeclass resolution calls [proper_subrelation], and then tries to convert each Proper instance it finds for lt with (lt ==> _ ==> impl), which is, of course, impossible.  This means I need to be extremely careful to not put any lemmas in my rewriting databases which can utterly fail to be respected by any other relation (so any facts about [le] or [lt] are right out).  This is annoying, especially when I want facts of the form [forall x, lt x x <-> False] or [forall x, le x x <-> True],* so that I can use rewriting databases to find contradictions in the hypotheses.

Are there ways to fix this?

Thanks,

Jason

* The actual situation is a bit more complicated: I am using boolean-valued relations with a coercion to Sortclass (is_true), and the problem comes when I have something like [forall x, leb x x = true].  Since I've declared [leb : nat -> nat -> Prop] as a relation which can have instances, the setoid rewriting machinery tries both to replace [leb x x] with [true], and also to replace [x] with [x] via the [fun x y => is_true (leb x y)] relation, which is what causes the slowness.