I tried to define function “sum (x y z: R): R := radd x (radd y z)” which finds the corresponding field structure. How to do it correctly - so that I don’t have to supply addition to it?
Thank you!
Set Implicit Arguments.
Require Import Field Equivalence Morphisms.
Section M.
Variable R: Type.
Variable req: R -> R -> Prop.
Variable rEquiv: Equivalence req.
Variables rO rI: R.
Variable radd rmul rsub rdiv: R -> R -> R.
Variable ropp rinv: R -> R.
Variable Proper_radd: Proper (req ==> req ==> req) radd.
Variable Proper_rmul: Proper (req ==> req ==> req) rmul.
Variable Proper_rsub: Proper (req ==> req ==> req) rsub.
Variable Proper_rdiv: Proper (req ==> req ==> req) rdiv.
Variable Proper_ropp: Proper (req ==> req) ropp.
Variable Proper_rinv: Proper (req ==> req) rinv.
Variable field: field_theory rO rI radd rmul rsub ropp rdiv rinv req.
Add Field Rfield: field.
Definition sum (x y z: R): R := radd x (radd y z).
End M.
Require Import Reals.
Print sum.
Eval compute in sum Rplus (INR 1) (INR 2) (INR 3).