The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Yes, the typeclass depth needs to depend on the shape of the subgoal, or at least the tactic I'm running.  If I set the depth to 1, [autorewrite] succeeds in 0.04 seconds.  But then earlier typeclass resolution fails.  If I set the depth to 5, then the earlier resolution succeeds, but [autorewrite] takes 1.3 seconds each time I run it.

-Jason

On Tue, May 31, 2016 at 6:22 PM, Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

Does the following work?

Typeclasses eauto := 1 (* or a small number denoting the depth of search *)

https://coq.inria.fr/refman/Reference-Manual023.html#TypeClassCommands (20.6.6)

Do you want a way to make the depth of the search depend on the shape of the typeclass-resolution subgoal?

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Tue, May 31, 2016 at 5:33 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

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.