0

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

要清楚：

  • “true”应该是字段的“1”元素。

  • “false”应该是字段的“0”元素。

  • “xorb”应该是addititon。

  • “andb”应该是乘法。

我希望我应该从这里将这些信息传递给一些记录并提供正确性证明。但是，我不知道如何设置它。

4

1 回答 1

2

在标准库字段结构中，您首先需要展示该字段所在的环形结构。对于这个环结构，我们需要弄清楚什么是相反的函数，什么是减法函数。答案是：对面是恒等函数，减法也是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中间工具。因此，您可以在命令中使用对象 GF2_Field ，但在 GF(2) 的情况下，这些策略不如在数字字段的情况下有用。ringfieldAdd Field

如果您对代数结构感兴趣，我认为您应该关注诸如数学组件或数学类之类的发展。

于 2018-06-03T09:40:09.743 回答