用 mathcomp 实例化 Zn 的交换环

Question

我能够创建一个 ComRingMixin，但是当我尝试将此类型声明为规范环时，Coq 抱怨：

x : phantom (GRing.Zmodule.class_of ?bT) (GRing.Zmodule.class ?bT) The term "x" has type "phantom (GRing.Zmodule.class_of ?bT) (GRing.Zmodule.class ?bT)" while it is expected to have type "phantom (GRing.Zmodule.class_of 'I_n) ?b".

这就是我目前所拥有的，我能够定义操作并实例化阿贝尔群 mixin 以及规范声明，但是对于环，我的代码失败了。

From mathcomp Require Import all_ssreflect  all_algebra.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import GRing.Theory.
Open Scope ring_scope.

Section Zn. 
 Variables n :nat.

Axiom one_lt_n : (1 < n)%N.
Axiom z_lt_n : (0 < n)%N.
Lemma mod_lt_n : forall (x : nat), ((x %% n)%N < n)%N.
Proof.
  move=> x0; rewrite ltn_mod; by exact: z_lt_n.
Qed.

Definition mulmod (a b : 'I_n) : 'I_n := Ordinal (mod_lt_n (((a*b)%N %% n)%N)).
Definition addmod (a b : 'I_n) : 'I_n := Ordinal (mod_lt_n (((a+b)%N %% n)%N)).
Definition oppmod (x : 'I_n) : 'I_n := Ordinal (mod_lt_n (n - x)%N).

Lemma addmodC : commutative addmod. Admitted.
Lemma addmod0 : left_id (Ordinal z_lt_n) addmod. Admitted.
Lemma oppmodK : involutive oppmod. Admitted.
Lemma addmodA : associative addmod. Admitted.
Lemma addmodN : left_inverse (Ordinal z_lt_n) oppmod addmod. Admitted.

Definition Mixin := ZmodMixin addmodA addmodC addmod0 addmodN.

Canonical ordn_ZmodType := ZmodType 'I_n Mixin.

Lemma mulmodA : associative mulmod. Admitted.
Lemma mulmodC : commutative mulmod. Admitted.
Lemma mulmod1 : left_id (Ordinal one_lt_n) mulmod. Admitted.
Lemma mulmod_addl : left_distributive mulmod addmod. Admitted.
Lemma one_neq_0_ord : (Ordinal one_lt_n) != Ordinal z_lt_n. Proof. by []. Qed.

Definition mcommixin := @ComRingMixin ordn_ZmodType (Ordinal one_lt_n) mulmod mulmodA mulmodC mulmod1 mulmod_addl one_neq_0_ord.

Canonical ordnRing := RingType 'I_n mcommixin.
Canonical ordncomRing := ComRingType int intRing.mulzC.

我做错了什么？我基于 http://www-sop.inria.fr/teams/marelle/advanced-coq-17/lesson5.html.

Answer 1

问题是 ssralg 已经将 ordinal 声明为 zmodType 实例。每个头符号只能有一个结构的规范实例，因此您对 ordn_ZmodType 的声明实际上被忽略了。

围绕它的一个解决方案是在本节中引入本地同义词并使用它来定义规范结构：

(* ... *)

Definition foo := 'I_n.

(* ... *)

Definition ordn_ZmodType := ZmodType foo Mixin.

(* ... *)

Canonical ordnRing := RingType foo mcommixin. (* This now works *)

另一个解决方案是使用 MathComp 中为 ordinal 定义的 ringType 实例。问题是它只为 'I_n.+2 形式的类型定义。原则上，人们也可以声明这些实例假设 n 上的公理与您所做的相同，但这会使规范结构的推断更加困难。

Check fun n => [ringType of 'I_n.+2].
(* ... : nat -> ringType *)

用 mathcomp 实例化 Zn 的交换环

Instantiating a commutative ring of Zn with mathcomp

coq

ssreflect