ring3.v

rom mathcomp Require Import ssreflect ssrnat eqtype ssrbool ssrnum ssralg.
Require Import Ring.

Import GRing.Theory.
Open Scope ring_scope.

Section foo.
Variable R: numFieldType.

Definition T:= R.
Definition subT : T -> T -> T := fun x y => (x - y)%R.
Local Notation "x - y":= (subT x y).

Definition oppT : T -> T :=
    fun x => (-x)%R.
Local Notation "- x":= (oppT x).

Definition addT : T -> T -> T := +%R.
Local Infix "+" := addT.

Definition rt :

  (* Doesn't work.*)
  (* @ring_theory T 0%:R 1%:R +%R *%R (fun a b => a - b) -%R eq. *)
  (* Works. *)
  (* @ring_theory T 0%:R 1%:R addT *%R (fun a b => a - b) -%R eq. *)
  (* Also works. *)
  @ring_theory T 0%:R 1%R addT *%R subT oppT eq.
(* Admitted. *) (* Also enough! *)
Proof.
  apply mk_rt.
  - apply add0r.
  - apply addrC.
  - apply addrA.
  - apply mul1r.
  - apply mulrC.
  - apply mulrA.
  - apply mulrDl.
  - by [].
  - apply subrr.
Qed.
Add Ring Ringgg : rt.

Lemma tmp2:
    forall x y:T, x + y = y + x.
Proof. move => x y. ring. Qed.
End foo.