The Coq mailing list

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

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.