Stream: math-comp users

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


view this post on Zulip Mukesh Tiwari (May 17 2022 at 17:08):

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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Karl Palmskog (May 19 2022 at 17:59):

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

view this post on Zulip 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 induction but an abstract type R with field axioms.

view this post on Zulip 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).


Last updated: Jan 29 2023 at 19:02 UTC