The Coq mailing list

[qgxu AT mail.shu.edu.cn]

Hello coq-club:
  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.

 On  page 98, there are the defintions about "refl_equal" and "eq_ind":

  refl_equal : forall (A: Type)(x:A), x = x

  eq_ind : forall (A: Type)(x:A)(P:A->Prop), P x -> forall y: A. x=y -> P y

 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"?
 my anwsers is:  "eq_sym" has the 4 arguments A, x, y and h, so "eq_sym A x y h", has the type "y=x", is it correct?

  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" ?
  ...

  These questions are dancing in my mind for a long time.  who can help me? thanks in advance!
 
  Best Kinds!

  Q.g. XU
����������������������������qgxu AT mail.shu.edu.cn
����������������������������������2010-05-27