Stream: Coq users

Topic: Lra but for an arbitrary field?

view this post on Zulip Lessness (Jul 31 2023 at 07:52):

Is it possible to automate remaining parts of test_theorem's proof?
I don't know, using some kind of lra, maybe?

Require Import Lra Field Equivalence Morphisms Utf8.
Set Implicit Arguments.

Section Field.

Parameter R: Type.
Parameter req: R  R  Prop.
Parameters rO rI: R.
Parameters radd rmul rsub rdiv: R  R  R.
Parameters ropp rinv: R  R.

Parameter reqProperty: Equivalence req.

Parameter radd_Proper: Proper (req ==> req ==> req) radd.
Parameter rmul_Proper: Proper (req ==> req ==> req) rmul.
Parameter rsub_Proper: Proper (req ==> req ==> req) rsub.
Parameter ropp_Proper: Proper (req ==> req) ropp.
Parameter rdiv_Proper: Proper (req ==> req ==> req) rdiv.
Parameter rinv_Proper: Proper (req ==> req) rinv.

Instance req_equivalence: Equivalence req := reqProperty.
Instance radd_morphism: Proper (req ==> req ==> req) radd := radd_Proper.
Instance rmul_morphism: Proper (req ==> req ==> req) rmul := rmul_Proper.
Instance rsub_morphism: Proper (req ==> req ==> req) rsub := rsub_Proper.
Instance ropp_morphism: Proper (req ==> req) ropp := ropp_Proper.
Instance rdiv_morphism: Proper (req ==> req ==> req) rdiv := rdiv_Proper.
Instance rinv_morphism: Proper (req ==> req) rinv := rinv_Proper.

Parameter F: field_theory rO rI radd rmul rsub ropp rdiv rinv req.
Add Field fieldF: F.

Theorem test_theorem: req (radd rO (radd rI rI)) (rinv (rinv (radd rI rI))).
  field. split.
  + intro. admit.
  + eapply (F_1_neq_0 F).

End Field.

view this post on Zulip Lessness (Jul 31 2023 at 07:53):

And another question - is it possible to replace rO, rI, rI + rI and etc. with numbers like 0, 1, 2 (probably in some scope F)?

view this post on Zulip Pierre Roux (Jul 31 2023 at 08:30):

Don't know if that helps (I only read the title) but if you are using mathcomp, algebra-tactics make lra work for any realFieldType. So if you build a realFieldType instance on your type (you can look at for an example with the rational numbers (note that this is for MC2 but you may have to wait a few more weeks for algebra-tactics to be ported to MC2, you can also look at the math-comp-1 branch if using MC1)) you get lra on it.

view this post on Zulip Pierre Roux (Jul 31 2023 at 08:31):

For you second question, you should probably look at Number Notation in Coq's manual.

view this post on Zulip Lessness (Jul 31 2023 at 09:13):

Oh, 1+1 can be equal to 0 in some fields. That means it's impossible to prove that test theorem.
My bad.

Last updated: Jun 13 2024 at 19:02 UTC