Hi everyone, I want to convert a `Type`

with `Field`

axioms to `fieldType`

of math-comp. Is there a way to do this? I don't know how to construct `GRing.Field.mixin_of (GRing.UnitRing.Pack ?base)`

. My understanding for `?base`

is that it's a record with two things: `sort`

--which I have already instantiated with `R`

and a hypothesis `GRing.UnitRing.class_of sort `

but I can't split it to get those values separately. (Btw, this is very interesting because so far I have never seen any project where `Type`

is also hidden within a structure)

```
Require Import Field_theory
Ring_theory List NArith
Ring Field Utf8 Lia
Coq.Arith.PeanoNat
Vector Fin Lia .
From mathcomp Require Import
all_ssreflect algebra.matrix
algebra.ssralg.
Import ListNotations.
Set Implicit Arguments.
Section Computation.
Variable
(R : Type)
(rO rI:R)
(radd rmul rsub : R -> R -> R)
(ropp : R -> R)
(rdiv : R -> R -> R)
(rinv : R -> R)
(rfield :
field_theory rO rI radd rmul rsub ropp rdiv rinv eq).
Lemma Rfield : fieldType.
Proof.
econstructor.
(* My goal is GRing.Field.class_of ?sort *)
Print GRing.Field.class_of.
(*
Record class_of (F : Type) : Type := Class
{ base : GRing.IntegralDomain.class_of F;
mixin : GRing.Field.mixin_of (GRing.UnitRing.Pack base) }.
*)
instantiate (1 := R).
econstructor.
Print GRing.UnitRing.Pack.
(*
Record type : Type := Pack
{ sort : Type; _ : GRing.UnitRing.class_of sort }.
*)
Print GRing.Field.mixin_of.
(*
λ R : unitRingType, ∀ x : R, x != 0%R → x \is a GRing.unit
: unitRingType → Prop
*)
Admitted.
End Computation.
```

After a bit of trial and error, I feel that `ZmodMixing Check (@ZmodMixin R rO ropp radd).`

can be helpful (I get this idea from here). I haven't finished the proof (construction) yet but I feel it should be very similar. If you have any other example link, feel free to let me know.

Hi everyone, I made a bit of progress in construction but now I am stuck with `choiceType`

. I don't know how to get `choiceType`

for type `Field R`

. Once I get past this, I feel it will be fairly straight forward by just following this.

```
Section Computation.
Variable
(R : Type)
(rO rI:R)
(radd rmul rsub : R -> R -> R)
(ropp : R -> R)
(rdiv : R -> R -> R)
(rinv : R -> R)
(Radd_0_l: ∀ x : R, radd rO x = x)
(Radd_comm: ∀ x y : R, radd x y = radd y x)
(Radd_assoc: ∀ x y z : R,
radd x (radd y z) =
radd (radd x y) z)
(Rmul_1_l: ∀ x : R, rmul rI x = x)
(Rmul_comm: ∀ x y : R, rmul x y = rmul y x)
(Rmul_assoc: ∀ x y z : R,
rmul x (rmul y z) =
rmul (rmul x y) z)
(Rdistr_l: ∀ x y z : R,
rmul (radd x y) z =
radd (rmul x z) (rmul y z))
(Rsub_def: ∀ x y : R,
rsub x y = radd x (ropp y))
(Ropp_def: ∀ x : R, radd x (ropp x) = rO)
(F_1_neq_0: rI ≠ rO)
(Fdiv_def: ∀ p q : R,
rdiv p q = rmul p (rinv q))
(Finv_l: ∀ p : R,
p ≠ rO → rmul (rinv p) p = rI)
(Hdec : forall r1 r2 : R, {r1 = r2} + {r1 <> r2}).
(* rfield :
field_theory rO rI radd rmul rsub ropp rdiv rinv eq *)
Lemma radd_assoc : associative radd.
Proof.
move =>x y z.
apply Radd_assoc.
Qed.
Lemma radd_comm : commutative radd.
Proof.
move =>x y.
apply Radd_comm.
Qed.
Lemma radd_left_id : left_id rO radd.
Proof.
move => x.
apply Radd_0_l.
Qed.
Lemma radd_left_inv : left_inverse rO ropp radd.
Proof.
move =>x.
rewrite Radd_comm.
apply Ropp_def.
Qed.
Definition R_zmodmixin :=
ZmodMixin radd_assoc radd_comm radd_left_id radd_left_inv.
(*I don't know how to get choiceType *)
Canonical R_zmodtype := ZmodType R R_zmodmixin.
```

@Mukesh Tiwari have you tried looking at if this can help? https://github.com/arthuraa/deriving

@Karl Palmskog No, I haven't looked at it, but I am not sure if it will be helpful in my case `The Deriving library builds instances of basic MathComp classes for inductive data types`

. My type is not inductive but an abstract type `R`

with `field`

axioms.

But I am glad I am going through this pain because it forcing me to learn/explore bits and pieces here and there :) (I must admit it's a bit frustrating but I understand that the learning curve for math-comp is steep).

Mukesh Tiwari has marked this topic as resolved.

@Mukesh Tiwari I think the community would appreciate if you posted a link to your solution (e.g., use GitHub Gist)

@Karl Palmskog It was simple but very informative. I followed this Rstruct.v from the FFS-CoqRK-FP. I used Coq.Logic.Epsilon to get the choiceType, same as the FFS-CoqRK-F library. Here is the gist, but it still has few admits because there is nothing in (normal) Field type about the interaction between 0 (rO) and * (rmul).

Last updated: Jul 15 2024 at 21:02 UTC