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] Typeclasses vs canonical instances
- Date: Thu, 28 Apr 2016 02:11:02 +0000
- Authentication-results: mail3-smtp-sop.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-oi0-f45.google.com
- Ironport-phdr: 9a23:Aa+zShHs4RvkfagTCncLJ51GYnF86YWxBRYc798ds5kLTJ75pMqwAkXT6L1XgUPTWs2DsrQf27qQ4/urBzRIyK3CmU5BWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/nh6bioNaNO01hv3mUX/BbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv50IbaKvdKMhCLdcET4OMmYv5cStuwOQYxGI4y4+W34RlFJnGQ/e91muXJ7qtS31rO1mw3iyMsj/TLRyUjOnufQ4ACT0gTsKYmZquFrcjdZ92fpW
If you have [Definition foo := Set.] and you can't get multiple successes out of [unify foo foo] (where the second success comes from unfolding both [foo]s), which I suspect you can't, then the backtracking of unification isn't accessible from Ltac-land.
On Wed, Apr 27, 2016, 9:29 PM Jonathan Leivent <jonikelee AT gmail.com> wrote:
On 04/27/2016 05:04 AM, Enrico Tassi wrote:
> ...
> In short unification already performs some backtracking, in particular
> when constants are unfolded. By crafting a chain of aliases (constants
> begin just another name for the same value) one can trick unification
> into trying many "canonical" solutions for the "same" problem.
If so, then there should be open_constrs X and Y such that "unify X Y"
succeeds but "exactly_once (unify X Y)" fails due to multiple
successes. I tried a few cases involving constant unfolding, but can't
seem to get this to occur. Can anyone else?
I'm not doubting that canonical structures can do backtracking - but it
might be "confined" backtracking, just like typeclasses backtracking is
confined to within a single invocation of typeclasses eauto, such that
one cannot backtrack back into a successful case from the outside.
-- Jonathan
- [Coq-Club] Typeclasses vs canonical instances, Igor Zhirkov, 04/24/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Gregory Malecha, 04/25/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Guillaume Melquiond, 04/26/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Jonathan Leivent, 04/27/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Gregory Malecha, 04/27/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Pierre-Marie Pédrot, 04/27/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Enrico Tassi, 04/27/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Jonathan Leivent, 04/28/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Jason Gross, 04/28/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Enrico Tassi, 04/29/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Enrico Tassi, 04/27/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Pierre-Marie Pédrot, 04/27/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Gregory Malecha, 04/27/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Jonathan Leivent, 04/27/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Guillaume Melquiond, 04/26/2016
- Re: [Coq-Club] Typeclasses vs canonical instances, Gregory Malecha, 04/25/2016
Archive powered by MHonArc 2.6.18.