Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Ltac unify expressions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Ltac unify expressions


chronological Thread 
  • From: Gregory Malecha <gmalecha AT eecs.harvard.edu>
  • To: Matthieu Sozeau <matthieu.sozeau AT gmail.com>
  • Cc: Coq Club <coq-club AT inria.fr>, gmalecha AT cs.harvard.edu
  • Subject: Re: [Coq-Club] Ltac unify expressions
  • Date: Sun, 19 Feb 2012 17:03:20 -0500
  • Authentication-results: mr.google.com; spf=pass (google.com: domain of gmalecha AT eecs.harvard.edu designates 10.60.3.167 as permitted sender) smtp.mail=gmalecha AT eecs.harvard.edu

This is great. Thanks.

On Fri, Feb 17, 2012 at 7:49 PM, Matthieu Sozeau <matthieu.sozeau AT gmail.com> wrote:
Hi Gregory,

 there is an undocumented tactic [unify x y [with hintdb]] that
does exactly what you expect. And it's now documented in the
reference manual.
-- Matthieu

Le 17 févr. 2012 à 23:49, Adam Chlipala a écrit :

> OK, perhaps then this to avoid adding unused cruft to proof terms:
>     (let unused := (refl_equal _ : a = b) in k true) || k false
>
> As for avoiding CPS, nothing comes to mind yet.
>
> On 02/17/2012 05:45 PM, Gregory Malecha wrote:
>> Does the [clear] call remove all traces of this from the proof? I'm going to end up calling this a lot (at least 100) and I'm worried about even small bits being left in the proof.
>>
>> The other thing is that this means is that I have to cps convert all of my ltac. Is there any other way to do this? I assume there is some Ocaml function that I could expose using a plugin if this doesn't exist right now. Would this be reasonable?
>>
>> Thanks.
>>
>> On Fri, Feb 17, 2012 at 5:26 PM, Adam Chlipala <adamc AT csail.mit.edu> wrote:
>> On 02/17/2012 04:44 PM, Gregory Malecha wrote:
>>> I am wondering if there is a better way to perform semantic equivalence checking in Ltac. Currently, I'm doing the following:
>>>
>>> Ltac unifies a b :=
>>>   match a with
>>>     | b => true
>>>     | _ =>
>>>       let a := eval cbv in a in
>>>       let b := eval cbv in b in
>>>       match a with
>>>         | b => true
>>>         | _ => false
>>>       end
>>>   end.
>>
>> Here's one of those Gallina/Ltac puns that is both horrifying and super-fun IMO:
>>     (let H := fresh in assert (H : a = b) by reflexivity; clear H; (* call a continuation with [true]) || (* call continuation with [false] *)
>> This may have side effects if there are unification variables left undetermined beforehand.
>>
>



--
gregory malecha
http://www.people.fas.harvard.edu/~gmalecha/




Archive powered by MhonArc 2.6.16.

Top of Page