Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Typeclasses vs canonical instances

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Typeclasses vs canonical instances


Chronological Thread 
  • 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




Archive powered by MHonArc 2.6.18.

Top of Page