Как импортировать теоремы из Coq.Numbers.NatInt.NZDiv? - PullRequest
Новая
       50

Как импортировать теоремы из Coq.Numbers.NatInt.NZDiv?

0 голосов
/ 17 июня 2019

В этой ссылке документа есть полезные теоремы о делении.Я попытался импортировать его, используя Require Import в CoqIDE 8.9.0, однако, хотя импорт завершился успешно, следующий код завершился неудачно с The reference div_lt_upper_bound was not found in the current environment. 

Require Import Coq.Numbers.NatInt.NZDiv.
Check div_lt_upper_bound.

Я попытался загрузить исходный код файла и импортировать его вручнуючерез Load, но затем я получаю следующее сообщение без дальнейших объяснений (первая строка красного цвета): 

Application of a functor with too few arguments.
Interactive Module Type DivMod started
div is declared
modulo is declared
Module Type DivMod is defined
Interactive Module Type DivModNotation started
Module Type DivModNotation is defined
Module Type DivMod' is defined
Interactive Module Type NZDivSpec started
div_mod is declared
mod_bound_pos is declared
Module Type NZDivSpec is defined
Module Type NZDiv is defined

Как правильно загрузить эти теоремы?Почему предыдущие методы не сработали?

1 Ответ

1 голос
/ 17 июня 2019

Быстрый ответ: вы смотрите на Module Type (см. Print NZDivProp.).

Фактическое использование просто, e. г. 

Require Import Arith.
Check Nat.div_lt_upper_bound.
(*
     Nat.div_lt_upper_bound
          : forall a b q : nat, b <> 0 -> a < b * q -> a / b < q
*)
...