The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

qgxu AT mail.shu.edu.cn
 wrote:
> Now, I am reading the book "Interactive theorem proving and program
> development: Coq'Art : ...".
> I have some question about the proving "eq_sym" using the defition for
> "eq_ind" on pages 99 and 100.

I'm happy to be able to give you two generic recipes for answering these
questions. :)

> On Page 99, there is a proof for "eq_sym":
> Defintion eq_sym (A:Type)(x y: A)(h: x=y) : y=x :=
> eq_ind x (fun z => z=x) (refl_equal x) y h.
>
> My question is:
> 1) what's the type of "eq_sym"?

Run this command to see:
Check eq_sym.

> 2) how to instance the definition of eq_ind in the process of proving
> the eq_sym?
> i.e.
> "x" in page 99 is corresponding to "A" or "x" of "eq_ind : forall (A:
> Type)(x:A)(P:A->Prop), P x -> forall y: A. x=y -> P y"?
> "refl_equal x" is corresponding to "P" ?

Run this command to get all the info you need:
About eq_ind.

The type that is displayed will make clear what all of the arguments
are. A later line lists which arguments are implicit. In a particular
application of [eq_ind], the arguments passed will be exactly those not
marked implicit, in exactly the same order you can read off from
[eq_ind]'s type.