Как мне использовать лемму из библиотеки Coq?

Question

Я пытаюсь использовать лемму eqb_sym из этой библиотеки: https://coq.inria.fr/library/Coq.Structures.Equalities.html

Я попытался «Требовать импорта Coq.Structures.Equalities».и «Требовать импорта BoolEqualityFacts», но ни один не позволяет мне использовать лемму eqb_sym.Coq жалуется, что не может найти лемму в текущей среде.В общем, когда я нахожу лемму, которую я хотел бы использовать из библиотеки в https://coq.inria.fr/library/,, где я могу найти подходящий модуль для импорта, и является ли "Require Import Module-Name" правильным способом его использования?

Answer 1

Лемма 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.