The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

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.
>> 
>