The Coq mailing list

[Jonas Oberhauser <s9joober AT googlemail.com>]

I'm not sure I understood what you want. You want to do destruction
along the recursive argument of plus?
And not just of plus, but given a recursive function f and an
application (f x_0 ... x_n), destruct x_i such that f recurses on x_i
?
Such that i could say:
"induction alongside f."
and I would get the subgoals where x_i is constructed?

2012/3/21 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/
>> >
>> >
>> >
>>