Оператор мощности Coq "^" не найден - PullRequest
Новая
       83

Оператор мощности Coq "^" не найден

3 голосов
/ 08 мая 2020

Я пытаюсь определить функцию мощности в 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 я вижу следующее описание:

Интерфейс степенная функция, затем ее спецификация на натуральных

А также это: 

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

Так что же мне не хватает?

Ответы [ 2 ]

2 голосов
/ 08 мая 2020

(TL; DR; вы можете просто Require Import Nat., чтобы получить определение pow и обозначение для nat. 

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

)

Проблема в том, что вы пытаетесь для использования модуля типа вместо модуля.

Необходимо создать экземпляры абстрактных интерфейсов NZPow для указанных c типов. В случае nat это уже сделано в библиотеке в NPeano . Он просто берет уже определенный материал в "старом" PeanoNat.Nat, поэтому он очень короткий. Кстати, обратите внимание на предупреждение об устаревании ... 

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

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

Module Nat <: NAxiomsSig := Nat.

В любом случае, если вы настаиваете на использовании этого, вы должны импортировать NPeano, который является модулем, который конкретно реализует тип модуля NAxsiomsSig для nat . Он просто предоставит вам те же функции, которые вы получаете, когда вы выполняете Require Import Nat.. Вы можете видеть, что они действительно определенно являются той же функцией с 

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

(Numbers, похоже, не привлекает большого внимания с 2011 года. , так что, возможно, вам следует использовать что-то более поддерживаемое для своей работы. OTOH, натуральные числа также оставались неизменными в течение последних 13 миллиардов с лишним лет, так что ...)

1 голос
/ 08 мая 2020

Все модули NZ содержат аксиоматизацию . Они определяют свойства таких функций, как pow, фактически не определяя их. Они делают это, используя Module s. A Module - это набор определений, обозначений и т.д. c., А также имен и типов этих определений и c. форма Module Type. Вы можете «открыть» Module и использовать все, что находится внутри, Import, но для этого вам нужно иметь модуль правильного типа в первую очередь.

Pow A - это тип реализации pow : A -> A -> A, а PowNotation - это тип модулей, которые содержат обозначение Infix "^" := pow. Если у вас есть Module с типом (или супертипом!) PowNotation, вы можете Import этот модуль, чтобы получить эту нотацию. Но, опять же, поскольку модули NZ являются просто аксиоматизацией, они не предоставляют вам такой модуль, и поэтому вы не импортировали ничего, что дает вам эту нотацию. Вы можете напрямую импортировать фактическую реализацию: 

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.

Или вы можете абстрагироваться от используемой системы счисления (так что это может быть унарный nat s, или двоичные натуральные числа, или целые числа или целые числа образуют некоторое число, et c.), точно так же, как все модули NZ абстрагируются по системе счисления: 

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.
...