Как получить доступ к функциям внутри записи внутри модуля - PullRequest
Новая
       4

Как получить доступ к функциям внутри записи внутри модуля

0 голосов
/ 06 ноября 2019

Я пытаюсь сделать модульную арифметику в Coq. Я заметил, что есть библиотека ZModulo , которую я пытаюсь импортировать и создать модуль ZModuloCyclicType. 

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 или что-то ещепохоже.

1 Ответ

1 голос
/ 06 ноября 2019

Если вы выбрали запись, это 

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

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

Но дело в том, что ZnZ.Ops это Class, а не просто запись, ZquotZ8.ops это 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.

...