Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2018 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro, Tim Baanen
-/
import Mathlib.Tactic.Ring.Basic
import Mathlib.Tactic.Conv
import Mathlib.Util.Qq
/-!
# `ring_nf` tactic
A tactic which uses `ring` to rewrite expressions. This can be used non-terminally to normalize
ring expressions in the goal such as `⊢ P (x + x + x)` ~> `⊢ P (x * 3)`, as well as being able to
prove some equations that `ring` cannot because they involve ring reasoning inside a subterm,
such as `sin (x + y) + sin (y + x) = 2 * sin (x + y)`.
-/
namespace Mathlib.Tactic
open Lean hiding Rat
open Qq Meta
namespace Ring
/-- True if this represents an atomic expression. -/
def ExBase.isAtom : ExBase sα a → Bool
| .atom _ => true
| _ => false
/-- True if this represents an atomic expression. -/
def ExProd.isAtom : ExProd sα a → Bool
| .mul va₁ ( .const 1 _) ( .const 1 _) => va₁ . isAtom
| _ => false
/-- True if this represents an atomic expression. -/
def ExSum.isAtom : ExSum sα a → Bool
| .add va₁ va₂ => match va₂ with -- FIXME: this takes a while to compile as one match
| .zero => va₁ . isAtom
| _ => false
| _ => false
end Ring
namespace RingNF
open Ring
/-- The normalization style for `ring_nf`. -/
inductive RingMode where
/-- Sum-of-products form, like `x + x * y * 2 + z ^ 2`. -/
| SOP
/-- Raw form: the representation `ring` uses internally. -/
| raw
deriving Inhabited , BEq , Repr
/-- Configuration for `ring_nf`. -/
structure Config where
/-- the reducibility setting to use when comparing atoms for defeq -/
red := TransparencyMode.reducible
/-- if true, atoms inside ring expressions will be reduced recursively -/
recursive := true
/-- The normalization style. -/
mode := RingMode.SOP
deriving Inhabited , BEq , Repr
/-- Function elaborating `RingNF.Config`. -/
declare_config_elab elabConfig Config
/-- The read-only state of the `RingNF` monad. -/
structure Context where
/-- A basically empty simp context, passed to the `simp` traversal in `RingNF.rewrite`. -/
ctx : Simp.Context
/-- A cleanup routine, which simplifies normalized polynomials to a more human-friendly
format. -/
simp : Simp.Result → SimpM Simp.Result
/-- The monad for `RingNF` contains, in addition to the `AtomM` state,
a simp context for the main traversal and a simp function (which has another simp context)
to simplify normalized polynomials. -/
abbrev M := ReaderT : Type ?u.45219 → (Type ?u.45219 → Type ?u.45218Type ?u.45219 → Type (max?u.45219?u.45218) Context AtomM
/--
A tactic in the `RingNF.M` monad which will simplify expression `parent` to a normal form.
* `root`: true if this is a direct call to the function.
`RingNF.M.run` sets this to `false` in recursive mode.
-/
def rewrite ( parent : Expr ) ( root := true ) : M Simp.Result :=
fun nctx rctx s ↦ do
let pre : (e : ?m.45269 ) → ?m.45274 e
pre e :=
try
guard <| root || parent != e -- recursion guard
let e ← withReducible <| whnf e
guard e . isApp -- all interesting ring expressions are applications
let ⟨ u , α , e ⟩ ← inferTypeQ' e
let sα ← synthInstanceQ ( q( CommSemiring : Type ?u.46532 → Type ?u.46532CommSemiring $ α ) : Q( Type u ))
let c ← mkCache sα
let ⟨ a , _, pa ⟩ ← match ← isAtomOrDerivable sα c e rctx s with
| none => eval eval sα c e rctx s : SimpM (?m.46680 y✝ sα eval sα c e rctx s : SimpM (?m.46680 y✝ c eval sα c e rctx s : SimpM (?m.46680 y✝ e eval sα c e rctx s : SimpM (?m.46680 y✝ rctx eval sα c e rctx s : SimpM (?m.46680 y✝ s -- `none` indicates that `eval` will find something algebraic.
| some none => failure -- No point rewriting atoms
| some ( some r ) => pure : {f : Type ?u.46939 → Type ?u.46938[self : Pure f {α : Type ?u.46939} → α → f α pure r : SimpM (?m.46680 y✝ r -- Nothing algebraic for `eval` to use, but `norm_num` simplifies.
let r ← nctx . simp { expr := a , proof? := pa }
if ← withReducible <| isDefEq r . expr e then return .done { expr := r . expr }
pure : {f : Type ?u.48055 → Type ?u.48054[self : Pure f {α : Type ?u.48055} → α → f α ( .done r )
catch _ => pure : {f : Type ?u.48582 → Type ?u.48581[self : Pure f {α : Type ?u.48582} → α → f α <| .visit { expr := e }
let post := ( Simp.postDefault · fun _ ↦ none )
(·.1) <$> Simp.main parent nctx . ctx (methods := { pre : (e : ?m.45269 ) → ?m.45274 e
pre , post })
variable [ CommSemiring : Type ?u.102140 → Type ?u.102140 R ]
theorem add_assoc_rev : ∀ (a b c : R ), a + (b + c = a + b + c add_assoc_rev ( a b c : R ) : a + ( b + c ) = a + b + c := ( add_assoc ..). symm : ∀ {α : Sort ?u.72622} {a b : α }, a = b b = a symm
theorem mul_assoc_rev : ∀ (a b c : R ), a * (b * c = a * b * c mul_assoc_rev ( a b c : R ) : a * ( b * c ) = a * b * c := ( mul_assoc : ∀ {G : Type ?u.73918} [inst : Semigroup G a b c : G ), a * b * c = a * (b * c ..). symm : ∀ {α : Sort ?u.73938} {a b : α }, a = b b = a symm
theorem mul_neg : ∀ {R : Type u_1} [inst : Ring R a b : R ), a * - b = - (a * b mul_neg { R } [ Ring R ] ( a b : R ) : a * - b = -( a * b ) := by simp
theorem add_neg : ∀ {R : Type u_1} [inst : Ring R a b : R ), a + - b = a - b add_neg { R } [ Ring R ] ( a b : R ) : a + - b = a - b := ( sub_eq_add_neg ..). symm : ∀ {α : Sort ?u.74611} {a b : α }, a = b b = a symm
theorem nat_rawCast_0 : ( Nat.rawCast 0 : R ) = 0 := by simp
theorem nat_rawCast_1 : ( Nat.rawCast 1 : R ) = 1 := by simp
theorem nat_rawCast_2 [ Nat.AtLeastTwo n ] : ( Nat.rawCast n : R ) = OfNat.ofNat : {α : Type ?u.76617} → (x : ℕ ) → [self : OfNat α x α n := rfl : ∀ {α : Sort ?u.76767} {a : α }, a = a
theorem int_rawCast_1 { R } [ Ring R ] : ( Int.rawCast : {α : Type ?u.76797} → [inst : Ring α ℤ → α ( .negOfNat 1 ) : R ) = - 1 := by
simp [ Int.negOfNat_eq ]
theorem int_rawCast_2 { R } [ Ring R ] [ Nat.AtLeastTwo n ] :
( Int.rawCast : {α : Type ?u.78208} → [inst : Ring α ℤ → α ( .negOfNat n ) : R ) = - OfNat.ofNat : {α : Type ?u.78226} → (x : ℕ ) → [self : OfNat α x α n := by
simp [ Int.negOfNat_eq , OfNat.ofNat : {α : Type ?u.78469} → (x : ℕ ) → [self : OfNat α x α ]
theorem rat_rawCast_2 { R } [ DivisionRing : Type ?u.79745 → Type ?u.79745 R ] : ( Rat.rawCast n d : R ) = n / d := by simp
/--
Runs a tactic in the `RingNF.M` monad, given initial data:
* `s`: a reference to the mutable state of `ring`, for persisting across calls.
This ensures that atom ordering is used consistently.
* `cfg`: the configuration options
* `x`: the tactic to run
-/
partial def M.run
( s : IO.Ref AtomM.State ) ( cfg : RingNF.Config ) ( x : M α ) : MetaM α := do
let ctx := {
simpTheorems := #[← Elab.Tactic.simpOnlyBuiltins.foldlM (·.addConst ·) {}] : Array ?m.82602 Elab.Tactic.simpOnlyBuiltins #[← Elab.Tactic.simpOnlyBuiltins.foldlM (·.addConst ·) {}] : Array ?m.82602 foldlM : {m : Type ?u.80709 → Type ?u.80708[inst : Monad m {s : Type ?u.80709} → {α : Type ?u.80707} → (s → α → m s s → List α m s #[← Elab.Tactic.simpOnlyBuiltins.foldlM (·.addConst ·) {}] : Array ?m.82602 addConst #[← Elab.Tactic.simpOnlyBuiltins.foldlM (·.addConst ·) {}] : Array ?m.82602 {} #[← Elab.Tactic.simpOnlyBuiltins.foldlM (·.addConst ·) {}] : Array ?m.82602
congrTheorems := ← getSimpCongrTheorems }
let simp ← match cfg . mode with
| .raw => pure : {f : Type ?u.80955 → Type ?u.80954[self : Pure f {α : Type ?u.80955} → α → f α pure pure : MetaM (?m.80904 y✝ pure : {f : Type ?u.80980 → Type ?u.80979[self : Pure f {α : Type ?u.80980} → α → f α
| .SOP =>
let thms : SimpTheorems := {}
let thms ← [`` add_zero , `` add_assoc_rev , `` _root_.mul_one , `` mul_assoc_rev ,
`` _root_.pow_one : ∀ {M : Type u} [inst : Monoid M a : M ), a ^ 1 = a , `` mul_neg : ∀ {R : Type u_1} [inst : Ring R a b : R ), a * - b = - (a * b , `` add_neg : ∀ {R : Type u_1} [inst : Ring R a b : R ), a + - b = a - b ]. foldlM : {m : Type ?u.81199 → Type ?u.81198[inst : Monad m {s : Type ?u.81199} → {α : Type ?u.81197} → (s → α → m s s → List α m s foldlM (·. addConst ·) thms
let thms ← [`` nat_rawCast_0 , `` nat_rawCast_1 , `` nat_rawCast_2 , `` int_rawCast_1 , `` int_rawCast_2 ,
`` rat_rawCast_2 ]. foldlM : {m : Type ?u.81316 → Type ?u.81315[inst : Monad m {s : Type ?u.81316} → {α : Type ?u.81314} → (s → α → m s s → List α m s foldlM (·. addConst · (post := false )) thms
let ctx' := { ctx with simpTheorems := #[ thms ] }
pure : {f : Type ?u.81422 → Type ?u.81421[self : Pure f {α : Type ?u.81422} → α → f α pure fun r' : Simp.Result ↦ do
Simp.mkEqTrans r' (← Simp.main r'.expr ctx' (methods := Simp.DefaultMethods.methods)).1 : MetaM (?m.80904 y✝ pure fun r' : Simp.Result ↦ do
Simp.mkEqTrans r' (← Simp.main r'.expr ctx' (methods := Simp.DefaultMethods.methods)).1 : MetaM (?m.80904 y✝ fun pure fun r' : Simp.Result ↦ do
Simp.mkEqTrans r' (← Simp.main r'.expr ctx' (methods := Simp.DefaultMethods.methods)).1 : MetaM (?m.80904 y✝ r' pure fun r' : Simp.Result ↦ do
Simp.mkEqTrans r' (← Simp.main r'.expr ctx' (methods := Simp.DefaultMethods.methods)).1 : MetaM (?m.80904 y✝ Simp.Result pure fun r' : Simp.Result ↦ do
Simp.mkEqTrans r' (← Simp.main r'.expr ctx' (methods := Simp.DefaultMethods.methods)).1 : MetaM (?m.80904 y✝ pure fun r' : Simp.Result ↦ do
Simp.mkEqTrans r' (← Simp.main r'.expr ctx' (methods := Simp.DefaultMethods.methods)).1 : MetaM (?m.80904 y✝ do pure fun r' : Simp.Result ↦ do
Simp.mkEqTrans r' (← Simp.main r'.expr ctx' (methods := Simp.DefaultMethods.methods)).1 : MetaM (?m.80904 y✝ Simp.mkEqTrans pure fun r' : Simp.Result ↦ do
Simp.mkEqTrans r' (← Simp.main r'.expr ctx' (methods := Simp.DefaultMethods.methods)).1 : MetaM (?m.80904 y✝ r' pure fun r' : Simp.Result ↦ do
Simp.mkEqTrans r' (← Simp.main r'.expr ctx' (methods := Simp.DefaultMethods.methods)).1 : MetaM (?m.80904 y✝ (← Simp.main r'.expr ctx' (methods := Simp.DefaultMethods.methods)) : ?m.82876
(← Simp.main (← Simp.main r'.expr ctx' (methods := Simp.DefaultMethods.methods)) : ?m.82876
r' (← Simp.main r'.expr ctx' (methods := Simp.DefaultMethods.methods)) : ?m.82876
. expr (← Simp.main r'.expr ctx' (methods := Simp.DefaultMethods.methods)) : ?m.82876
ctx' (← Simp.main r'.expr ctx' (methods := Simp.DefaultMethods.methods)) : ?m.82876
(methods := Simp.DefaultMethods.methods (← Simp.main r'.expr ctx' (methods := Simp.DefaultMethods.methods)) : ?m.82876
)) pure fun r' : Simp.Result ↦ do
Simp.mkEqTrans r' (← Simp.main r'.expr ctx' (methods := Simp.DefaultMethods.methods)).1 : MetaM (?m.80904 y✝ 1 : {α : Type ?u.82891} → {β : Type ?u.82890} → α × β α
let nctx := { ctx , simp }
let rec
/-- The recursive context. -/
rctx := { red := cfg . red , evalAtom },
/-- The atom evaluator calls either `RingNF.rewrite` recursively,
or nothing depending on `cfg.recursive`. -/
evalAtom := if cfg . recursive
then fun e ↦ rewrite e false nctx rctx s
else fun e ↦ pure : {f : Type ?u.81977 → Type ?u.81976[self : Pure f {α : Type ?u.81977} → α → f α { expr := e }
x nctx rctx s
/-- Overrides the default error message in `ring1` to use a prettified version of the goal. -/
initialize ringCleanupRef . set fun e => do
M.run (← IO.mkRef {}) : ?m.87076
(← IO.mkRef (← IO.mkRef {}) : ?m.87076
{} (← IO.mkRef {}) : ?m.87076
) { recursive := false } fun nctx _ _ =>
return (← nctx.simp { expr := e } nctx.ctx |>.run {}) : ?m.87399
(← nctx (← nctx.simp { expr := e } nctx.ctx |>.run {}) : ?m.87399
. simp (← nctx.simp { expr := e } nctx.ctx |>.run {}) : ?m.87399
{ expr := e (← nctx.simp { expr := e } nctx.ctx |>.run {}) : ?m.87399
} nctx (← nctx.simp { expr := e } nctx.ctx |>.run {}) : ?m.87399
. ctx (← nctx.simp { expr := e } nctx.ctx |>.run {}) : ?m.87399
|>. run (← nctx.simp { expr := e } nctx.ctx |>.run {}) : ?m.87399
{} (← nctx.simp { expr := e } nctx.ctx |>.run {}) : ?m.87399
) . 1 : {α : Type ?u.87427} → {β : Type ?u.87426} → α × β α . expr
open Elab.Tactic Parser.Tactic
/-- Use `ring_nf` to rewrite the main goal. -/
def ringNFTarget ( s : IO.Ref AtomM.State ) ( cfg : Config ) : TacticM Unit := withMainContext do
let goal ← getMainGoal
let tgt ← instantiateMVars (← goal.getType) : ?m.89672
(← goal (← goal.getType) : ?m.89672
. getType (← goal.getType) : ?m.89672
)
let r ← M.run s cfg <| rewrite tgt
if r . expr . isConstOf `` True then
goal . assign (← mkOfEqTrue (← r.getProof)) : ?m.90105
(← mkOfEqTrue (← mkOfEqTrue (← r.getProof)) : ?m.90105
(← r . getProof ) (← mkOfEqTrue (← r.getProof)) : ?m.90105
)
replaceMainGoal []
else
replaceMainGoal [← applySimpResultToTarget goal tgt r] : List ?m.90306 applySimpResultToTarget [← applySimpResultToTarget goal tgt r] : List ?m.90306 goal [← applySimpResultToTarget goal tgt r] : List ?m.90306 tgt [← applySimpResultToTarget goal tgt r] : List ?m.90306 r [← applySimpResultToTarget goal tgt r] : List ?m.90306
/-- Use `ring_nf` to rewrite hypothesis `h`. -/
def ringNFLocalDecl ( s : IO.Ref AtomM.State ) ( cfg : Config ) ( fvarId : FVarId ) :
TacticM Unit := withMainContext do
let tgt ← instantiateMVars (← fvarId.getType) : ?m.92314
(← fvarId (← fvarId.getType) : ?m.92314
. getType (← fvarId.getType) : ?m.92314
)
let goal ← getMainGoal
let myres ← M.run s cfg <| rewrite tgt
match ← applySimpResultToLocalDecl goal fvarId myres false with
| none => replaceMainGoal []
| some (_, newGoal ) => replaceMainGoal [ newGoal ]
/--
Simplification tactic for expressions in the language of commutative (semi)rings,
which rewrites all ring expressions into a normal form.
* `ring_nf!` will use a more aggressive reducibility setting to identify atoms.
* `ring_nf (config := cfg)` allows for additional configuration:
* `red`: the reducibility setting (overridden by `!`)
* `recursive`: if true, `ring_nf` will also recurse into atoms
* `ring_nf` works as both a tactic and a conv tactic.
In tactic mode, `ring_nf at h` can be used to rewrite in a hypothesis.
-/
elab ( name := ringNF ) "ring_nf" tk :"!"? cfg :( config ?) loc :( ppSpace location )? : tactic => do
let mut cfg ← elabConfig cfg
if tk . isSome then cfg := { cfg with red := .default }
let loc := ( loc . map expandLocation ). getD ( .targets #[] true )
let s ← IO.mkRef {}
withLocation loc ( ringNFLocalDecl s cfg ) ( ringNFTarget s cfg )
fun _ ↦ throwError "ring_nf failed" : ?m.95731 ?m.95732
throwError throwError "ring_nf failed" : ?m.95731 ?m.95732
@[inherit_doc ringNF ] macro "ring_nf!" cfg :( config )? loc :( ppSpace location )? : tactic =>
`(tactic| ring_nf ! $( cfg )? $( loc )?)
@[inherit_doc ringNF ] syntax ( name := ringNFConv ) "ring_nf" "!"? ( config )? : conv
/--
Tactic for solving equations of *commutative* (semi)rings, allowing variables in the exponent.
* This version of `ring1` uses `ring_nf` to simplify in atoms.
* The variant `ring1_nf!` will use a more aggressive reducibility setting
to determine equality of atoms.
-/
elab ( name := ring1NF ) "ring1_nf" tk :"!"? cfg :( config ?) : tactic => do
let mut cfg ← elabConfig cfg
if tk . isSome then cfg := { cfg with red := .default }
let s ← IO.mkRef {}
liftMetaMAtMain fun g ↦ M.run s cfg <| proveEq g
@[inherit_doc ring1NF ] macro "ring1_nf!" cfg :( config )? : tactic => `(tactic| ring1_nf ! $( cfg )?)
/-- Elaborator for the `ring_nf` tactic. -/
@[tactic ringNFConv ] def elabRingNFConv : Tactic := fun stx ↦ match stx with
| `(conv| ring_nf $[!%$ tk ]? $( _cfg )?) => withMainContext do
let mut cfg ← elabConfig stx [ 2 ]
if tk . isSome then cfg := { cfg with red := .default }
let s ← IO.mkRef {}
Conv.applySimpResult (← M.run s cfg <| rewrite (← instantiateMVars (← Conv.getLhs))) : ?m.110166
(← M.run (← M.run s cfg <| rewrite (← instantiateMVars (← Conv.getLhs))) : ?m.110166
s (← M.run s cfg <| rewrite (← instantiateMVars (← Conv.getLhs))) : ?m.110166
cfg (← M.run s cfg <| rewrite (← instantiateMVars (← Conv.getLhs))) : ?m.110166
<| rewrite (← M.run s cfg <| rewrite (← instantiateMVars (← Conv.getLhs))) : ?m.110166
(← instantiateMVars (← Conv.getLhs)) : ?m.109942
(← instantiateMVars (← instantiateMVars (← Conv.getLhs)) : ?m.109942
(← Conv.getLhs) : ?m.109813
(← Conv.getLhs (← Conv.getLhs) : ?m.109813
) (← instantiateMVars (← Conv.getLhs)) : ?m.109942
) (← M.run s cfg <| rewrite (← instantiateMVars (← Conv.getLhs))) : ?m.110166
)
| _ => Elab.throwUnsupportedSyntax
@[inherit_doc ringNF ] macro "ring_nf!" cfg :( config )? : conv => `(conv| ring_nf ! $( cfg )?)
/--
Tactic for evaluating expressions in *commutative* (semi)rings, allowing for variables in the
exponent.
* `ring!` will use a more aggressive reducibility setting to determine equality of atoms.
* `ring1` fails if the target is not an equality.
For example:
```
example (n : ℕ) (m : ℤ) : 2^(n+1) * m = 2 * 2^n * m := by ring
example (a b : ℤ) (n : ℕ) : (a + b)^(n + 2) = (a^2 + b^2 + a * b + b * a) * (a + b)^n := by ring
example (x y : ℕ) : x + id y = y + id x := by ring!
```
-/
macro ( name := ring ) "ring" : tactic =>
`(tactic| first | ring1 | ring_nf; trace "Try this: ring_nf") : ?m.115891 ?m.115894
`(tactic| first | ring1 | ring_nf; trace "Try this: ring_nf") : ?m.115891 ?m.115894
first `(tactic| first | ring1 | ring_nf; trace "Try this: ring_nf") : ?m.115891 ?m.115894
`(tactic| first | ring1 | ring_nf; trace "Try this: ring_nf") : ?m.115891 ?m.115894
ring1 `(tactic| first | ring1 | ring_nf; trace "Try this: ring_nf") : ?m.115891 ?m.115894
`(tactic| first | ring1 | ring_nf; trace "Try this: ring_nf") : ?m.115891 ?m.115894
ring_nf `(tactic| first | ring1 | ring_nf; trace "Try this: ring_nf") : ?m.115891 ?m.115894
`(tactic| first | ring1 | ring_nf; trace "Try this: ring_nf") : ?m.115891 ?m.115894
trace `(tactic| first | ring1 | ring_nf; trace "Try this: ring_nf") : ?m.115891 ?m.115894
@[inherit_doc ring ] macro "ring!" : tactic =>
`(tactic| first | ring1! | ring_nf!; trace "Try this: ring_nf!") : ?m.118468 ?m.118471
`(tactic| first | ring1! | ring_nf!; trace "Try this: ring_nf!") : ?m.118468 ?m.118471
first `(tactic| first | ring1! | ring_nf!; trace "Try this: ring_nf!") : ?m.118468 ?m.118471
`(tactic| first | ring1! | ring_nf!; trace "Try this: ring_nf!") : ?m.118468 ?m.118471
ring1! `(tactic| first | ring1! | ring_nf!; trace "Try this: ring_nf!") : ?m.118468 ?m.118471
`(tactic| first | ring1! | ring_nf!; trace "Try this: ring_nf!") : ?m.118468 ?m.118471
ring_nf! `(tactic| first | ring1! | ring_nf!; trace "Try this: ring_nf!") : ?m.118468 ?m.118471
`(tactic| first | ring1! | ring_nf!; trace "Try this: ring_nf!") : ?m.118468 ?m.118471
trace `(tactic| first | ring1! | ring_nf!; trace "Try this: ring_nf!") : ?m.118468 ?m.118471
/--
The tactic `ring` evaluates expressions in *commutative* (semi)rings.
This is the conv tactic version, which rewrites a target which is a ring equality to `True`.
See also the `ring` tactic.
-/
macro ( name := ringConv ) "ring" : conv =>
`(conv| first | discharge => ring1 | ring_nf; tactic => trace "Try this: ring_nf") : ?m.121060 ?m.121063
`(conv| first | discharge => ring1 | ring_nf; tactic => trace "Try this: ring_nf") : ?m.121060 ?m.121063
first `(conv| first | discharge => ring1 | ring_nf; tactic => trace "Try this: ring_nf") : ?m.121060 ?m.121063
`(conv| first | discharge => ring1 | ring_nf; tactic => trace "Try this: ring_nf") : ?m.121060 ?m.121063
discharge `(conv| first | discharge => ring1 | ring_nf; tactic => trace "Try this: ring_nf") : ?m.121060 ?m.121063
`(conv| first | discharge => ring1 | ring_nf; tactic => trace "Try this: ring_nf") : ?m.121060 ?m.121063
ring1 `(conv| first | discharge => ring1 | ring_nf; tactic => trace "Try this: ring_nf") : ?m.121060 ?m.121063
`(conv| first | discharge => ring1 | ring_nf; tactic => trace "Try this: ring_nf") : ?m.121060 ?m.121063
ring_nf `(conv| first | discharge => ring1 | ring_nf; tactic => trace "Try this: ring_nf") : ?m.121060 ?m.121063
`(conv| first | discharge => ring1 | ring_nf; tactic => trace "Try this: ring_nf") : ?m.121060 ?m.121063
tactic `(conv| first | discharge => ring1 | ring_nf; tactic => trace "Try this: ring_nf") : ?m.121060 ?m.121063
`(conv| first | discharge => ring1 | ring_nf; tactic => trace "Try this: ring_nf") : ?m.121060 ?m.121063
trace `(conv| first | discharge => ring1 | ring_nf; tactic => trace "Try this: ring_nf") : ?m.121060 ?m.121063
@[inherit_doc ringConv ] macro "ring!" : conv =>
`(conv| first | discharge => ring1! | ring_nf!; tactic => trace "Try this: ring_nf!") : ?m.124091 ?m.124094
`(conv| first | discharge => ring1! | ring_nf!; tactic => trace "Try this: ring_nf!") : ?m.124091 ?m.124094
first `(conv| first | discharge => ring1! | ring_nf!; tactic => trace "Try this: ring_nf!") : ?m.124091 ?m.124094
`(conv| first | discharge => ring1! | ring_nf!; tactic => trace "Try this: ring_nf!") : ?m.124091 ?m.124094
discharge `(conv| first | discharge => ring1! | ring_nf!; tactic => trace "Try this: ring_nf!") : ?m.124091 ?m.124094
`(conv| first | discharge => ring1! | ring_nf!; tactic => trace "Try this: ring_nf!") : ?m.124091 ?m.124094
ring1! `(conv| first | discharge => ring1! | ring_nf!; tactic => trace "Try this: ring_nf!") : ?m.124091 ?m.124094
`(conv| first | discharge => ring1! | ring_nf!; tactic => trace "Try this: ring_nf!") : ?m.124091 ?m.124094
ring_nf! `(conv| first | discharge => ring1! | ring_nf!; tactic => trace "Try this: ring_nf!") : ?m.124091 ?m.124094
`(conv| first | discharge => ring1! | ring_nf!; tactic => trace "Try this: ring_nf!") : ?m.124091 ?m.124094
tactic `(conv| first | discharge => ring1! | ring_nf!; tactic => trace "Try this: ring_nf!") : ?m.124091 ?m.124094
`(conv| first | discharge => ring1! | ring_nf!; tactic => trace "Try this: ring_nf!") : ?m.124091 ?m.124094
trace `(conv| first | discharge => ring1! | ring_nf!; tactic => trace "Try this: ring_nf!") : ?m.124091 ?m.124094