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
|
*****************************************************
**** ****
**** PROOF OBJECTS FOR HOL-LIGHT ****
**** EXPORTATION TO COQ ****
**** ****
**** Steven Obua (obua@in.tum.de) ****
**** Technische Universitt Mnchen ****
**** February 2005 ****
**** and ****
**** Chantal Keller (keller@lix.polytechnique.fr)****
**** Laboratoire d'Informatique de Polytechnique ****
**** January 2010 ****
**** ****
*****************************************************
LICENSE: The usual Hol-light license applies.
********************************************
* How to set up proof objects in Hol-light *
********************************************
There are two environment variables that need to be set in order to
generate and save proof objects.
Example:
export HOLPROOFOBJECTS=EXTENDED
export HOLPROOFEXPORTDIR=/home/obua/tmp/holproofexport
1. HOLPROOFOBJECTS
This environment variable switches proof objects on and off. In
addition, it allows to choose between two different modes of proof
objects. It can have one of four different values: NONE, BASIC,
EXTENDED, COQ. If it is not set or different from those three values
(the check is case-sensitive), NONE is assumed.
NONE
Proof objects are switched off.
BASIC
Proof objects are switched on.
EXTENDED
Proof objects are switched on. In contrast to BASIC, not only
the hol-light kernel generates proof objects, but also selected
theorem generating functions (like SYM) generate proof objects,
replacing and therefore abbreviating the primitive proof objects.
If you want to generate proof objects, the EXTENDED mode is the recommended
one. Hol-light needs much less memory in EXTENDED mode than in BASIC mode,
and it generates more compact proof objects on disk, too. The BASIC mode
might be useful if the proof object importer does not understand the EXTENDED
proof objects, but only the BASIC proof objects.
The proof object importer that comes with Isabelle/HOL understands EXTENDED
proof objects.
2. HOLPROOFEXPORTDIR
If proof objects are switched on, this environment variable needs to point
to a writeable directory, otherwise an exception is thrown when the user
tries to save his proof objects.
After setting these environment variables, see the following instructions.
*******************************************************
* How to build a "proof objects" version of HOL Light *
*******************************************************
Just go into the following subdirectory, which starts empty except for
the Makefile:
Proofrecording/hol_light
and type "make" (or "make hol" etc. if building an image). This will
(1) Copy all the core HOL Light files into this directory
(2) Copy those that need to be radically changed from ../diffs
(3) Systematically change "prove" into named "nprove" calls
Now you should just be able to start HOL Light as usual, but from
within this directory "Proofrecording/hol_light", and the various
proof recording options will be available to you; see below.
Note that the "unix" library is needed. If on a platform like Cygwin
where dynamic loading isn't supported, you need to use a standalone
image with both the "unix" and "num" libraries preinstalled, e.g. by
ocamlmktop -o ocamlnumunix nums.cma unix.cma
************************************
* Using proof objects in Hol-light *
************************************
There are basically three commands that are at your disposal for dealing
with proof objects:
1. save_thm : string -> thm -> thm
"save_thm n th" saves the proof of the given theorem th under the given
name n in the proof database. It returns as a value the unmodified theorem.
2. nprove: string -> term * tactic -> thm
"nprove n x" calls "prove x", saves the proof of the resulting theorem
under the given name n in the proof database, and returns the theorem.
3. export_saved_proofs: (string option) -> unit
"export_saved_proofs (Some <thyname>)" saves the whole current proof
database to the subdirectory $HOLPROOFEXPORTDIR/hollight/<thyname>.
For "export_saved_proofs None" the destination directory is
$HOLPROOFEXPORTDIR/hollight/hollight.
*********************************************************
* No built-in equality of theorems (and proofs) anymore *
*********************************************************
With the introduction of proof objects, theorems now not only consist
of a list of assumptions and a conclusion, but of a proof object as well.
Therefore even if theorems A and B state the same proposition,
they might not be equal under built-in equality "=", because the proof
for A might differ from the proof of B. Therefore built-in equality
for theorems is now forbidden, a comparison "A = B" fails with
the following message:
Exception: Invalid_argument "equal: functional value".
If theorems need to be compared, the function
equals_thm: thm -> thm -> bool
can be used. This function only compares assumptions and
conclusion, and ignores the proof object.
***************************************
* Eporting the proof objects into Coq *
***************************************
It is now possible to export the proof objects in a format that is
readable for Coq, such that the theorems can be re-checked and used in
Coq. The differences with the standard exportation system are:
1. Set the environment variable HOLPROOFOBJECTS to COQ:
COQ
The same as for EXTENDED, but proof objects are not exported to
an XML format but to a format that is readable by Coq.
2. To start HOL-Light, the ocamlgraph and str libraries are needed. You
have to install ocamlgraph, then use a standalone image with both these
libraries preinstalled. This can be done automatically by executing
make top
The top-level that is created has the name top.
3. In addition with the commands save_thm and nprove, you dispose of
three commands to perform the exportation:
- export_saved_proofs: unit -> unit
"export_saved_proofs ()" saves the whole current proof database to the
subdirectory $HOLPROOFEXPORTDIR/hollight/hollight.
- export_one_proof: string -> unit
"export_one_proof "foobar"" saves the proof of the theorem foobar to the
subdirectory $HOLPROOFEXPORTDIR/hollight/hollight.
- export_list: string list -> unit
"export_list l" saves the proofs of all the theorems of l to the
subdirectory $HOLPROOFEXPORTDIR/hollight/hollight.
4. To exploit the theorems that have been exported, you have to download
the Coq's interface at
<http://perso.ens-lyon.fr/chantal.keller/Documents-recherche/Stage09/hollightcoq-coq.tar.gz>.
A README file explains how to use it.
********************
* Acknowledgements *
********************
Thanks to Sebastian Skalberg for his tremendous help with
porting his HOL4 code to Hol-light. Thanks to Tobias Nipkow for his idea
on how to detect calls to the built-in equality of theorems during runtime,
and thanks to Virgile Prevosto for his proposal on how to statically
detect calls to the built-in equality on theorems.
Last, but not least, thanks to John Harrison for including and integrating
this proof object stuff in his very nice and clean Hol-light distribution.
|
