Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] adventures in setoid_rewrite

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] adventures in setoid_rewrite


Chronological Thread 
  • From: Jason Gross <jasongross9 AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] adventures in setoid_rewrite
  • Date: Tue, 28 Feb 2017 15:29:39 +0000
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f170.google.com
  • Ironport-phdr: 9a23:3a4NExP6Wq30LHfO5/0l6mtUPXoX/o7sNwtQ0KIMzox0K/v6rarrMEGX3/hxlliBBdydsKMZzbCG+P++ESxYuNDa7yBEKMQNHzY+yuwo3CUYSPafDkP6KPO4JwcbJ+9lEGFfwnegLEJOE9z/bVCB6le77DoVBwmtfVEtfre9ScbuiJG80Pn38JnOaS1JgiC8aPV8NkaYtwLU4+sfmoxkYokrzQDS6i9Kcv9Rw2xyIkmIzj7z486x+Nho9CEG6KFpzNJJTaivJ/dwdrdfFjlza20=

The anomalies seem like bugs; please report them on the bug tracker.

I believe setoid_rewrite resolves a Params instance before trying partial_application_tactic.  My interpretation is:
1. Try to find the Proper instance for (bar c), with two remaining goals after this one
2. Since that failed, invoke TC resolution with a single Params instance to determine how many arguments to strip off (bar c)
3. Since that failed, default to stripping off one argument (via partial_application_tactic), and try again to find a Proper instance

Note that TC resolution seems to have no notion of nesting resolutions which are not subgoals; if, in an external TC hint, you do [let foo := constr:(_ : some_class) in ... ], this invokes TC resolution in a way that doesn't leave any indication of nesting in the log, as far as I can tell.


On Tue, Feb 28, 2017, 1:49 AM Vadim Zaliva <vzaliva AT cmu.edu> wrote:
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:


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
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

...

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




Archive powered by MHonArc 2.6.18.

Top of Page