Coq power operator "^" unfound

Question

I'm trying to define a power function in Coq, and I can't seem to find the relevant module to import:

Require Import Coq.Numbers.NatInt.NZPow.
Definition func (a b : nat) : nat := a+b*2^a.

Gives me the following error:

Unknown interpretation for notation "_ ^ _".

I'm a bit confused, because inside Coq.Numbers.NatInt.NZPow, I see the following description:

Interface of a power function, then its specification on naturals

And also this:

Module Type PowNotation (A : Typ)(Import B : Pow A).
 Infix "^" := pow.
End PowNotation.

So what am I missing?

Answer 1

(TLDR; You can to just Require Import Nat. to get the pow definition and notation for nat.

Require Import Nat.
Definition func (a b : nat) : nat := a+b*2^a.

)

The problem is that you are trying to use a module type instead of a module.

The abstract interfaces of NZPow need to be instantiated for the specific types. In the case of nat it is already done in the library in NPeano. It is just taking the already defined stuff in the "old" PeanoNat.Nat, so its very short. Btw, note the deprecation warning...

(** This file is DEPRECATED ! Use [PeanoNat] (or [Arith]) instead. *)

(** [PeanoNat.Nat] already implements [NAxiomSig] *)

Module Nat <: NAxiomsSig := Nat.

Anyway, if you insist on using this, you should import NPeano which is a module that concretely implements the NAxsiomsSig module type for nat. It will just give you the same functions you get when you do Require Import Nat. You can see they are really definitionally the same function with

Require Import Init.Nat.
Require Import NPeano.
Check eq_refl: Init.Nat.add = NPeano.Nat.add.

(The Numbers seem to not have gotten much attention since 2011, so perhaps you should use something more maintained for your work. OTOH, natural numbers have also been around unchanged for the last 13 billion plus years, so...)

Answer 2

All the NZ modules contain axiomatizations. They specify the properties of functions like pow without actually defining them. They do this by using Modules. A Module is a collection of definitions, notations, etc., and the names and types of those definitions etc. form a Module Type. You can "open" a Module and use whatever's inside by Importing it, but to do that you need to have a module of the correct type in the first place.

Pow A is the type of implementations of pow : A -> A -> A, and PowNotation is the type of modules that contain the notation Infix "^" := pow. If you have a Module that has type (or supertype!) PowNotation, you can Import that module to get at that notation. But, again, since the NZ modules are just axiomatizations, they don't give you such a module and so you haven't imported anything that gives you that notation. You can directly import an actual implementation:

Require Import PeanoNat.
(* The module Nat has type Pow nat, witnessed by Nat.pow : nat -> nat -> nat
   however, it does not have type Pow' nat, so it doesn't actually contain
   Infix "^" := pow.
   The "^" notation is just coming from PeanoNat itself. *)
Definition func (a b : nat) : nat := a+b*2^a.

Or you can abstract over the number system in use (so it could be unary nats, or the binary naturals, or the integers, or the integers mod some number, etc.), in the same way that all the NZ modules abstract over the number system:

Require Import NZAxioms.
Require Import NZPow.

Module Type NZFunc (Import A : Typ) (Import OT : OneTwo' A) (Import ASM : AddSubMul' A) (Import P : Pow' A).
Definition func (a b : t) : t := a+b*2^a.
(* t means A.t, and can be many things depending on the final implementation of this module type *)
(* 2 comes from OT, + from ASM, and ^ from P *)
End NZFunc.