The Coq mailing list

["" <judy AT mail.ccnu.edu.cn>]

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.