✔ Converting Coq (normal) Field Type to math-comp fieldType · math-comp users

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.

Mukesh Tiwari (May 19 2022 at 07:11):

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.

Mukesh Tiwari (May 19 2022 at 17:51):

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.

Karl Palmskog (May 19 2022 at 17:59):

Mukesh Tiwari (May 19 2022 at 18:03):

@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.

Mukesh Tiwari (May 19 2022 at 18:07):

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).

Notification Bot (May 21 2022 at 10:33):

Karl Palmskog (May 21 2022 at 11:32):

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

Mukesh Tiwari (May 21 2022 at 12:09):

@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).

Stream: math-comp users

Topic: ✔ Converting Coq (normal) Field Type to math-comp fieldType

Mukesh Tiwari (May 17 2022 at 17:08):