Coq导入问题 [英] Coq Import problems

问题描述

我正在尝试导入图书馆Coq.Structures.OrdersFacts ，通常使用：

I'm trying to import Library Coq.Structures.OrdersFacts as usual with:

Require Import Coq.Structures.OrdersFacts

然后我尝试在其中使用引理：
应用CompareFacts.compare_nlt_iff。或 apply compare_nlt_iff。
但是没有用……我想念什么？

Then I try to use of the lemmas there with either: apply CompareFacts.compare_nlt_iff. or apply compare_nlt_iff. But none work ... what am I missing?

推荐答案

CompareFacts 是 Module Type ，而不是 Module 。您可以看到是否这样做

CompareFacts is a Module Type, not a Module. You can see that if you do

Require Import  Coq.Structures.OrdersFacts.
Print OrdersFacts.CompareFacts.

找到这种类型的模块并应用其Lemmas。

Find a Module of this type and apply its Lemmas instead.

编辑：

我的意思是要在 nat 上使用引理，您需要模块，显示 nat 是 DecStrOrder'（和 Nat 来自 PeanoNat 就是这样的模块），也是专门针对 nat 。

I meant that to use the lemmas on i.e. nat, you need a module that shows that nat is a DecStrOrder' (and Nat from PeanoNat is such a module), and also one that specializes CompareFacts for nat .

也许一个例子更有用。

Require Import  Coq.Structures.OrdersFacts.

Module mymodule (O:DecStrOrder') (T: CompareFacts O).
  Import T.
  Import O.
  Check compare_eq_iff. (* from CompareFacts *)

  (* a theorem about terms of type O.t *)
  Lemma lem1 a b c: (a ?= b) = Eq -> b == c -> c == a. 
    intros.
    rewrite compare_eq_iff in H.  (* here we use the lemma *)
    rewrite H.
    rewrite H0.
    apply eq_equiv.
  Qed.
End mymodule.

(* the above module functor can be specialised for i.e. nat *)

Require Import PeanoNat.

Print CompareFacts.
Module M : CompareFacts Nat.
  Definition compare_eq_iff := Nat.compare_eq_iff.
  Definition compare_eq := Nat.compare_eq.
  Definition compare_lt_iff := Nat.compare_lt_iff.
  Definition compare_gt_iff := Nat.compare_gt_iff.
  Definition compare_nlt_iff := Nat.compare_nlt_iff.
  Definition compare_ngt_iff := Nat.compare_ngt_iff.
  Definition compare_refl := Nat.compare_refl.
  Definition compare_compat: Proper (eq==>eq==>eq) Nat.compare.
    intros x y Hxy a b Hab; now subst. Defined.
  Definition compare_antisym := Nat.compare_antisym.
End M.  

Module natmodule := mymodule Nat M.
Check natmodule.lem1.

这篇关于Coq导入问题的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！