Невозможно использовать NDiv coq после импорта - PullRequest
Новая
       8

Невозможно использовать NDiv coq после импорта

0 голосов
/ 10 мая 2018

Я пытаюсь использовать функциональные возможности NDiv в стандартной библиотеке coq (см. Здесь: https://coq.inria.fr/library/Coq.Numbers.Natural.Abstract.NDiv.html),, поэтому я ввожу две строки ниже в coqide: 

Require Import NDiv.
Check div_unique_exact.

Но это приводит к выводу 

Error: The reference div_unique_exact was not found in the current environment

Я не уверен, где проблема. Я также использую импорт, такой как List Arth Bool и Classical_Prop без проблем. Спасибо за любую помощь.

1 Ответ

0 голосов
/ 10 мая 2018

Обратите внимание, что NDiv начинается с 

Module Type NDivProp (Import N : NAxiomsSig')(Import NP : NSubProp N).

Весь файл обернут в эту Module Type, что означает, что каждая лемма, которую вы видите, определяется только при передаче аргументов модуля этому типу модуля.функтор.Вы, вероятно, хотите что-то вроде Require Import NArith. (или Require Import ZArith.), откуда вы можете увидеть, может ли Coq найти div_unique_exact с Locate.Если я сделаю 

Require Import Coq.NArith.NArith.
Locate div_unique_exact.

, я получу 

Constant Coq.NArith.BinNat.N.div_unique_exact
  (shorter name to refer to it in current context is N.div_unique_exact)
Constant Coq.ZArith.BinInt.Z.Private_Div.NZQuot.div_unique_exact
  (shorter name to refer to it in current context is BinInt.Z.Private_Div.NZQuot.div_unique_exact)
Constant Coq.Arith.PeanoNat.Nat.div_unique_exact
  (shorter name to refer to it in current context is PeanoNat.Nat.div_unique_exact)
Constant Coq.NArith.BinNat.N.Private_NZDiv.div_unique_exact
  (shorter name to refer to it in current context is N.Private_NZDiv.div_unique_exact)
Constant Coq.Arith.PeanoNat.Nat.Private_NZDiv.div_unique_exact
  (shorter name to refer to it in current context is PeanoNat.Nat.Private_NZDiv.div_unique_exact)
Constant Coq.ZArith.BinInt.Z.Private_NZDiv.div_unique_exact
  (shorter name to refer to it in current context is BinInt.Z.Private_NZDiv.div_unique_exact)
Constant Coq.ZArith.BinInt.Z.div_unique_exact
  (shorter name to refer to it in current context is BinInt.Z.div_unique_exact)

, и мы увидим, что первая запись показывает, что следующее будет успешным: 

Check N.div_unique_exact.
...