I was able to create a ComRingMixin, but when I try to declare this type as a canonical ring, Coq complains:
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".
This is what I have so far, I was able to define the operations and instantiate the abelian group mixin as well as the canonical declaration, but for the ring, my code fails.
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.
What am i doing wrong? I'm basing myself on http://www-sop.inria.fr/teams/marelle/advanced-coq-17/lesson5.html.
The problem is that ssralg already declares ordinal as a zmodType instance. There can only be one canonical instance of a structure per head symbol, so your declaration of ordn_ZmodType is effectively ignored.
One solution around it is to introduce a local synonym in this section and use it to define the canonical structures:
(* ... *)
Definition foo := 'I_n.
(* ... *)
Definition ordn_ZmodType := ZmodType foo Mixin.
(* ... *)
Canonical ordnRing := RingType foo mcommixin. (* This now works *)
The other solution is to use the ringType instance defined in MathComp for ordinal. The catch is that it is only defined for types of the form 'I_n.+2.
In principle, one could also have declared these instances assuming the same axioms on n as you did, but this would make the inference of canonical structures more difficult.
Check fun n => [ringType of 'I_n.+2].
(* ... : nat -> ringType *)