Coq 幂运算符“^”未找到

Question

我试图在 Coq 中定义一个 幂函数 ，但我似乎找不到要导入的相关模块：

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

出现以下错误：

Unknown interpretation for notation "_ ^ _".

我有点糊涂，因为在Coq.Numbers.NatInt.NZPow里面，我看到了下面的描述：

Interface of a power function, then its specification on naturals

还有这个：

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

那我错过了什么？

Answer 1

所有NZ mod规则都包含公理化。他们指定 properties 函数，例如 pow 而没有实际定义它们。他们通过使用 Modules 来做到这一点。一个Module是定义、符号等的集合，这些定义的名称和类型等组成一个Module Type。您可以 "open" a Module 并通过 Importing 使用其中的任何内容，但要做到这一点，您需要拥有 a mod首先是正确类型的规则。

Pow A 是 pow : A -> A -> A 的实现类型，PowNotation 是包含符号 Infix "^" := pow 的 mod 规则的类型。如果你有一个 Module 类型（或超类型！）PowNotation，你可以 Import 那个 module 得到那个符号。但是，同样，由于 NZ mod 规则只是公理化，它们不会给你这样的 mod 规则，所以你 还没有 导入任何能给你那种符号的东西。你可以直接导入一个actual实现：

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.

或者您可以对正在使用的数字系统进行抽象（因此它可以是一元 nats，或者二进制自然数，或者整数，或者整数 mod 一些数字，等等。 ), 与所有 NZ mod 规则在数字系统上的抽象相同：

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.

Answer 2

(TLDR; 您只需 Require Import Nat. 即可获得 nat 的 pow 定义和符号。

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

)

问题是您正在尝试使用模块 type 而不是模块。

NZPow的抽象接口需要针对具体的类型进行实例化。在 nat 的情况下，它已经在 NPeano 的库中完成。它只是取 "old" PeanoNat.Nat 中已经定义的东西，所以它很短。顺便说一句，注意弃用警告...

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

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

Module Nat <: NAxiomsSig := Nat.

无论如何，如果你坚持要使用这个，你应该导入NPeano，这是一个模块，具体实现了nat的NAxsiomsSig模块类型。它只会为您提供与 Require Import Nat. 相同的功能。您可以看到它们在定义上确实与

相同的功能

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

（Numbers 自 2011 年以来似乎没有受到太多关注，所以也许您应该为您的工作使用更多维护的东西。OTOH，在过去的 130 亿多年里，自然数也几乎没有变化, 所以...)

Coq 幂运算符“^”未找到

Coq power operator "^" unfound

coq

exponential