1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
|
(******************************************************************************)
(* Copyright (C) 2000-2004, Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
(* Project Helm (http://helm.cs.unibo.it) *)
(* Project MoWGLI (http://mowgli.cs.unibo.it) *)
(* *)
(* Coq Exportation to XML *)
(* *)
(******************************************************************************)
This module provides commands to export a piece of Coq library in XML format.
Only the information relevant to proof-checking and proof-rendering is exported,
i.e. only the CIC proof objects (lambda-terms).
This document is tructured in the following way:
1. User documentation
1.1. New vernacular commands available
1.2. New coqc/coqtop flags and suggested usage
1.3. How to exploit the XML files
2. Technical informations
2.1. Inner-types
2.2. CIC with Explicit Named Substitutions
2.3. The CIC with Explicit Named Substitutions XML DTD
================================================================================
USER DOCUMENTATION
================================================================================
=======================================
1.1. New vernacular commands available:
=======================================
The new commands are:
Print XML qualid. It prints in XML (to standard output) the
object whose qualified name is qualid and
its inner-types (see Sect. 2.1).
The inner-types are always printed
in their own XML file. If the object is a
constant, its type and body are also printed
as two distinct XML files.
The object printed is always the most
discharged form of the object (see
the Section command of the Coq manual).
Print XML File "filename" qualid. Similar to "Print XML qualid". The generated
files are stored on the hard-disk using the
base file name "filename".
Show XML Proof. It prints in XML the current proof in
progress. Its inner-types are also printed.
Show XML File "filename" Proof. Similar to "Show XML Proof". The generated
files are stored on the hard-disk using
the base file name "filename".
The verbosity of the previous commands is raised if the configuration
parameter verbose of xmlcommand.ml is set to true at compile time.
==============================================
1.2. New coqc/coqtop flags and suggested usage
==============================================
The following flag has been added to coqc and coqtop:
-xml export XML files either to the hierarchy rooted in
the directory $COQ_XML_LIBRARY_ROOT (if the environment
variable is set) or to stdout (if unset)
If the flag is set, every definition or declaration is immediately
exported to XML. The XML files describe the user-provided non-discharged
form of the definition or declaration.
The coq_makefile utility has also been modified to easily allow XML
exportation:
make COQ_XML=-xml (or, equivalently, setting the environment
variable COQ_XML)
The suggested usage of the module is the following:
1. add to your own contribution a valid Make file and use coq_makefile
to generate the Makefile from the Make file.
*WARNING:* Since logical names are used to structure the XML hierarchy,
always add to the Make file at least one "-R" option to map physical
file names to logical module paths. See the Coq manual for further
informations on the -R flag.
2. set $COQ_XML_LIBRARY_ROOT to the directory where the XML file hierarchy
must be physically rooted.
3. compile your contribution with "make COQ_XML=-xml"
=================================
1.3. How to exploit the XML files
=================================
Once the information is exported to XML, it becomes possible to implement
services that are completely Coq-independent. Projects HELM and MoWGLI
already provide rendering, searching and data mining functionalities.
In particular, the standard library and contributions of Coq can be
browsed and searched on the HELM web site:
http://helm.cs.unibo.it/library.html
If you want to publish your own contribution so that it is included in the
HELM library, use the MoWGLI prototype upload form:
http://mowgli.cs.unibo.it
================================================================================
TECHNICAL INFORMATIONS
================================================================================
==========================
2.1. Inner-types
==========================
In order to do proof-rendering (for example in natural language),
some redundant typing information is required, i.e. the type of
at least some of the subterms of the bodies and types. So, each
new command described in section 1.1 print not only
the object, but also another XML file in which you can find
the type of all the subterms of the terms of the printed object
which respect the following conditions:
1. It's sort is Prop or CProp (the "sort"-like definition used in
CoRN to type computationally relevant predicative propositions).
2. It is not a cast or an atomic term, i.e. it's root is not a CAST, REL,
VAR, MUTCONSTR or CONST.
3. If it's root is a LAMBDA, then the root's parent node is not a LAMBDA,
i.e. only the type of the outer LAMBDA of a block of nested LAMBDAs is
printed.
The rationale for the 3rd condition is that the type of the inner LAMBDAs
could be easily computed starting from the type of the outer LAMBDA; moreover,
the types of the inner LAMBDAs requires a lot of disk/memory space: removing
the 3rd condition leads to XML file that are two times as big as the ones
exported appling the 3rd condition.
==========================================
2.2. CIC with Explicit Named Substitutions
==========================================
The exported files are and XML encoding of the lambda-terms used by the
Coq system. The implementative details of the Coq system are hidden as much
as possible, so that the XML DTD is a straightforward encoding of the
Calculus of (Co)Inductive Constructions.
Nevertheless, there is a feature of the Coq system that can not be
hidden in a completely satisfactory way: discharging. In Coq it is possible
to open a section, declare variables and use them in the rest of the section
as if they were axiom declarations. Once the section is closed, every definition
and theorem in the section is discharged by abstracting it over the section
variables. Variable declarations as well as section declarations are entirely
dropped. Since we are interested in an XML encoding of definitions and
theorems as close as possible to those directly provided the user, we
do not want to export discharged forms. Exporting non-discharged theorem
and definitions together with theorems that rely on the discharged forms
obliges the tools that work on the XML encoding to implement discharging to
achieve logical consistency. Moreover, the rendering of the files can be
misleading, since hyperlinks can be shown between occurrences of the discharge
form of a definition and the non-discharged definition, that are different
objects.
To overcome the previous limitations, Claudio Sacerdoti Coen developed in his
PhD. thesis an extension of CIC, called Calculus of (Co)Inductive Constructions
with Explicit Named Substitutions, that is a slight extension of CIC where
discharging is not necessary. The DTD of the exported XML files describes
constants, inductive types and variables of the Calculus of (Co)Inductive
Constructions with Explicit Named Substitions. The conversion to the new
calculus is performed during the exportation phase.
The following example shows a very small Coq development together with its
version in CIC with Explicit Named Substitutions.
# CIC version: #
Section S.
Variable A : Prop.
Definition impl := A -> A.
Theorem t : impl. (* uses the undischarged form of impl *)
Proof.
exact (fun (a:A) => a).
Qed.
End S.
Theorem t' : (impl False). (* uses the discharged form of impl *)
Proof.
exact (t False). (* uses the discharged form of t *)
Qed.
# Corresponding CIC with Explicit Named Substitutions version: #
Section S.
Variable A : Prop.
Definition impl(A) := A -> A. (* theorems and definitions are
explicitly abstracted over the
variables. The name is sufficient
to completely describe the abstraction *)
Theorem t(A) : impl. (* impl where A is not instantiated *)
Proof.
exact (fun (a:A) => a).
Qed.
End S.
Theorem t'() : impl{False/A}. (* impl where A is instantiated with False
Notice that t' does not depend on A *)
Proof.
exact t{False/A}. (* t where A is instantiated with False *)
Qed.
Further details on the typing and reduction rules of the calculus can be
found in Claudio Sacerdoti Coen PhD. dissertation, where the consistency
of the calculus is also proved.
======================================================
2.3. The CIC with Explicit Named Substitutions XML DTD
======================================================
A copy of the DTD can be found in the file "cic.dtd".
<ConstantType> is the root element of the files that correspond to
constant types.
<ConstantBody> is the root element of the files that correspond to
constant bodies. It is used only for closed definitions and
theorems (i.e. when no metavariable occurs in the body
or type of the constant)
<CurrentProof> is the root element of the file that correspond to
the body of a constant that depends on metavariables
(e.g. unfinished proofs)
<Variable> is the root element of the files that correspond to variables
<InductiveTypes> is the root element of the files that correspond to blocks
of mutually defined inductive definitions
The elements
<LAMBDA>,<CAST>,<PROD>,<REL>,<SORT>,<APPLY>,<VAR>,<META>, <IMPLICIT>,<CONST>,
<LETIN>,<MUTIND>,<MUTCONSTRUCT>,<MUTCASE>,<FIX> and <COFIX>
are used to encode the constructors of CIC. The sort or type attribute of the
element, if present, is respectively the sort or the type of the term, that
is a sort because of the typing rules of CIC.
The element <instantiate> correspond to the application of an explicit named
substitution to its first argument, that is a reference to a definition
or declaration in the environment.
All the other elements are just syntactic sugar.
|
