Le 28/05/2010 12:59, a crit :
Prof. Pierre Casteran:
thank you very much!
I learned a lot from your reply,
especially the usage of the implicit argument.
Would you like to
give me the further hints?
the term "eq_ind x (fun z => z
= x) (refl_equal x) y h" has type "y=x"
What's meaning
of the type "x=y" ? Is it a predication type over type Aor a Set type
or the dependent product type?
Hi,
I don't understand your question quite well.
"x = y" is a proposition, which written, without any abbreviation, is
"@eq A x y" , where eq has type "forall (A:Type), A -> A -> Prop".
But a proposition is also a type, so there is no harm to write such
things as "the type x=y"
or "the proposition x = y", depending on whether i'm thinking in terms
of logic or type checking.
Is this an answer to your question ? or did I fail to understand it ?
Cheers,
Pierre
thanks a lot!
Best Kinds!
Q.g. XU
2010-05-28
From:
Pierre Casteran
Date:
2010-05-27 20:30:12
To:
qgxu
Cc:
coq-club
Subject:
Re: [Coq-Club] usage of eq_ind
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
|
