The Coq mailing list

[Vadim Zaliva <vzaliva AT cmu.edu>]

Hi!

Since I am working with setoid_rewriting tactic a lot I am trying to get a better understanding how it works to be able to resolve the problems. For instance, I have noticed changes in behavior between Coq 8.5 and 8.6. Often, type class resolution for Proper instances during setoid_rewrite runs amok and I need to be able to debug such situations. I found options which enable logging, but my logs are huge and hard to read. I even wrote a small script which visualizes them via graphvis. On some examples it works reasonably well, producing output like this:

https://github.com/vzaliva/coq-log-analysis/blob/master/samples/samplepdf.pdf

However, I could not make sense of log files for fairly simple cases. Here is an example:

Require Import Relations Setoid Morphisms.

Parameter Foo: Type.

Parameter R: relation Foo.

Parameter bar: Foo -> Foo -> Foo.

Instance R_reflexive: Reflexive R. Admitted.

Instance R_trasitive: Transitive R. Admitted.

Instance bar_proper: Proper ((R) ==> (R) ==> (R)) (bar). Admitted.

Example Test (a b c: Foo):

  R a b -> R (bar c a) (bar c b).

Proof.

  intros H.

  Set Typeclasses Debug.

  Set Typeclasses Debug Verbosity 2.

  Set Printing All.

  setoid_rewrite H.

The very first message mentions 3 goals:

Debug: Starting resolution with 3 goal(s) under focus and 0 shelved goal(s) in only_classes mode, unbounded

Not sure what these goals are, but hopefully they will reveal themselves as we proceed. Then, it proceeds to try what I assume is the first goal:

Debug: 1: looking for (@Proper (forall _ : Foo, Foo) (@respectful Foo Foo R ?r) (bar c)) with backtracking

Trying bunch of tactics, each of them failing with an Anomaly:

Debug: 1.1: exact bar_proper on

(@Proper (forall _ : Foo, Foo) (@respectful Foo Foo R ?r) (bar c)) failed with 

Anomaly: Uncaught exception Pretype_errors.PretypeError(_, _, _). Please report at

http://coq.inria.fr/bugs/.

Debug: 1.1: simple apply @Morphisms_Prop.well_founded_morphism on

(@Proper (forall _ : Foo, Foo) (@respectful Foo Foo R ?r) (bar c)) failed with 

Error:

Anomaly: Uncaught exception Pretype_errors.PretypeError(_, _, _). Please report at

http://coq.inria.fr/bugs/.

...

After exhausting all tactics it has to try (failed "1.1" leaves) it suddenly reports that it restarting resolutions with just one goal (not 3 anymore!). Note it has the same level "1" as before and does not look like a subgoal.

Debug: Starting resolution with 1 goal(s) under focus and 0 shelved goal(s) in only_classes mode, unbounded

It is now looking for Params instance, not Proper. It is unclear where this comes from. The only mention of Params class I found is in LTAC "partial_application_tactic," but there is no record of its application in the log yet.

Debug: 1: looking for (@Params (forall (_ : Foo) (_ : Foo), Foo) bar ?H1) with backtracking

It looks like it immediately fails to resolve Param:

Debug: 1: no match for (@Params (forall (_ : Foo) (_ : Foo), Foo) bar ?H1)

, 0 possibilities

Now I would guess it has to proceed to a new goal. But there is no  message "Starting resolution" like before, it just applies partial_applicatoin_tactic to the initial goal.

Debug: 1.1: (*external*) partial_application_tactic on

(@Proper (forall _ : Foo, Foo) (@respectful Foo Foo R ?r) (bar c)), 2 subgoal(s)

Probably my interpretation of these messages is pretty naive and I am just poking in the dark. Any advice or hints are greatly appreciated. I am also started to look at the Coq source code, but I am at early stages of understanding it and have not been able yet to connect where these messages are generated. I am starting to suspect that the log messages might be incomplete and it is not possible to reconstruct search tree from them alone.

P.S. I wish there is a way to disable typeclass resolution during setoid_rewrite and generate them as goals instead, letting the user to manually supply proofs.

--

CMU ECE PhD candidate

Mobile: +1(510)220-1060