如何在 Coq 中定义特定字段

Question

我正在尝试在 Coq 中使用标准库定义的字段在标准库的布尔实现上构建 GF(2)。

要明确：

"true" 应该是字段的“1”元素。
"false" 应该是字段的“0”元素。
"xorb"应该是附加的。
"andb"应该是乘法。

我希望我必须将此信息传递给来自 here 的某些记录并提供正确性证明。但是，我不知道如何设置它。

Answer 1

在标准库的字段结构中，首先需要展示这个字段所在的环结构。对于这个环形结构，我们需要弄清楚什么是相反的功能，什么是减法的功能。答案是：对面是恒等函数，减法也是xorb。所以我们首先要表示false、true、xorb、andb、xorb、(fun x => x)构成一个环。在 Coq 的例子中，我们还需要指定我们将使用什么等价关系来识别环的两项，在这种情况下我们选择简单的等式 @eq bool。要描述这样一个环形结构，我们需要创建一个类型的对象。

 Ring_theory.ring_theory false true xorb andb xorb (fun x => x) (@eq bool).

最简单的方法是只说我们想做，不提供结构的值，并使用证明模式来帮助发现所有需要验证的命题。

Definition GF2_ring :
   Ring_theory.ring_theory false true xorb andb xorb (fun x => x) (@eq bool).

系统的回答只是重复预期的类型。我们现在可以告诉 Coq 我们想要应用记录构造函数。

apply Ring_theory.mk_rt.

这创建了 9 个目标，每个目标验证环的预期属性之一：中性元素属性、结合性、交换性、分配性和相反函数的属性。

您可以搜索表达所有这些属性的现有定理，但另一种可能性是通过检查所有变量的所有可能情况来验证这些属性。这是在以下完整证明中完成的。

Require Import Field.

Definition GF2_ring :
   Ring_theory.ring_theory false true xorb andb xorb (fun x => x) (@eq bool).
Proof.
apply Ring_theory.mk_rt;
  solve[now intros [] | now intros [] [] | now intros [] [] []].
Qed.

可以使用类似的证明结构来完成字段结构。

Definition GF2_Field :
  field_theory false true xorb andb xorb (fun x => x) andb (fun x => x) (@eq bool).
constructor; try solve[exact GF2_ring | now easy ].
now intros [] abs; auto; try case abs.
Qed.

现在，什么给了你？ ring_theory 和 field_theory 实际上是实现 ring 和 field 策略的中间工具。所以你可以在 Add Field 命令中使用对象 GF2_Field，但是在 GF(2) 的情况下，这些策略不如在数字字段的情况下有用。

如果您对代数结构感兴趣，我认为您应该看看 mathematical components or math classes.

这样的发展

如何在 Coq 中定义特定字段

How to define a specific field in Coq

coq

abstract-algebra