The Coq mailing list

[henaien amira <henaien_amira AT hotmail.com>]

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