3

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

x : phantom (GRing.Zmodule.class_of ?bT) (GRing.Zmodule.class ?bT) 术语“x”的类型为“phantom (GRing.Zmodule.class_of ?bT) (GRing.Zmodule.class ?bT)”，而预计其类型为“phantom (GRing.Zmodule.class_of 'I_n) ?b”。

这就是我到目前为止所拥有的，我能够定义操作并实例化 abelian 组 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为基础。

4

1 回答 1

2

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

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

(* ... *)

Definition foo := 'I_n.

(* ... *)

Definition ordn_ZmodType := ZmodType foo Mixin.

(* ... *)

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

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

Check fun n => [ringType of 'I_n.+2].
(* ... : nat -> ringType *)
于 2019-11-06T03:02:23.667 回答