Skip to content

Instantly share code, notes, and snippets.

@vlj
Created April 1, 2020 18:20
Show Gist options
  • Save vlj/7c95a64470a941a4290ad018c58a5f22 to your computer and use it in GitHub Desktop.
Save vlj/7c95a64470a941a4290ad018c58a5f22 to your computer and use it in GitHub Desktop.
From mathcomp Require Import ssreflect ssrnat eqtype ssrbool ssrnum ssralg.
Require Import Ring.
Import GRing.Theory.
Variable R: numFieldType.
Open Scope ring_scope.
Definition T:= GRing.Zmodule.sort R.
(*
Definition addT : T -> T -> T :=
fun x y => (x + y)%R.
Notation "x ++ y":= (addT x y).
Definition mulT : T -> T -> T :=
fun x y => (x * y)%R.
Local Notation "x * y":= (mulT x y). *)
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 rt :
@ring_theory T 0%R 1%R +%R *%R subT oppT eq.
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.
Set Ltac Backtrace.
Lemma tmp2:
forall x y z:T, x + y = y + x.
Proof.
move => x y z.
Unset Printing Notations.
Fail ring.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment