时间戳

首页 > 解决方案 > 如何访问模块内记录中的函数

coq - 如何访问模块内记录中的函数

问题描述

我正在尝试在 Coq 中进行模运算。我注意到我尝试导入和创建模块的ZModuloZModuloCyclicType库。

Require Import Utf8_core.
Require Import ZArith_base.
Require Import Coq.Numbers.Cyclic.ZModulo.ZModulo.

Ltac positive_ne1 :=
  match goal with
  | [ |- ?p ≠ 1%positive ] => unfold not; intro H; inversion H
  end.

Module Positive8 : PositiveNotOne.
  Definition p := 8%positive.
  Theorem not_one : p ≠ 1%positive. 
  Proof. positive_ne1. Qed.
End Positive8.
Module ZquotZ8 := ZModuloCyclicType(Positive8).
Export ZquotZ8.

现在，我想访问succ记录中的操作Instance zmod_ops : ZnZ.Ops Z := ZnZ.MkOps。然而，

Check ZquotZ8.ops.succ. (* Error: The reference ZquotZ8_ops.succ was not found in the current environment. *)
Check ZquotZ8.ops.(succ). (* Error: The term "ops" has type "ZnZ.Ops t" while it is expected to have type "Z". *)

Definition ZquotZ8_ops : ZnZ.Ops Z := zmod_ops 8.
Check ZquotZ8_ops.succ. (* Error: The reference ZquotZ8_ops.succ was not found in the current environment. *)
Check ZquotZ8_ops.(succ). (* Error: The term "ZquotZ8_ops" has type "ZnZ.Ops Z" while it is expected to have type "Z". *)

我的问题是：如何访问此实例succ而不是中定义的实例Coq.Numbers.Cyclic.ZModulo.ZModulo.？

我想要的是Compute succ_Z8 255 = 0%Z : Z或类似的东西。

标签： coq

解决方案

如果您设置了记录选择，它是

Require Import Coq.Numbers.Cyclic.Abstract.CyclicAxioms.

ZquotZ8.ops.(@ZnZ.succ _)
(* equivalent to *)
@ZnZ.succ _ ZquotZ8.ops

但是，问题是，ZnZ.Opsis a Class，而不仅仅是一条记录，ZquotZ8.opsis an Instance，并且ZnZ.succ可以ZquotZ8.ops隐式找到，因为您使用过Export ZquotZ8. 所以这只是

ZnZ.succ

但是，我认为您还需要将标题更改Positive8为

(* NOT            : *)
Module Positive8 <: PositiveNotOne.

否则，Positive8.p它是不透明的，你不能用它来计算。一旦完成，你得到

Compute (ZnZ.compare (ZnZ.succ 255%Z) 0%Z).
(* = Eq *)

注意succ不会翻车；在这里，它返回256%Z。ZnZ.to_Z实际上会计算余数，或者您可以使用succ_c.

推荐阅读