The Coq mailing list

[henaien amira <henaien_amira AT hotmail.com>]

Actually "destruct plus" for this subgoal : "plus n id_0 = n"  will work only in the lhs of the equality so the result is : 

1.  id_0 = n

2. id_s (n0 ) = n

But I want to have this :

1.  id_0 = id_0
2.  id_s (plus  n0 id_0) = id_s n0

> Date: Wed, 21 Mar 2012 09:25:37 -0400
> From: krismicinski AT gmail.com
> To: henaien_amira AT hotmail.com
> CC: beta AT mpi-sws.org; coq-club AT inria.fr
> Subject: Re: [Coq-Club] Ltac unify expressions
>
> wait, why can't you just destruct on something involving plus, then?
>
> kris
>
> On Wed, Mar 21, 2012 at 9:21 AM, henaien amira
> <henaien_amira AT hotmail.com> wrote:
> > "Case n" will do case analysis by following the definition of type of n
> > (here nat ) but in my work I need a case analysis following the definition
> > of the function : "plus".
> >
> >
> >
> > ________________________________
> > From: beta AT mpi-sws.org
> > Date: Wed, 21 Mar 2012 13:42:07 +0100
> > To: henaien_amira AT hotmail.com
> > CC: coq-club AT inria.fr
> >
> > Subject: Re: [Coq-Club] Ltac unify expressions
> >
> > I'm still unsure of what you want to do, but I think that the tactic "case"
> > is what you need here.
> >
> > If you do
> >
> > case n.
> >
> > you will get the exact result you described.
> >
> > Best,
> > Beta
> >
> > On Wed, Mar 21, 2012 at 11:02 AM, henaien amira <henaien_amira AT hotmail.com>
> > wrote:
> >
> > Hi Beta,
> >
> > Well,  I take a look in Matita's home page and it seems that you are right.
> > Actually I'm working in something similar: the implementation of an
> > interactive theorem prover in Coq. But I have some difficulties with some
> > rules. For example I have an inference rule which should take a function and
> > an equality and give a case analysis of this last one. For example if I have
> > the function plus  :
> >
> > Fixpoint plus (x y : nat ) : nat   :=
> > match x with
> > | id_0 => y
> > | id_s x' => id_s ( plus x' y)
> > end.
> >
> > And if I have a theorem :
> >
> > Theorem th : forall n : nat , plus n id_0 = n.
> >  intro n .
> > ===========
> > plus n id_0 = n
> >
> > in this state my rule should give two subgoals :
> > 1. plus id_0 id_0 = id_0
> > 2.  id_s (plus  n id_0) = id_s n
> >
> > I have tried the tactic destruct plus. but destruct works only in the first
> > part so I'm looking for a tactic that may give the substitution used in the
> > first part of the equality so I can applied it for the second one. Or it
> > will great if there is a tactic that my do the case analysis.
> >
> > I hope that I have explained enough to get help :) .
> >
> > Thanks,
> >
> > Amira
> >
> > ________________________________
> > From: beta AT mpi-sws.org
> > Date: Wed, 21 Mar 2012 09:33:14 +0100
> >
> > Subject: Re: [Coq-Club] Ltac unify expressions
> > To: henaien_amira AT hotmail.com
> >
> >
> > Hi Amira,
> >
> > I'm curious about the use for such tactic. Can you tell me more about your
> > idea? The reason why I'm asking is because I have the impression that it
> > would be useful to have explicit meta-variables like Matita[1] does. And
> > your problems seems to fit into this concept.
> >
> > Cheers,
> > Beta
> >
> > [1] Table 4.10 in
> > http://matita.cs.unibo.it/docs/manual/html/sec_terms.html#terms_and_co
> >
> >
> >
> > On Wed, Mar 21, 2012 at 9:03 AM, henaien amira <henaien_amira AT hotmail.com>
> > wrote:
> >
> >
> > 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/
> >
> >
> >
>