The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi,



Le 27/05/2010 13:32, qgxu AT mail.shu.edu.cn a ��crit :

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?

Ok. The type of eq_sym is the following :


Check eq_sym.
eq_sym
     : forall (A : Type) (x y : A), x = y -> y = x

(Note that Coq's Standard Library already has sym_eq (in Init.Logic)

  2) how to instance the definition of eq_ind in the process of proving the eq_sym?

In an interactive proof of eq_sym , the simplest way is to get a goal :

H : x = y
-----------
  y = x

then rewrite <- H.

You can also apply explicitely eq_ind, but rewrite is more usual.
Goal forall (A : Type) (x y : A), x = y -> y = x.
intros A x y H.
pattern y. (* puts the goal under the form (P y) *)
apply (eq_ind  x);trivial.
Qed.

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

In eq_ind, the argument "A" is implicit (just check it by typing "About eq_ind"
 About eq_ind.
eq_ind :
forall (A : Type) (x : A) (P : A -> Prop), P x -> forall y : A, x = y -> P y

Argument A is implicit


So if you consider the term eq_ind x (fun z => z=x) (refl_equal x) y h.

the correspondance is
A  <-> A (A implicit in eq_ind)
x <->  x
P  <->fun z => z = x
P x <->  (fun z => z = x) x     (reduces to  x = x )
y <-> y
x = y <-> x = y
P y <->  (fun z => z = x) y   (reduces to  y = x )

So the term "eq_ind x (fun z => z = x) (refl_equal x) y h" has type "y=x"

Again, this job is done by "rewrite"

Hope it helps,

Pierre

  ...

  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