16.3 Customizing Natural

16.3 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.

16.3.1 Implicit proof steps

Implicit lemmas

Applying a given lemma or theorem lem1 of statement, say A Þ B, to an hypothesis, say H (assuming A) produces the following kind of output translation:
...
Using lem1 with H we get B.
...


But sometimes, you may prefer not to see the explicit invocation to the lemma. You may prefer to see:
...
With H we have A.
...


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

Coq < Add Natural Implicit lem1.


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

Coq < Remove Natural Implicit lem1.


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

Coq < Test Natural Implicit lem1.

Implicit proof constructors

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


But sometimes, you may prefer not to see the explicit invocation to this constructor. You may prefer to see:
...
With H we have (Q a).
...


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

Coq < Add Natural Implicit constr1.


By default, the proposition (or predicate) constructors

conj, or_introl, or_intror, ex_intro, exT_intro, refl_equal, refl_eqT and exist

are declared implicit. Note that declaring implicit the constructeur of a datatype (i.e. an inductive type of type Set) has no effect.

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

Implicit inductive constants

Let Ind be an inductive type (either a proposition (or a predicate) -- on Prop --, or a datatype -- on Set). Suppose the proof proceeds by induction on an hypothesis h proving Ind (or more generally (Ind A1 ... An)). The following kind of output is produced:
...
With H, we will prove A by induction on the definition of Ind.
Case 1. ...
Case 2. ...
...


But sometimes, you may prefer not to see the explicit invocation to Ind. You may prefer to see:
...
We will prove A by induction on H.
Case 1. ...
Case 2. ...
...


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

Coq < Add Natural Implicit Ind.


This kind of parametrization 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 nat and the inductive connectives and, or, sig, False, eq, eqT, ex and exT are declared implicit.

As above, you can remove or test a constant declared implicit. Use Remove Natural Contractible id or Test Natural Contractible id.

16.3.2 Contractible proof steps

Contractible lemmas or constructors

Somme lemmas, theorems or proof constructors of inductive predicates are often applied in a row and you obtain an output of this kind:
...
Using T with H1 and H2 we get P.
      * By H3 we have Q.
      Using T with theses results we get R.
...


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

You may obtain a condensed output of the form
...
Using T with H1, H2, and H3 we get R.
...


by prealably declaring T as contractible:

Coq < Add Natural Contractible T.


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

Contractible induction steps

Let Ind be an inductive type. When the proof proceeds by induction in a row, you may obtain an output of this kind:
...
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.
...


You may prefer to see
...
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.
...


This is possible by declaring Ind as contractible:

Coq < Add Natural Contractible T.


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

16.3.3 Transparent definitions

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

Transparent non inductive normal definitions

When using the definition of a non inductive constant, say D, the following kind of output is produced:
...
We have proved C which is equivalent to D.
...


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


This is possible by declaring C as transparent:

Coq < Add Natural Transparent D.


By default, only not (normally written ~) 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 Remove Natural Transparent identor Test Natural Transparent ident.

Transparent inductive definitions

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


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


This is possible by declaring Ind as transparent:

Coq < Add Natural Transparent Ind.


By default, and, or, ex, exT, 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.

16.3.4 Extending the maximal depth of nested text

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

Coq < Set Natural Depth.
The current max size of nested text is 50


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

Coq < Set Natural Depth 125.
The max size of nested text is now 125


16.3.5 Restoring the default parametrization

The command Set Natural Default sets back the parametrization 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.

16.3.6 Printing the current parametrization

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

16.3.7 Interferences with Reset

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

Retrieved by Memoweb from http://pauillac.inria.fr/coq/doc/node.3.5.2.html at 8/10/98