如何从Coq.Numbers.NatInt.NZDiv中导入定理? [英] How to import theorems from Coq.Numbers.NatInt.NZDiv?

问题描述

在此文档链接中，有一些有用的定理分配.我尝试使用CoqIDE 8.9.0中的 Require Import 导入它，但是，虽然导入成功，但以下代码失败，并显示在当前环境中找不到参考div_lt_upper_bound.

In this doc link there are useful theorems about division. I tried importing it using Require Import in CoqIDE 8.9.0, however while the import succeeds, the following code fails with 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 手动导入，但是随后得到以下消息，没有进一步说明(第一行为红色):

I tried downloading the source code for the file and manually importing it via Load, but then I get the following message with no further explanation (the first line is in red):

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

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

How do I load those theorems properly? Why did the previous methods not work?

推荐答案

快速答案是您正在查看模块类型(请参见打印NZDivProp.).

The quick answer is that you are looking at the Module Type (see Print NZDivProp.).

实际用法很简单，例如.g.

The actual usage is simple, 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
*)

这篇关于如何从Coq.Numbers.NatInt.NZDiv中导入定理?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！