The Coq mailing list

[henaien amira <henaien_amira AT hotmail.com>]

Hi Malecha,

Think you very much for responding me. So, Unify will not be helpful to me. And as I say in my question, the example is just to illustrate. Actually what I wish to get is the substitution that will be applied by the tactic "apply" if it was used. 

---

From: gmalecha AT eecs.harvard.edu
Date: Tue, 20 Mar 2012 17:19:43 -0400
To: henaien_amira AT hotmail.com
CC: matthieu.sozeau AT gmail.com; coq-club AT inria.fr
Subject: Re: [Coq-Club] Ltac unify expressions

Hi, Henaien --

This tactic is not meant do do what you are asking it to do. This tactic only checks that the two terms are equal to each other (where equal is Coq's equal, i.e. beta, delta, iota, zeta equivalence). This isn't the case for your term because

n + 0 

does not reduce to 

0 + 0

What you need to do here is pick a particular [n] to instantiate with. I think you are meaning your lemma to be phrased as:

Theorem th_exp : (forall n : nat, n + 0 = n) -> 0 + 0 = 0.

This would be solved by 

intro H; apply H.

or [auto].

Hope this helps.

On Tue, Mar 20, 2012 at 3:32 PM, henaien amira <henaien_amira AT hotmail.com> wrote:

Hi,

I'm interested in this tactic, I tried to use it to unify two terms but unfortunately I get Error. Here is an example (well I know that there is an easier way to proved but i give it just as an example):

Ltac unification_hyp :=
match goal with
|[_ : ?t = ?u |- ?tg = ?ug  ] => unify t tg
| _ => fail
end.

Theorem th_exp : forall n : nat, n + 0 = n -> 0 + 0 = 0 .
intros.
unification_hyp. (*Error: No matching clauses for match goal  (use "Set Ltac Debug" for more info).*)


Thanks,

Amira

> From: matthieu.sozeau AT gmail.com
> Date: Sat, 18 Feb 2012 01:49:09 +0100
> CC: gmalecha AT cs.harvard.edu
> To: coq-club AT inria.fr
> Subject: Re: [Coq-Club] Ltac unify expressions

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