16.1 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:Coq < Require Natural.Coq < Print nat_double_ind.nat_double_ind =
[R:nat->nat->Prop]
[H:(n:nat)(R O n)]
[H0:(n:nat)(R (S n) O)]
[H1:(n,m:nat)(R n m)->(R (S n) (S m))]
[n:nat]
(nat_ind [n0:nat](m:nat)(R n0 m) H
[n0:nat]
[H2:(m:nat)(R n0 m)]
[m:nat]
(nat_ind [n1:nat](R (S n0) n1) (H0 n0)
[n1:nat][_:(R (S n0) n1)](H1 n0 n1 (H2 n1)) m) n)
: (R:nat->nat->Prop)
((n:nat)(R O n))
->((n:nat)(R (S n) O))
->((n,m:nat)(R n m)->(R (S n) (S m)))->(n,m:nat)(R n m)
Piping it through the Natural pretty-printer gives:
Coq < Print Natural nat_double_ind.Theorem : nat_double_ind.
Statement : (R:nat->nat->Prop)
((n:nat)(R O n))
->((n:nat)(R (S n) O))
->((n,m:nat)(R n m)->(R (S n) (S m)))
->(n,m:nat)(R n m).
Proof :
Consider a term R of type nat->nat->Prop such that
(n:nat)(R O n) (H),
(n:nat)(R (S n) O) (H0) and (n,m:nat)(R n m)->(R (S n) (S m)) (H1);
consider an element n of nat.
We will prove (m:nat)(R n m) by induction on n.
Case 1. (base):
We use H.
Case 2. (inductive):
We know an element n0 of nat such that (m:nat)(R n0 m) (H2).
To prove (m:nat)(R (S n0) m), consider an element m of nat.
We will prove (R (S n0) m) by induction on m.
Case 2.1. (base):
From H0 we obtain (R (S n0) O).
Case 2.2. (inductive):
We know an element n1 of nat such that (R (S n0) n1) (H3).
We will prove (R (S n0) (S n1)).
From H2 we obtain (R n0 n1).
We apply now H1.
Q.E.D.