The Coq mailing list

[Kristopher Micinski <krismicinski AT gmail.com>]

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