16.2 Activating Natural
To enable the printing of proofs in natural language, you should type under coqtop or coqtop -full the commandCoq < Require Natural.By default, proofs are transcripted in english. If you wish to print them in french, set the french option by
Coq < Set Natural French.If you want to go back to english, type in
Coq < Set Natural English.Currently, only
French and English are available.You may see for example the natural transcription of the proof of the induction principle on pairs of natural numbers:
Coq < Print Natural nat_double_ind.You may also show in natural language the current proof in progress:
Coq < Goal (n:nat)(le O n).1 subgoal
============================
(n:nat)(le O n)
Coq < Induction n.2 subgoals
n : nat
============================
(le O O)
subgoal 2 is:
(n:nat)(le O n)->(le O (S n))
Coq < Show Natural Proof.Theorem : Unnamed_thm.
Statement : (n:nat)(le O n).
Proof :
Consider an element n of nat.
We will prove (le O n) by induction on n.
Case 1. (base):
Imagine a proof of (le O O).
Case 2. (inductive):
Imagine a proof of (n0:nat)(le O n0)->(le O (S n0)).
Q.E.D.
Restrictions
For Natural, a proof is an object of type a proposition (i.e. an object of type something of type Prop). Only proofs are written in natural language when typing Print Natural ident. All other objects (the objects of type something which is of type Set or Type) are written as usual l-terms.