4

I am currently learning coq thanks to the Software Fondation's ebook. I successfully wrote the addition as follow:

Definition cnat := forall X : Type, (X -> X) -> X -> X.
Definition plus (n m : cnat) : cnat :=
  fun (X : Type) (f : X -> X) (x : X) => n X f (m X f x).

But I'm stuck with exp because of the following error:

Definition exp (n m : cnat) : cnat :=
  m cnat (mult n) n.
(*
In environment
n : cnat
m : cnat
The term "cnat" has type "Type@{cnat.u0+1}"
while it is expected to have type "Type@{cnat.u0}"
(universe inconsistency). 
*)

Since they wrote:

If you hit a "Universe inconsistency" error, try iterating over a different type. Iterating over cnat itself is usually problematic. I tried using the definition of cnat:

Definition exp (n m : cnat) : cnat :=
  m (forall X : Type, (X -> X) -> X) (mult n) n.

But then I have:

In environment
n : cnat
m : cnat
The term "mult n" has type "cnat -> cnat"
while it is expected to have type
 "(forall X : Type, (X -> X) -> X) -> forall X : Type, (X -> X) -> X"
(universe inconsistency).

I do not ask for a solution, but I'd really like to understand these errors. Thanks for your lights !

user4035
  • 22,508
  • 11
  • 59
  • 94
Potiron
  • 41
  • 2
  • 2
    A first step towards understanding these errors is to ask Coq to print more information so that we can actually see the culprit with `Set Printing Universes.`. These are not printed by default to keep output readable. Then to understand the error itself, note that in order to define `cnat` you are quantifying over all types in some universe `Type@{i}`. In order to keep the calculus consistent Coq has to put `cnat` in a greater universe `Type@{j}` for `i < j` (see Girard's paradox), so you cannot instantiate `cnat` with itself (what's called impredicativity). – kyo dralliam Jul 19 '20 at 10:21
  • So what's the solution to this? – Wong Jia Hau Oct 31 '20 at 09:19

1 Answers1

6

Just post the solution for others who got stuck on this problem.

Definition exp (n m : cnat) : cnat := 
  fun X => (m (X->X)) (n X).

The key is to understand m (X->X). The figure below might be helpful.

An example of 2 ^ 2

An example of 2 ^ 2

Emma
  • 27,428
  • 11
  • 44
  • 69
Liqing Yang
  • 61
  • 1
  • 4