The Coq mailing list

[henaien amira <henaien_amira AT hotmail.com>]

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