时间戳

首页 > 解决方案 > 如何从 Coq.Numbers.NatInt.NZDiv 导入定理？

module - 如何从 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

如何正确加载这些定理？为什么以前的方法不起作用？

标签： modulecoqcoqide

解决方案

快速的回答是您正在查看Module Type（请参阅 参考资料Print NZDivProp.）。

实际用法很简单，e。G。

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
*)

推荐阅读