The Coq mailing list

["许庆国" <qgxu AT mail.shu.edu.cn>]



coq-club

 

Hello.

 

    I cannot replay one of the sample in hurry, while the other samples works well in coq 8.4. Who can help me, thank you very much.

 

----------------------------

  When  coq check the  following defition,

 

      Definition fact_aux (n:Z) :=  iter n (Z*Z) (fun p => (fst p + 1, snd p * (fst p + 1))) (0, 1).

 

Coq give me the following message:

 

===>  

   Error: In environment

   n : Z

   The term "Z" has type "Set" while it is expected to have type "Z".

====== 

 

According to the explain from the command "Print Z.iter. "

 

=====>

Warning: query commands should not be inserted in scripts

Z.iter = 

fun (n : Z) (A : Type) (f : A -> A) (x : A) =>

match n with

| 0 => x

| Z.pos p => Pos.iter p f x

| Z.neg _ => x

end

     : Z -> forall A : Type, (A -> A) -> A -> A

Argument A is implicit and maximally inserted

Argument scopes are [Z_scope type_scope _ _]

=====

 

I think the parameter (Z*Z)  should   be omitted because of implicit.  

 

When   Coq check 

 

    Definition fact_aux (n:Z) := iter n (fun p => (fst p + 1, snd p * (fst p + 1))) (0, 1).

 

It responds the following error message for the above  fun  function :

 

===>

   Error: The type of this term is a product while it is expected to be a sort.

===========

 

 

 

 

 

ps:  coq version info. in my computer.

 

Version information

-------------------

The Coq Proof Assistant, version 8.4pl2 (April 2013)

Architecture win32 running Win32 operating system

Gtk version is 2.18.7

This is coqide.exe (opt is the best one for this architecture and OS)

 

 

Cheers

Qingguo XU

------------------  

2013-06-22

 

 

发件人： Yves Bertot

发送时间： 2010-02-25 16:44:32

收件人： Coq Club

抄送：

主题： [Coq-Club] Announcement: Coq in a Hurry (new version)

Hi all,

This message is to announce a new version of a document called "Coq in 

Hurry", designed as a short tutorial to the Coq system, aiming at a 

public whose main background would be programming (but not necessarily 

functional programming).  The objective is to describe a 

"self-contained" subset of the Coq facilities, strong enough to let 

people write programs and prove their correctness and to give a 

practical feeling while avoiding theoretical issues.

This is available at the following address

http://cel.archives-ouvertes.fr/inria-00001173/

My own usage of these notes it to provide the Coq training that is 

enough for a course in programming language semantics where all concepts 

are then encoded and reasoned about in the Coq system.

I will be happy to receive feedback on this tutorial, especially on the 

following matters:

- How long would it take to a real beginner to read through the notes 

and make the exercises?

- What is really the necessary background?  I hope to provide material 

that can be understood by people who start  with just a basic training 

in programming with a conventional programming language (C or Java), is 

that reasonable?

Yves