The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

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.