aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/Natural.tex
blob: f33c0d35633d6cfd32f3d7617371b61f31aefba6 (plain)
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
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
\achapter{\texttt{Natural} : proofs in natural language}
\aauthor{Yann Coscoy}

\asection{Introduction}

\Natural~ is a package allowing the writing of proofs in natural
language. For instance, the proof in \Coq~of the induction principle on pairs
of natural numbers looks like this:

\begin{coq_example*}
Require Natural.
\end{coq_example*}
\begin{coq_example}
Print nat_double_ind.
\end{coq_example}

Piping it through the \Natural~pretty-printer gives:

\comindex{Print Natural}
\begin{coq_example}
Print Natural nat_double_ind.
\end{coq_example}

\asection{Activating \Natural}

To enable the printing of proofs in natural language, you should
type under \texttt{coqtop} or \texttt{coqtop -full} the command

\begin{coq_example*}
Require Natural.
\end{coq_example*}

By default, proofs are transcripted in english. If you wish to print them 
in French, set the French option by

\comindex{Set Natural}
\begin{coq_example*}
Set Natural French.
\end{coq_example*}

If you want to go back to English, type in

\begin{coq_example*}
Set Natural English.
\end{coq_example*}

Currently, only \verb=French= and \verb=English= are available.

You may see for example the natural transcription of the proof of
the induction principle on pairs of natural numbers:

\begin{coq_example*}
Print Natural nat_double_ind.
\end{coq_example*}

You may  also show in natural language the current proof in progress:

\comindex{Show Natural}
\begin{coq_example}
Goal (n:nat)(le O n).
Induction n.
Show Natural Proof.
\end{coq_example}

\subsection*{Restrictions}

For \Natural, a proof is an object of type a proposition (i.e. an
object of type something of type {\tt Prop}). Only proofs are written
in natural language when typing {\tt Print Natural \ident}.  All other
objects (the objects of type something which is of type {\tt Set} or
{\tt Type}) are written as usual $\lambda$-terms.

\asection{Customizing \Natural}

The transcription of proofs in natural language is mainly a paraphrase of
the formal proofs, but some specific hints in the transcription
can be given.
Three kinds of customization are available.

\asubsection{Implicit proof steps}

\subsubsection*{Implicit lemmas}

Applying a given lemma or theorem \verb=lem1= of statement, say $A
\Rightarrow B$, to an hypothesis, say $H$ (assuming $A$) produces the
following kind of output translation:

\begin{verbatim}
...
Using lem1 with H we get B.
...
\end{verbatim}

But sometimes, you may prefer not to see the explicit invocation to
the lemma. You may prefer to see:

\begin{verbatim}
...
With H we have A.
...
\end{verbatim}

This is possible by declaring the lemma as implicit. You should type:

\comindex{Add Natural}
\begin{coq_example*}
Add Natural Implicit lem1.
\end{coq_example*}

By default, the lemmas \verb=proj1=, \verb=proj2=, \verb=sym_equal=
and \verb=sym_eqT= are declared implicit. To remove a lemma or a theorem
previously declared as implicit, say \verb=lem1=, use the command

\comindex{Remove Natural}
\begin{coq_example*}
Remove Natural Implicit lem1.
\end{coq_example*}

To test if the lemma or theorem \verb=lem1= is, or is not,
declared as implicit, type

\comindex{Test Natural}
\begin{coq_example*}
Test Natural Implicit for lem1.
\end{coq_example*}

\subsubsection*{Implicit proof constructors}

Let \verb=constr1= be a proof constructor of a given inductive
proposition (or predicate)
\verb=Q= (of type \verb=Prop=). Assume \verb=constr1= proves 
\verb=(x:A)(P x)->(Q x)=. Then, applying \verb=constr1= to an hypothesis,
say \verb=H= (assuming \verb=(P a)=) produces the following kind of output:

\begin{verbatim}
...
By the definition of Q, with H we have (Q a).
...
\end{verbatim}

But sometimes, you may prefer not to see the explicit invocation to
this constructor. You may prefer to see:

\begin{verbatim}
...
With H we have (Q a).
...
\end{verbatim}

This is possible by declaring the constructor as implicit. You should
type, as before:

\comindex{Add Natural Implicit}
\begin{coq_example*}
Add Natural Implicit constr1.
\end{coq_example*}

By default, the proposition (or predicate) constructors

\verb=conj=, \verb=or_introl=, \verb=or_intror=, \verb=ex_intro=,
\verb=eq_refl= and \verb=exist=

\noindent are declared implicit. Note that declaring implicit the
constructor of a datatype (i.e. an inductive type of type \verb=Set=)
has no effect.

As above, you can remove or test a constant declared implicit.

\subsubsection*{Implicit inductive constants}

Let \verb=Ind= be an inductive type (either a proposition (or a
predicate) -- on \verb=Prop= --, or a datatype -- on \verb=Set=).
Suppose the proof proceeds by induction on an hypothesis \verb=h=
proving \verb=Ind= (or more generally \verb=(Ind A1 ... An)=). The
following kind of output is produced:

\begin{verbatim}
...
With H, we will prove A by induction on the definition of Ind.
Case 1. ...
Case 2. ...
...
\end{verbatim}

But sometimes, you may prefer not to see the explicit invocation to
\verb=Ind=. You may prefer to see:

\begin{verbatim}
...
We will prove A by induction on H.
Case 1. ...
Case 2. ...
...
\end{verbatim}

This is possible by declaring the inductive type as implicit. You should
type, as before:

\comindex{Add Natural Implicit}
\begin{coq_example*}
Add Natural Implicit Ind.
\end{coq_example*}

This kind of parameterization works for any inductively defined
proposition (or predicate) or datatype. Especially, it works whatever
the definition is recursive or purely by cases.

By default, the data type \verb=nat= and the inductive connectives
\verb=and=, \verb=or=, \verb=sig=, \verb=False=, \verb=eq=,
\verb=eqT=, \verb=ex= and \verb=exT= are declared implicit.

As above, you can remove or test a constant declared implicit.  Use
{\tt Remove Natural Contractible $id$} or {\tt Test Natural
Contractible for $id$}.

\asubsection{Contractible proof steps}

\subsubsection*{Contractible lemmas or constructors}

Some lemmas, theorems or proof constructors of inductive predicates are
often applied in a row and you obtain an output of this kind:

\begin{verbatim}
...
Using T with H1 and H2 we get P.
      * By H3 we have Q.
      Using T with theses results we get R.
...
\end{verbatim}

where \verb=T=, \verb=H1=, \verb=H2= and \verb=H3= prove statements
of the form \verb=(X,Y:Prop)X->Y->(L X Y)=, \verb=A=, \verb=B= and \verb=C=
respectively (and thus \verb=R= is \verb=(L (L A B) C)=).

You may obtain a condensed output of the form

\begin{verbatim}
...
Using T with H1, H2, and H3 we get R.
...
\end{verbatim}

by declaring \verb=T= as contractible:

\comindex{Add Natural Contractible}
\begin{coq_example*}
Add Natural Contractible T.
\end{coq_example*}

By default, the lemmas \verb=proj1=, \verb=proj2= and the proof
constructors \verb=conj=, \verb=or_introl=, \verb=or_intror= are
declared contractible. As for implicit notions, you can remove or
test a lemma or constructor declared contractible.

\subsubsection*{Contractible induction steps}

Let \verb=Ind= be an inductive type. When the proof proceeds by
induction in a row, you may obtain an output of this kind:

\begin{verbatim}
...
We have (Ind A (Ind B C)).
We use definition of Ind in a study in two cases.
Case 1: We have A.
Case 2: We have (Ind B C).
  We use definition of Ind in a study of two cases.
  Case 2.1: We have B.
  Case 2.2: We have C.
...
\end{verbatim}

You may prefer to see

\begin{verbatim}
...
We have (Ind A (Ind B C)).
We use definition of Ind in a study in three cases.
Case 1: We have A.
Case 2: We have B.
Case 3: We have C.
...
\end{verbatim}

This is possible by declaring \verb=Ind= as contractible:

\begin{coq_example*}
Add Natural Contractible T.
\end{coq_example*}

By default, only \verb=or= is declared as a contractible inductive
constant.
As for implicit notions, you can remove or test an inductive notion declared
contractible.

\asubsection{Transparent definitions}

``Normal'' definitions are all constructions except proofs and proof constructors.

\subsubsection*{Transparent non inductive normal definitions}

When using the definition of a non inductive constant, say \verb=D=, the
following kind of output is produced:

\begin{verbatim}
...
We have proved C which is equivalent to D.
...
\end{verbatim}

But you may prefer to hide that D comes from the definition of C as
follows:

\begin{verbatim}
...
We have prove D.
...
\end{verbatim}

This is possible by declaring \verb=C= as transparent:

\comindex{Add Natural Transparent}
\begin{coq_example*}
Add Natural Transparent D.
\end{coq_example*}

By default, only \verb=not= (normally written \verb=~=) is declared as
a non inductive transparent definition.
As for implicit and contractible definitions, you can remove or test a
non inductive definition declared transparent.
Use \texttt{Remove Natural Transparent} \ident or 
\texttt{Test Natural Transparent for} \ident.

\subsubsection*{Transparent inductive definitions}

Let \verb=Ind= be an inductive proposition (more generally: a
predicate \verb=(Ind x1 ... xn)=). Suppose the definition of
\verb=Ind= is non recursive and built with just
one constructor proving something like \verb=A -> B -> Ind=.
When coming back to the definition of \verb=Ind= the
following kind of output is produced:

\begin{verbatim}
...
Assume Ind (H).
      We use H with definition of Ind.
      We have A and B.
      ...
\end{verbatim}

When \verb=H= is not used a second time in the proof, you may prefer
to hide that \verb=A= and \verb=B= comes from the definition of
\verb=Ind=. You may prefer to get directly:

\begin{verbatim}
...
Assume A and B.
...
\end{verbatim}

This is possible by declaring \verb=Ind= as transparent:

\begin{coq_example*}
Add Natural Transparent Ind.
\end{coq_example*}

By default, \verb=and=, \verb=or=, \verb=ex=, \verb=exT=, \verb=sig=
are declared as inductive transparent constants.  As for implicit and
contractible constants, you can remove or test an inductive
constant declared transparent.

As for implicit and contractible constants, you can remove or test an
inductive constant declared transparent.

\asubsection{Extending the maximal depth of nested text}

The depth of nested text is limited. To know the current depth, do:

\comindex{Set Natural Depth}
\begin{coq_example}
Set Natural Depth.
\end{coq_example}

To change the maximal depth of nested text (for instance to 125) do:

\begin{coq_example}
Set Natural Depth 125.
\end{coq_example}

\asubsection{Restoring the default parameterization}

The command \verb=Set Natural Default= sets back the parameterization tables of
\Natural~ to their default values, as listed in the above sections.
Moreover, the language is set back to English and the max depth of
nested text is set back to its initial value.

\asubsection{Printing the current parameterization}

The commands {\tt Print Natural Implicit}, {\tt Print Natural
Contractible} and {\tt Print \\ Natural Transparent} print the list of
constructions declared {\tt Implicit}, {\tt Contractible},
{\tt Transparent} respectively.

\asubsection{Interferences with \texttt{Reset}}

The customization of \texttt{Natural} is dependent of the \texttt{Reset}
command. If you reset the environment back to a point preceding an
\verb=Add Natural ...= command, the effect of the command will be
erased. Similarly, a reset back to a point before a 
\verb=Remove Natural ... = command invalidates the removal.

\asection{Error messages}

An error occurs when trying to \verb=Print=, to \verb=Add=, to
\verb=Test=, or to \verb=remove= an undefined ident. Similarly, an
error occurs when trying to set a language unknown from \Natural.
Errors may also occur when trying to parameterize the printing of
proofs: some parameterization are effectively forbidden.
Note that to \verb=Remove= an ident absent from a table or to
\verb=Add= to a table an already present ident does not lead to an
error.

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "Reference-Manual"
%%% End: