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))).
Proof.
field. split.
+ intro. admit.
+ eapply (F_1_neq_0 F).
Admitted.
End Field.
```

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

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.

For you second question, you should probably look at `Number Notation`

in Coq's manual.

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