时间戳

首页 > 解决方案 > 如何使用 Coq 库中的引理？

coq - 如何使用 Coq 库中的引理？

问题描述

我正在尝试使用此库中的引理 eqb_sym： https ://coq.inria.fr/library/Coq.Structures.Equalities.html

我试过“需要导入 Coq.Structures.Equalities”。和“需要导入 BoolEqualityFacts”，但也不让我使用引理 eqb_sym。Coq 抱怨它在当前环境中找不到引理。一般来说，当我从https://coq.inria.fr/library/的库中找到我想使用的引理时，我在哪里可以找到要导入的正确模块并且是“需要导入模块名称”正确的使用方法？

标签： coq

解决方案

eqb_sym引理在由类型模块参数化的函子内定义BooleanEqualityType'。要使用它，您必须实例化该函子并导入它。以下是标准自然数类型的可能用途nat：

Require Import Coq.Structures.Equalities.

(* We are defining an implementation of a module of
   type BooleanEqualityType'. You can check what fields are required
   by asking Coq to print BooleanEqualityType'. *)
Module N <: BooleanEqualityType'.

Definition t := nat.
Definition eq := @eq nat.
Lemma eq_equiv : Equivalence eq.
Proof. split; congruence. Qed.
Definition eqb := Nat.eqb.
Lemma eqb_eq : forall n m, eqb n m = true <-> eq n m.
Proof. (* Fill in here *) Admitted.

End N.

(* Instantiate the generic lemmas for our implementation *)
Module Import NBoolEqualityFacts := BoolEqualityFacts(N).

(* We can now use the lemma *)
Check eqb_sym.

推荐阅读