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

В этой ссылке на документ есть полезные теоремы о делении. Я попытался импортировать его с помощью 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

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


module coq coqide
person Joald    schedule 17.06.2019    source источник
comment
Если можете, попробуйте использовать более новую версию Coq, чем 8.4. Доступна версия 8.9, скоро выйдет версия 8.10.   -  person eponier    schedule 19.06.2019
comment
@eponier Извините, это опечатка. Я использую 8.9.   -  person Joald    schedule 19.06.2019

Ответы (1)


arrow_upward
1
arrow_downward

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

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

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
*)
person lelf    schedule 17.06.2019