## Stream: Coq users

### Topic: Lra but for an arbitrary field?

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

Proof.
field. split.
+ eapply (F_1_neq_0 F).

End Field.
``````

#### 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)?

#### 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 https://github.com/math-comp/algebra-tactics/ make `lra` work for any `realFieldType`. So if you build a `realFieldType` instance on your type (you can look at https://github.com/math-comp/math-comp/blob/master/mathcomp/algebra/rat.v 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.

#### Pierre Roux (Jul 31 2023 at 08:31):

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

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