coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] ChoiceType for Coq Type with Field Axioms

From: mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] ChoiceType for Coq Type with Field Axioms
Date: Thu, 19 May 2022 19:51:37 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mukeshtiwari.iiitm AT gmail.com; spf=Pass smtp.mailfrom=mukeshtiwari.iiitm AT gmail.com; spf=None smtp.helo=postmaster AT mail-ej1-f50.google.com
Ironport-data: A9a23:Ar+fEq3MX4Vo1Tsyy/bD5ex3kn2cJEfYwER7XKvMYLTBsI5bp2NVm 2pNXWqDbK6NYGH2fdgnOYzgpE9Qv5+Hnd4wQQtv3Hw8FHgiRejtVY3IdB+oV8+xBpSeFxw/t 512hv3odp1coqr0/0/1WlTZhSAgk/nOHNIQMcacUsxLbVYMpBwJ1FQywobVvqYy2YLjW17U6 IuryyHiEAbNNwBcYjp8B52r80sHUMTa4Fv0aXRjDRzjlAa2e0g9VPrzF4npR5fLatU88tqBe gr25OrRElU1UPsaIojNfr7TKiXmS1NJVOSEoiI+t6OK2nCuqsGuu0o2HKJ0VKtZt9mGt/N8l /hIjsyBcAI0I7Xlhus0dQVGNBgraMWq+JefSZS+mcmazkmDfnm1hvszVAc5OooX/usxCmZLn RAaAGpVP1bT2qTsmeL9F7EEascLdKEHOKsap3Jt1jHFDOkvW5GFQqTL+dpw0zI5h8QIFvHbD yYcQWMzMUSQM0AQUrsRIJsdxt6QjWj7STZz8H+fhJts4WrBkjUkhdABN/KMIoDQLSlPpW6To XuD9GDkCDkBJdmHwHyE9Gitj6nBh0vGtJk6EbS58rtnggTWyDFLThIRUlS/rL+yjUvWt89jx 1I82SdxgK0JpH2SS8TgRzSmr1eiogA7Yo8FewEl0z2lxq3R6gefI2ELSD9dddAr3PPaoxR6h zdlePu5VVRSXK2ppWG1rejL8GvjUcQBBSpTOn9eFFptD8zL+dlr1nryosBf/LlZZ+AZ9Bn1y jGO6SU83vAd0JZN2KK88lTKxTmro/AlrzLZBC2HAQpJDSsjPOZJgrBED3CFs56sy67HEDG8U IAswZT20Qz3JcjleNaxaOsMBqq1wP2OLSfRh1Vid7F4qWn3qyf5J9oPuG4lTKuMDiriUW+4C KM0kVMBjKK/wFP3BUOKS9nsV5l6kvSI+SrND6mMNoMmjmdNmP+vpXkyPyZ8Lkjil08jlaxXB HtoWZfEMJruMow+lGDeb75Fj9cDn3lirUuOG82T50n4idK2OS/NIZ9YYQDmRr1ovMus/l+Jm /4BbJDi40sEAIXDjtz/q9F7waYidihlW/gbaqV/Koa+H+aRMDhxVKCKmel5IOSIXc19z4/1w 510YWcAoHKXuJENAVzihqlLZOy9UJBhg2g8OCBwb1+k12JyM4mq5aYbMZAweOB/puBkyPd1S dgDetmBUqwfEGSZp2xFYMmvtpFmeTSqmRmKYHiobT05SJhqGF7E99riSQ3w+XRcFSGwr8Y// +at21qDE5oOTghvFujMb/erww/jtHQRgrMgUE7BI90Vc0LpqdA4Jyv0h/4xAscNNRSTnmvAh 1jKWU8V/LCfrZU0/d/FgbG/g72oS+YuTFBHG2T77KqtMXaI82emx7hGWrnacD3YUlTy5/z+N +hYyvfLMMoHkkxPhIxyHus51qk5/dbu++ZXwwk4TnXGa1OnVuFpLnWch5Ids6RMwvpUu1LzV B/XvNZdPrqNNYXuF1tIfFgpaeGK1Pc1nDjO7KRqfB+runcvpLfXA19POxSsiTBGKOcnOo0Sx +p86tUd7Bayi0Z3P9va3DpY8X+Aci4JX6k97MpIBYbqjk8myAgHb8GETCDx556LZpNHNUxze m2Yg6/LhrJ9wEvecipsSSKcg7IF3Zle6gpXyFIiJkiSnoaXjPEA2hAMoy88SR5Yz0ka3u9+U oSx25aZ+UlTE/ZUaMl/s6SEHghAAFiU+BW0xQZR0mLeSEasWyrGK2hV1SNhOqwG2zo0Q9SZ1 OjwJKXZvfLCc8T43y90UklgwxAmZcIk7RXMwahLAOzcd6TXolPZbmuGam8Bqh+hCsQ07KECS S+G484oAZDG2eUsT2HXxmVUOXn8iPxJGYCafcxcwQ==
Ironport-hdrordr: A9a23:e1D836Oh6LVEJ8BcTsKjsMiBIKoaSvp037BN7TEWdfU1SL3+qy nKpp4mPHDP+VUssR0b+exoW5PgfZq/z+8W3WB5B97LNzUO01HYSb2Kg7GSpwEI2BeTygee78 pdmmRFZ+EYxGIVsfrH
Ironport-phdr: A9a23:uLM0/RHAvwFiR9nF04D3ZZ1Gf4pGhN3EVzX9CrIZgr5DOp6u447ld BSGo6k31xmXBM6Csa0MotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7G MNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+5ZPebx9JiTagbr9+M Qu6oAfMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2Q rxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6 bpgRh31hycdLzM2/2HZhMJzgqxGvhyuuxNxzpXIYIGMLvdyYr/Rcc8YSGdHQ81fVzZBAoS5b 4YXCuoBIOVYoJfmp1sOsBC+GQisBe31xT9Sh3/9wKo30+E8EQHFwgMgBNIOsGjVrNT7LqgSS +G1wLPJzTXCbvNWxTL95ZPHchAku/6MXLZwfdDNxkkoEgPIl1OdopHqMD2JzOoCqXSb7/Z+W uK1jW4qsx18rzihyMswioTHiYIbx1/E+yllwIs4Id+1Rk56bNOkE5ZeuCGXOoloT84tTW9lu Dg2xqAbtJOmYSUH1pcqyRHZZveafYaI5RfjW/yQITd+nH9ld7O/hwqy8Ui90eLwTNW70FFPr idDj9LCtWgN2gTN5sSbTvZx5ESs1DaV2wzN9+1JIlo4mKrHJ5Mn37U+jIAcsV7ZES/zgEj2j LGZdkEj+uWw7uToeLTmppuFO4BqiAHyL70imsK/DOgkKAQOUG+b+eOz1L3n40L1WqlFjvozk qXBsZDaI9oUprKhDgNLzoou7wyzAjSm3dgCg3ULMVFIdAiHgoT1I13OJer3Dfa7g1Siijdrw PXGM6XkApXQLXjMjqzhfbZh605dxgs818pf55NOBrEAIfLzW1PxtNnDAx82Ngy72efnCNFn2 owCXmKPB7eVMKXJvlCQ/OIgP/GMZJMJuDb6M/Up+ubijWUlll8FYampwZwXZWikEfRhOkWVe GbjgtMcEWgRpQc+V+zriFiaUTFJfXqyXqQ85is6CI28F4vDSJqt0/S923KwGYQTbWRbAHiNF 23pfsOKQaQiciWXd8p8kTEfVfC9SpAozxDm4ArnyLd8LvbV5SQCtNTi1dlp4sXckBgz8Xp/C MHLgDLFdH19gm5dH2x+56t4u0Eokj9rsIB9iv1cTplI4u9RFxw9LdjaxvB7DNb7XkTAeM2IQ RCoWIbuGik/G/Q2xdJGeENhA5O6lBmW2jepDqQVi72UDYY1tKPd3mT0D8l4wnfCkqImigpuW dNBYFWvnbU37A3PH8jMmkSdmbytcPEZwS3A72efzHWHpkAeUQ9xTaDtUnUWZ0+QptP8tQvZV 7H7L7MhP0NazNKabKtHbtq8lVJdWPLqI8jTeUq0kma0QBuKn/aCMdKsdGIa0yHQTkMDlmj/5 F6gMg4zTmekqmPaV3l1EE73Jljr6a94oW+6SUk9y0eLaVdg3vy74Exdg/vUUP4V0r8e3UVp4 zxpAFaw2c7XANuctkJgeqtbe9Y0/FZA0yrQqQV8OpWqK60qiEQZdkx7uEbn1hM/DYsl84Biq W4pwRFyNaOH2UlAMTKZ3Iz1ErLSI2j2uhuobu+e213T1sqX5rZa8O4x+DCB9EmiEksv9Wki0 sEAiSPNoMWXSlBLAdSsChVSlVAyvbzRbygj6pmB0HRtNfLxqTrew5cyA/NjzB+8ftBZOafCF QnoEsRcCdL9TY5i01WvcB8AO/hfsaAuOMbzPf6b26OwPPphgzu8jCJG4YFh12qD8iN9TqjD2 JNPkJT6lkOXEizxilusqJW9nJ1HaCoSAmugwDLlQo9QZ7F3VYkOAGaqZcaww58t4vylE24d/ 1mlCVQc3cavchfHdF3x0zpb0kEPqGCmky+1p9BtuwkgtbHXnCnHwuC5MQECJnYOX256y1HlP YmzidkeGkmudQkg0hW/tw72wK1SpaI3KGe2Iw8AejX1InpiTqqvv6CDJc9O6Y8tmSpSWeW4J 1udT/bxrgAb3CXqA2ZFjGpjJnf659Ojxkw81TrVJW0WzjKRYcxqwBbD+NHQDeVc2DYLXmgwi DXaAES9I8j8+NyVk5nZteXtH2mlV5BVbWzq1dba7Hr9tTAsW0Tv2a3rybiFWUAg3CT21sdnT 3DNpRf4Oczw0riidPlgZg9uDUP97MxzHsd/lJExjdcewyt/5N3d8HwZnGP0Kdge17j5aS9HQ CMIzsXV/An60VdiaHOIxp78fnqYy8plIdK9ZylFv0B1p9APE6qS4LFeyGFwv1m1tgLNYOd0h DZbyPov9HsyjOQAuQ5rxSKYSON3fwEQLWnnkBKG6Mq7paNcaTO0cLS+40F5mMioELCIpgwPE Ga8YJopGjV8q9luKF+ZmmOm8ZnqIZODCLBb/g3RiRrLiPJZbY48huZfzzQyInrz5DUk07Jp1 kEohMDi+tLbdCM1u/jlSh9Aam+rO4VJoWqr1PgG2J7RhtHKfN0pGy1XDsW2C6vwSnRK86ygb V7GESVg+CnFX+CDTEnPsAE+6CiXW5GzayPIfj9AkZM7FUPbfAsG0GV2FH07hsJrSVzsnZa8N h8/vndIuBb5skcek7o4cUCgDSGP4l/vMG58SYDDfkMJtUcbthuTaYrGqbstekMQtpy58F7Xc j3dN1kOVDtZHBTDXg+rP6Hyt4OZra7FVqznfqGIOfLX+KRfT6van8vxlNE9rnDXbIPXeSAza p9zklxKWXQzcyjAsxMITSFf1yfEbsrA4Qy55jUytcentvLiRAPo44KLTbpUK9RmvR6s0++FM KaLiSB1JCw9tNtEzGLUyLUZwF8Zij1/PzirH7MasCfRTaXW0qZJBh8fYil3OYNG9aU5lgVKP MfajJvy2NsaxrYtDExZUFX6hsyzTckDImX4OVGeQUjWbPKJIjrEx8yxaqS5CPVRgOhSqxysq GObHkvkbVHh33HiUxGiN/0JjTnOZkQP/tHgNEw0WS6+FIGDCFXzKtJ8gDwozKdhg3rLMTVZK j1gawZWqaXW6ypEg/J5EmgH73x/LODClTzKiouQYpsQr/ZvBTx50uxA53Fvgb5I7yxfROB0h yLIr5hvolC6l8GAzzNmVFxFrTMB1+fp9Q1yfL7U8JVNQyOO5BUW8WCZEAgHvfNgA9zr/q1Sk 53Byfq1JzBF/NbZu8AbAoKHTaDPeGpkOh3vFjnOCQIDRjP+LmDTiXtWl/SK/2GUpJw3wnAJs JULQ75fElcyE6FCYqyENNkLIZMyUzF91LDG1IgH4n2xqBSXT8Jf7Mivvh26DvDmKTLfhr5BN UJg/A==
Ironport-sdr: ZCbGlnCKnh1T1DulKDXG6rOPgLZ1AYxRMAt8QlF5ATubpT/t4uhq4jv1WVxzosJakcNcX7YE7J ME0N0pXAYS6WRp84r/Uwrl6obZCkqpBHEjMmLqhnX8m8M264z/NIKzVE58mEx+mfUhsaXLuzDW ac9RvJJZ7HdhiOV11BrwiIV8ldqb3JiJoj6aLt6l6sxKnpWkPVhnnjar4aZO33tyS0IV9ouhxB dPp1bvUeQZ9Zitdf6d53Rn7FoV0Kir3FpmHhkREifhlqhwPSPMExD0S+06d9rhroG4d2qFw1Kz LGfvXBOqGDzSG4ZbwJeBVKM5

I have a Coq type R with field axiom and I am trying to construct a
math-comp fieldType. After reading a bit of source code [1, 2], I
managed to wrap my head around, or at least I think so, the details
and wrote the code (see below), but now I am stuck with choiceType. In
particular, I am getting error for this statement

(*I don't know how to get choiceType *)
Canonical R_zmodtype := ZmodType R R_zmodmixin.

You can see the rest of the source code [3].

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.

Best,
Mukesh

[1]
https://github.com/math-comp/math-comp/blob/master/mathcomp/field/fieldext.v#L145-L153
[2]
https://github.com/verified-network-toolchain/Verified-FEC/blob/master/proofs/Poly/BoolField.v
[3] https://gist.github.com/mukeshtiwari/375b2ae8198a8a236541ef7153dff598

[Coq-Club] ChoiceType for Coq Type with Field Axioms, mukesh tiwari, 05/19/2022