coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] adventures in setoid_rewrite

From: Vadim Zaliva <vzaliva AT cmu.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] adventures in setoid_rewrite
Date: Tue, 28 Feb 2017 09:48:57 -0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=vadim.zaliva AT west.cmu.edu; spf=Pass smtp.mailfrom=vadim.zaliva AT west.cmu.edu; spf=None smtp.helo=postmaster AT mail-wm0-f48.google.com
Ironport-phdr: 9a23:OOy4cRVg81fuluw/7FxuV7/sNjDV8LGtZVwlr6E/grcLSJyIuqrYbBCAt8tkgFKBZ4jH8fUM07OQ6PG9HzZQqs/Z7DgrS99lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal8IRiyrQjdrNcajIhtJqos1hfErWZDdvhLy29vOV+dhQv36N2q/J5k/SRQuvYh+NBFXK7nYak2TqFWASo/PWwt68LlqRfMTQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4qx2RhLklDsLOjgk+27Ql8JwkblboAq/qBNj347aboaVNP9kcaPce9MRWG5NU8lVWiBEBI63cokBAPcbPetArYb9qVsAoxW9CwexGu3g1iRFiWXq0aAgyektDR3K0Q4mEtkTsHrUttL1NKIKXO+61qbH0DTDb/ZL0jj+8ofIdhEhoe+WUrltdsfR10guGBnBjlWRt4zqJSiY2fgIs2iG9eZvS/+gi3M+pgx3vzOhyMAsiozTiYIUzFDJ7Tl2wIIvKt2jU050ecKkH4FMuCGGNot5XtgiT3ttuCY+0rEGuJi7fDILyJs93RLfZeaHf5CV7RL5U+aROSx3hHVqebKinBa971KgxfH7VsmyzFZFsCxFksXWun8R0BzT786KQeZ+8Ee5wTuC1Q/e5vtZLUwqlafXMZ0szqAqmpccsknOGDL9ll/sg6+MbEok//Cl6+T5bbXioZ+RL4p0hRv/MqQqg8C+D+E4PhQXU2iV9umx16fv/UL+QLVNgf02lrfWvIrGKsQco661Gw5V0oA95BajFzqr0tsVkWMaIF5beB+LlYvkN0/ULP33Dvqzm1Gsny1qx/DCML3hGJLNLn3bnbf/Z7ly9k9cyA8pwdFe/Z1UDrABIOzpVULqut3XEAQ5MxCuz+n7DdV9y5kSVnySDa+EKK/Sq0OH5vozI+mQY48YoCryK/885/L3kXA5nUIdcrKy0JsMaHG4G+xmLF+DbXrthNcBC2YKsRAkQOzkkl3RGQJUMn21Ruc34iwxIIOgF4bKAI6305Kb2yLuIJRaZ2UOOFmIEGnhP9GaSf4IaTybCsRkj3oJWaX3GNxp7g2nqAKvk+kvFeHT4CBN6cPu

Jason,

Thanks. See my comments below:

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

Reported as:

https://coq.inria.fr/bugs/show_bug.cgi?id=5360

also another very clear bug:

https://coq.inria.fr/bugs/show_bug.cgi?id=5364

I believe setoid_rewrite resolves a Params instance before trying partial_application_tactic.

I suspected that but quick grep though source code did not show any hardcoded mentions of Params class in tactics ML implementation. If it is caused by `partial_appliction_tactic` invocation via hints, it should have been logged *after* the extenral tactics invocation, not before. Myabe that's what happening: it first invokes the tactic and then logs the invocation? I guess the answer is somewhere in class_tactics.ml :)

My interpretation is:

1. Try to find the Proper instance for (bar c), with two remaining goals after this one

I wonder what are these remaining goals? By the way, here is the full log for this example:

https://dl.dropboxusercontent.com/u/24768226/tmp/test.txt.out

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

These steps make sense. I would like to the find corrsponding code which invokes them to make sure this is what happening.

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

By "nesting" you mean search deph as printed in log statement numbers like "1.1" and "1.1.2" (as printed by 'pr_deph' in 'class_tactics.ml')? This sounds like something which could be changed and will make logs more readable, but I am not sure if it would impact other things.

Thanks again!

Vadim

[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