Создание коммутативного кольца Zn с помощью mathcomp - PullRequest
Новая
       70

Создание коммутативного кольца Zn с помощью mathcomp

3 голосов
/ 05 ноября 2019

Мне удалось создать ComRingMixin, но когда я пытаюсь объявить этот тип как каноническое кольцо, Coq жалуется:

x: phantom (GRing.Zmodule.class_of? BT)(GRing.Zmodule.class? BT) Термин "x" имеет тип "фантом (GRing.Zmodule.class_of? BT) (GRing.Zmodule.class? BT)", в то время как ожидается, что он будет иметь тип "фантом (GRing.Zmodule.class_of 'I_n)? b ".

Это то, что у меня есть, я смог определить операции и создать миксин абелевой группы, а также каноническое объявление, но для кольца, мой код не работает. 

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 / groups / marelle / advanced-coq-17 / lesson5.html .

1 Ответ

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

Проблема в том, что ssralg уже объявляет ordinal как экземпляр zmodType. Может быть только один канонический экземпляр структуры на символ головы, поэтому ваше объявление ordn_ZmodType фактически игнорируется.

Единственное решение вокруг этого - ввести локальный синоним в этом разделе и использовать его для определенияканонические структуры: 

(* ... *)

Definition foo := 'I_n.

(* ... *)

Definition ordn_ZmodType := ZmodType foo Mixin.

(* ... *)

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

Другое решение заключается в использовании экземпляра ringType, определенного в MathComp для ordinal. Подвох в том, что он определен только для типов вида 'I_n.+2. В принципе, можно было бы также объявить эти случаи, приняв те же аксиомы на n, что и вы, но это усложнило бы вывод канонических структур. 

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