Using Coq Field axioms

Question

I'm experimenting with the Coq field module trying to prove the following simple identity directly from field axioms: forall v, 0v == v. I saw that both 0 and == have existing notations, so I tried this (but failed):

(***********)
(* IMPORTS *)
(***********)
Require Import Coq.setoid_ring.Field_theory.

(*********************)
(* forall v, 0v == v *)
(*********************)
Lemma mul_0_l: forall v,
  ("0" * v "==" "0")%R_scope.
Proof.

I got this error message:

Unknown scope delimiting key R_scope.

When I looked at the field library, R_scope is definitely there, so I must be missing something.

Answer 1

Actually, those notations are in a section, which means that they are not available from the outside.

Furthermore, all these definitions are parameterized by the field structure, so if you want to prove general results about fields you will need to declare (or instantiate) those parameters locally.

I'm not sure it is actually meant to be used that way. My advice is to open an issue on Github to ask the purpose of the setoid_ring plugin.

Require Import Coq.setoid_ring.Field_theory.
Require Import Coq.setoid_ring.Ring_theory.
Require Import Setoid.

Section MyFieldTheory.

(* Theory parameterized by a field R *)
Variable (R:Type)
         (rO:R) (rI:R)
         (radd rmul rsub : R -> R -> R)
         (ropp : R -> R)
         (rdiv : R -> R -> R)
         (rinv : R -> R)
         (req : R -> R -> Prop)
.
Variable Rfield : field_theory rO rI radd rmul rsub ropp rdiv rinv req.
Variable Reqeq : Equivalence req.
Variable Reqext : ring_eq_ext radd rmul ropp req.

(* Field notations *)
Notation "0" := rO : R_scope.
Notation "1" := rI : R_scope.
Infix "+" := radd : R_scope.
Infix "*" := rmul : R_scope.
Infix "==" := req : R_scope.

(* Use these notations by default *)
Local Open Scope R_scope.


(* Example lemma *)

Lemma mul_0_l: forall v, (0 * v == 0).
Proof.
  intros v.
  apply ARmul_0_l with rI radd rsub ropp.
  apply F2AF, AF_AR in Rfield; auto.
Qed.

---

About notation

Note that the quotes are part of the syntax for the Notation/Infix command

Infix "+" := radd : R_scope.

You can now just write x + y, no quotes.

It is good practice to assign scopes to your notations (via the : R_scope annotation above for example) as that enables mechanisms for disambiguation of different meanings for the same notation. In particular the main two ways to make notations available are:

• Local Open Scope R_scope. make all R_scope notations available for the current file.

• Bind Scope R_scope with whatever. associates a delimiting key whatever to the scope R_scope. The delimiting key is what goes after the % symbol to open a scope in a given expression, so you could write (0 == 0 * v)%whatever, whether or not R_scope was previously opened using Local Open Scope.

Answer 2

Here is an (unsuccessful) attempt based on @Li-yao-Xia:

(***********)
(* IMPORTS *)
(***********)
Require Import Coq.setoid_ring.Field_theory.
Require Import Coq.setoid_ring.Ring_theory.

(**********)
(* SCOPES *)
(**********)
Delimit Scope R_scope with ring.

(************)
(* SECTIONS *)
(************)
Section MyFieldTheory.

(* Theory parameterized by a field R *)
Variable (R:Type)
         (rO:R) (rI:R)
         (radd rmul rsub : R -> R -> R)
         (ropp : R -> R)
         (rdiv : R -> R -> R)
         (rinv : R -> R)
         (req : R -> R -> Prop)
.
Variable Rfield : field_theory rO rI radd rmul rsub ropp rdiv rinv req.

(*******************)
(* Field notations *)
(*******************)
Notation "0" := rO   : R_scope.
Notation "1" := rI   : R_scope.
Infix    "+" := radd : R_scope.
Infix    "*" := rmul : R_scope.
(*******************)
(* Field notations *)
(*******************)
Infix "==" := req (at level 70, no associativity) : R_scope.

(* Use these notations by default *)
Local Open Scope R_scope.


(* Example lemma *)

Lemma mul_0_l: forall v, (0 * v == 0).
Proof.
  intros v.
  apply ARmul_0_l with rI radd rsub ropp.
  apply Rfield.

In the assumptions I have:

Rfield : field_theory 0 1 radd rmul rsub ropp rdiv rinv req

And the goal says:

almost_ring_theory 0 1 radd rmul rsub ropp req

I figured there must be something that says: field_theory -> almost_ring_theory. But when I tried to apply Rfield I got:

In environment
R : Type
rO, rI : R
radd, rmul, rsub : R -> R -> R
ropp : R -> R
rdiv : R -> R -> R
rinv : R -> R
req : R -> R -> Prop
Rfield : field_theory 0 1 radd rmul rsub ropp rdiv rinv req
v : R
Unable to unify "field_theory 0 1 radd rmul rsub ropp rdiv rinv req" with
 "almost_ring_theory 0 1 radd rmul rsub ropp req".