Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Ltac unify expressions


chronological Thread 
  • From: Gregory Malecha <gmalecha AT eecs.harvard.edu>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Ltac unify expressions
  • Date: Fri, 17 Feb 2012 16:44:18 -0500
  • Authentication-results: mr.google.com; spf=pass (google.com: domain of gmalecha AT eecs.harvard.edu designates 10.60.18.163 as permitted sender) smtp.mail=gmalecha AT eecs.harvard.edu

Hello, 

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.

It seems to work alright, but I would rather not fully evaluate the terms if I can help it, I'm going to end up running this a lot.

Thank you very much for any suggestions.

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




Archive powered by MhonArc 2.6.16.

Top of Page