coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
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, unboundedNot 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 backtrackingTrying 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 withAnomaly: Uncaught exception Pretype_errors.PretypeError(_, _, _). Please report atDebug: 1.1: simple apply @Morphisms_Prop.well_founded_morphism on(@Proper (forall _ : Foo, Foo) (@respectful Foo Foo R ?r) (bar c)) failed withError: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, unboundedIt 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 backtrackingIt looks like it immediately fails to resolve Param:Debug: 1: no match for (@Params (forall (_ : Foo) (_ : Foo), Foo) bar ?H1), 0 possibilitiesNow 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 candidateMobile: +1(510)220-1060
- [Coq-Club] adventures in setoid_rewrite, Vadim Zaliva, 02/28/2017
- Re: [Coq-Club] adventures in setoid_rewrite, Jason Gross, 02/28/2017
- Re: [Coq-Club] adventures in setoid_rewrite, Vadim Zaliva, 02/28/2017
- Re: [Coq-Club] adventures in setoid_rewrite, Jason Gross, 02/28/2017
Archive powered by MHonArc 2.6.18.