没有合适的资源?快使用搜索试试~ 我知道了~
首页Coq教程The Coq Proof Assistant
资源详情
资源推荐
![](https://csdnimg.cn/release/download_crawler_static/11704697/bg1.jpg)
The Coq Proof Assistant
A Tutorial
April 4, 2013
Version 8.4pl2
1
Gérard Huet, Gilles Kahn and Christine Paulin-Mohring
TypiCal Project (formerly LogiCal)
1
This research was partly supported by IST working group “Types”
![](https://csdnimg.cn/release/download_crawler_static/11704697/bg2.jpg)
V8.4pl2, April 4, 2013
c
INRIA 1999-2004 (COQ versions 7.x)
c
INRIA 2004-2012 (COQ versions 8.x)
![](https://csdnimg.cn/release/download_crawler_static/11704697/bg3.jpg)
Getting started
COQ is a Proof Assistant for a Logical Framework known as the Calculus of Induc-
tive Constructions. It allows the interactive construction of formal proofs, and also
the manipulation of functional programs consistently with their specifications. It
runs as a computer program on many architectures. It is available with a variety of
user interfaces. The present document does not attempt to present a comprehensive
view of all the possibilities of COQ, but rather to present in the most elementary
manner a tutorial on the basic specification language, called Gallina, in which for-
mal axiomatisations may be developed, and on the main proof tools. For more
advanced information, the reader could refer to the COQ Reference Manual or the
Coq’Art, a new book by Y. Bertot and P. Castéran on practical uses of the COQ
system.
Coq can be used from a standard teletype-like shell window but preferably
through the graphical user interface CoqIde
1
.
Instructions on installation procedures, as well as more comprehensive docu-
mentation, may be found in the standard distribution of COQ, which may be ob-
tained from COQ web site http://coq.inria.fr.
In the following, we assume that COQ is called from a standard teletype-like
shell window. All examples preceded by the prompting sequence Coq < represent
user input, terminated by a period.
The following lines usually show COQ’s answer as it appears on the users
screen. When used from a graphical user interface such as CoqIde, the prompt is
not displayed: user input is given in one window and COQ’s answers are displayed
in a different window.
The sequence of such examples is a valid COQ session, unless otherwise spec-
ified. This version of the tutorial has been prepared on a PC workstation running
Linux. The standard invocation of COQ delivers a message such as:
unix:~> coqtop
Welcome to Coq 8.2 (January 2009)
Coq <
The first line gives a banner stating the precise version of COQ used. You
1
Alternative graphical interfaces exist: Proof General and Pcoq.
3
![](https://csdnimg.cn/release/download_crawler_static/11704697/bg4.jpg)
4
should always return this banner when you report an anomaly to our bug-tracking
system http://logical.futurs.inria.fr/coq-bugs
![](https://csdnimg.cn/release/download_crawler_static/11704697/bg5.jpg)
Chapter 1
Basic Predicate Calculus
1.1 An overview of the specification language Gallina
A formal development in Gallina consists in a sequence of declarations and defini-
tions. You may also send COQ commands which are not really part of the formal
development, but correspond to information requests, or service routine invoca-
tions. For instance, the command:
Coq < Quit.
terminates the current session.
1.1.1 Declarations
A declaration associates a name with a specification. A name corresponds roughly
to an identifier in a programming language, i.e. to a string of letters, digits, and a
few ASCII symbols like underscore (_) and prime (’), starting with a letter. We use
case distinction, so that the names A and a are distinct. Certain strings are reserved
as key-words of COQ, and thus are forbidden as user identifiers.
A specification is a formal expression which classifies the notion which is being
declared. There are basically three kinds of specifications: logical propositions,
mathematical collections, and abstract types. They are classified by the three basic
sorts of the system, called respectively Prop, Set, and Type, which are themselves
atomic abstract types.
Every valid expression e in Gallina is associated with a specification, itself a
valid expression, called its type τ(E). We write e : τ(E) for the judgment that e is
of type E. You may request COQ to return to you the type of a valid expression by
using the command Check:
Coq < Check O.
0
: nat
5
剩余52页未读,继续阅读
![pdf](https://img-home.csdnimg.cn/images/20210720083512.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![zip](https://img-home.csdnimg.cn/images/20210720083736.png)
![zip](https://img-home.csdnimg.cn/images/20210720083736.png)
![zip](https://img-home.csdnimg.cn/images/20210720083736.png)
![](https://profile-avatar.csdnimg.cn/ff643762db724ed6b76b764cd95b4aaf_qq_45624427.jpg!1)
qq_45624427
- 粉丝: 1
- 资源: 4
上传资源 快速赚钱
我的内容管理 收起
我的资源 快来上传第一个资源
我的收益
登录查看自己的收益我的积分 登录查看自己的积分
我的C币 登录后查看C币余额
我的收藏
我的下载
下载帮助
![](https://csdnimg.cn/release/wenkucmsfe/public/img/voice.245cc511.png)
会员权益专享
最新资源
- BSC绩效考核指标汇总 (2).docx
- BSC资料.pdf
- BSC绩效考核指标汇总 (3).pdf
- C5000W常见问题解决方案.docx
- BSC概念 (2).pdf
- ESP8266智能家居.docx
- ESP8266智能家居.pdf
- BSC概念 HR猫猫.docx
- C5000W常见问题解决方案.pdf
- BSC模板:关键绩效指标示例(财务、客户、内部运营、学习成长四个方面).docx
- BSC概念.docx
- BSC模板:关键绩效指标示例(财务、客户、内部运营、学习成长四个方面).pdf
- BSC概念.pdf
- 各种智能算法的总结汇总.docx
- BSC概念 HR猫猫.pdf
- bsc概念hr猫猫.pdf
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035111.png)
安全验证
文档复制为VIP权益,开通VIP直接复制
![](https://csdnimg.cn/release/wenkucmsfe/public/img/green-success.6a4acb44.png)