The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

judy AT mail.ccnu.edu.cn
 wrote:
> Dear Instructors
>
> ask for help 
>
> 1,how to use the tactic destruct.
>
> 2,if I have defined some Definitions such as 
> Definition A1:=a=b.
> Defintion A2:= c->d.
> and I want to  use the Definition A1 or A2 when proving the lemma.
> for example Lemma b=c->(a->d).
>
> what tactic I should use.
>
> 3 if I face the situation there are the parameters in the statements such as 
> forall x y:nat f x -> g y .and also there are the parameters in goal maybe Lemma
> forall x y:nat p x-> q y . which means they are acturally the same 
> parameters,but
> in goals the parameters changed into x0 y0,but in statements parameters are x 
> y,
> how to use tactic to solve this?
>
>
> 4 if there are H0 a->b->c->d->e in the statement and there's a Deinition
> AB:=a=h.Defintion ABC:=h->f.I want to use only a to  get h through AB,and 
> then I
> can get f from h through ABC .so how to make a alone as  H. Amd how to use 
> tactic
> to get h from a through AB, then get f from ABC.
>
>
> thanks looking forward your E-mails!
>
> Judy.
>
> --------------------------------------------------------
> Bug reports: http://logical.futurs.inria.fr/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>   

1/ To learn how to use the tactic destruct, you should look at the 
manual and at examples.  There are
some of these examples in the following tutorials:

Coq in a hurry,  http://cel.archives-ouvertes.fr/inria-00001173 
<http://cel.archives-ouvertes.fr/inria-00001173/fr/>
A tutorial on recursive types in Coq 
http://www.labri.fr/Perso/~casteran/RecTutorial.pdf.gz

2/ when you have a fact that is an equality, the tactic rewrite usually 
helps.  At first sight for your
example, intros, rewrite, and apply should be enough.

However, it turns out that your example is badly formed:  your 
"Definition A1 := a=b."  does not
mean that you assume a=b to be a true proposition and A1 to be a name 
for this hypothesis.
It means something totally different, which is probably not what you 
intended: this command
only defines A1 as another name for the proposition "a=b".  Thus A1 is 
not an hypothesis and
A1 and "a=b" are two ways to write the same proposition, which is not 
assumed to hold after
this declaration.

I believe you actually wanted to write : "Hypothesis A1 : a=b."  If you 
do write this, then a=b
is really suppose to hold after this command.  You should do the same 
thing for A2.  Then, if
you state correctly that you want to assume A1 and A2 to hold, your 
lemma should be easy to
state using intros, rewrite, and apply.

3/ changes of bound names (for instance universally quantified names) 
like these can be ignored.
So, if an hypothesis has the same statement as the goal, except for the 
renaming of bound variables,
then you should use the tactics "apply" or "exact" as if the name change 
had not taken place.

4/ It is very hard to understand what your question is, but here are two 
remarks.  First, you
did the same error as in question 2:  having written "Definition AB := 
a=h." does not mean
that you can henceforth deduce h from a.  The same problem appears for 
the way you want
to deduce f from h.  Second, you cannot obtain a proof of a from the
concept that you have described described.

I hope this helps,

Yves