3

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.

Anton Trunov
  • 15,074
  • 2
  • 23
  • 43
gtaumaturgo
  • 33
  • 3

1 Answers1

2

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 *)
Arthur Azevedo De Amorim
  • 23,012
  • 3
  • 33
  • 39
  • Thank you! Your solution worked. I am working on the mechanisation of an algorithm called AKS, and it's proof of correctness relies a lot on algebraic structures. If you don't mind, I have another question. I wanted to define this ring so I could define the following Lemma: (I defined 'I_n as Zn) ``` Lemma agrawal_biswas: forall (n : nat) (a : Zn), prime n == (('X + a%:P)^+n == 'X^n + a%:P).``` – gtaumaturgo Nov 06 '19 at 04:35
  • Its a lemma about polynomials, and to use a polynomial type, the coefficients must be a ring so i did this because i could not do it using 'I_n, but i was able to do it with 'I_2, 'I_3, ..., but not with 'I_n. Do you know why this happens? – gtaumaturgo Nov 06 '19 at 04:38
  • 2
    @gtaumaturgo The `n` must be of the form `m.+2`. This happens because rings in math comp must satisfy `1 != 0`. – Arthur Azevedo De Amorim Nov 06 '19 at 13:00