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 Cmdinstead of Ctrl.
/-
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: {a : Level} → {arg : Q(Type a)} → { : Q(CommSemiring «\$arg»)} → {a_1 : Q(«\$arg»)} → ExBase a_1Bool
ExBase.isAtom
:
ExBase: {u : Level} → {α : Q(Type u)} → Q(CommSemiring «\$α»)Q(«\$α»)Type
ExBase
: ?m.6
a: ?m.16
a
Bool: Type
Bool
|
.atom: {u : Level} → {α : Q(Type u)} → { : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → ExBase e
.atom
_ =>
true: Bool
true
| _ =>
false: Bool
false
/-- True if this represents an atomic expression. -/ def
ExProd.isAtom: {a : Level} → {arg : Q(Type a)} → { : Q(CommSemiring «\$arg»)} → {a_1 : Q(«\$arg»)} → ExProd a_1Bool
ExProd.isAtom
:
ExProd: {u : Level} → {α : Q(Type u)} → Q(CommSemiring «\$α»)Q(«\$α»)Type
ExProd
: ?m.1165
a: ?m.1175
a
Bool: Type
Bool
|
.mul: {u : Level} → {α : Q(Type u)} → { : Q(CommSemiring «\$α»)} → {x : Q(«\$α»)} → {e : Q()} → {b : Q(«\$α»)} → ExBase xExProd bExProd q(«\$x» ^ «\$e» * «\$b»)
.mul
va₁: ExBase x✝
va₁
(
.const: {u : Level} → {α : Q(Type u)} → { : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → optParam () noneExProd e
.const
1:
1
_) (
.const: {u : Level} → {α : Q(Type u)} → { : Q(CommSemiring «\$α»)} → {e : Q(«\$α»)} → optParam () noneExProd e
.const
1:
1
_) =>
va₁: ExBase x✝
va₁
.
isAtom: {a : Level} → {arg : Q(Type a)} → { : Q(CommSemiring «\$arg»)} → {a_1 : Q(«\$arg»)} → ExBase a_1Bool
isAtom
| _ =>
false: Bool
false
/-- True if this represents an atomic expression. -/ def
ExSum.isAtom: {a : Level} → {arg : Q(Type a)} → { : Q(CommSemiring «\$arg»)} → {a_1 : Q(«\$arg»)} → ExSum a_1Bool
ExSum.isAtom
:
ExSum: {u : Level} → {α : Q(Type u)} → Q(CommSemiring «\$α»)Q(«\$α»)Type
ExSum
: ?m.31171
a: ?m.31181
a
Bool: Type
Bool
|
.add: {u : Level} → {α : Q(Type u)} → { : Q(CommSemiring «\$α»)} → {a b : Q(«\$α»)} → ExProd aExSum bExSum q(«\$a» + «\$b»)
va₁: ExProd a✝
va₁
va₂: ExSum b✝
va₂
=> match
va₂: ExSum b✝
va₂
with -- FIXME: this takes a while to compile as one match |
.zero: ExSum q(0)
.zero
=>
va₁: ExProd a✝
va₁
.
isAtom: {a : Level} → {arg : Q(Type a)} → { : Q(CommSemiring «\$arg»)} → {a_1 : Q(«\$arg»)} → ExProd a_1Bool
isAtom
| _ =>
false: Bool
false
| _ =>
false: Bool
false
end Ring namespace RingNF open Ring /-- The normalization style for `ring_nf`. -/ inductive
RingMode: Sort ?u.37459
RingMode
where /-- Sum-of-products form, like `x + x * y * 2 + z ^ 2`. -/ | SOP /-- Raw form: the representation `ring` uses internally. -/ | raw deriving
Inhabited: Sort u → Sort (max1u)
Inhabited
,
BEq: Type u → Type u
BEq
,
Repr: Type u → Type u
Repr
/-- Configuration for `ring_nf`. -/ structure
Config:
Config
where /-- the reducibility setting to use when comparing atoms for defeq -/
red:
red
:=
TransparencyMode.reducible: TransparencyMode
TransparencyMode.reducible
/-- if true, atoms inside ring expressions will be reduced recursively -/
recursive:
recursive
:=
true: Bool
true
/-- The normalization style. -/
mode:
mode
:=
RingMode.SOP: RingMode
RingMode.SOP
deriving
Inhabited: Sort u → Sort (max1u)
Inhabited
,
BEq: Type u → Type u
BEq
,
Repr: Type u → Type u
Repr
/-- Function elaborating `RingNF.Config`. -/ declare_config_elab
elabConfig:
elabConfig
Config: Type
Config
Context:
Context
where /-- A basically empty simp context, passed to the `simp` traversal in `RingNF.rewrite`. -/
ctx:
ctx
:
Simp.Context: Type
Simp.Context
/-- A cleanup routine, which simplifies normalized polynomials to a more human-friendly format. -/
simp:
simp
:
Simp.Result: Type
Simp.Result
SimpM:
SimpM
Simp.Result: Type
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:
M
:=
ReaderT: Type ?u.45219 → (Type ?u.45219 → Type ?u.45218) → Type ?u.45219 → Type (max?u.45219?u.45218)
Context: Type
Context
AtomM:
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:
rewrite
(
parent: Expr
parent
:
Expr: Type
Expr
) (
root:
root
:=
true: Bool
true
) :
M:
M
Simp.Result: Type
Simp.Result
:= fun
nctx: ?m.45241
nctx
rctx: ?m.45244
rctx
s: ?m.45247
s
do let
pre: (e : ?m.45269) → ?m.45274 e
pre
e: ?m.45269
e
:= try
guard: {f : TypeType ?u.45722} → [inst : ] → (p : Prop) → [inst : ] → f Unit
guard
<|
root:
root
||
parent: Expr
parent
!=
e: ?m.45269
e
-- recursion guard let
e: ?m.46217
e
withReducible: {n : TypeType ?u.45933} → [inst : ] → [inst : ] → {α : Type} → n αn α
withReducible
<|
whnf:
whnf
e: ?m.45269
e
guard: {f : TypeType ?u.46261} → [inst : ] → (p : Prop) → [inst : ] → f Unit
guard
e: ?m.46217
e
.
isApp:
isApp
-- all interesting ring expressions are applications letu,
α: let u := u; Q(Type u)
α
,
e: Q(«\$α»)
e
⟩ ←
inferTypeQ': ExprMetaM ((u : Level) × (α : let u := u; Q(Type u)) × Q(«\$α»))
inferTypeQ'
e: ?m.46217
e
let
: ?m.46545
synthInstanceQ: {u : Level} → (α : Q(Sort u)) → MetaM Q(«\$α»)
synthInstanceQ
(q(
CommSemiring: Type ?u.46532 → Type ?u.46532
CommSemiring
CommSemiring \$α: Level
\$
α: Type u
α
) : Q(
Type u: Level
Type u
)) let
c: ?m.46608
c
mkCache: {u : Level} → {α : Q(Type u)} → ( : Q(CommSemiring «\$α»)) → MetaM ()
mkCache
: ?m.46545
let
a: Q(«\$α»)
a
, _,
pa: Q(«\$e» = «\$a»)
pa
⟩ ← match
isAtomOrDerivable: {u : Level} → {α : Q(Type u)} → ( : Q(CommSemiring «\$α»)) → (e : Q(«\$α»)) → AtomM (Option (Option (Result (ExSum ) e)))
isAtomOrDerivable
: ?m.46545
c: ?m.46608
c
e: Q(«\$α»)
e
rctx: ?m.45244
rctx
s: ?m.45247
s
with |
none: {α : Type ?u.45608} →
none
=>
eval: {u : Level} → {α : Q(Type u)} → ( : Q(CommSemiring «\$α»)) → (e : Q(«\$α»)) → AtomM (Result (ExSum ) e)
eval
eval sα c e rctx s: SimpM (?m.46680 y✝)
: ?m.46545
eval sα c e rctx s: SimpM (?m.46680 y✝)
c: ?m.46608
c
eval sα c e rctx s: SimpM (?m.46680 y✝)
e: Q(«\$α»)
e
eval sα c e rctx s: SimpM (?m.46680 y✝)
rctx: ?m.45244
rctx
eval sα c e rctx s: SimpM (?m.46680 y✝)
s: ?m.45247
s
-- `none` indicates that `eval` will find something algebraic. |
some: {α : Type ?u.46777} → α
some
none: {α : Type ?u.45614} →
none
=>
failure: {f : Type ?u.46835 → Type ?u.46834} → [self : ] → {α : Type ?u.46835} → f α
failure
-- No point rewriting atoms |
some: {α : Type ?u.46877} → α
some
(
some: {α : Type ?u.46880} → α
some
r: Result (ExSum ) e
r
) =>
pure: {f : Type ?u.46939 → Type ?u.46938} → [self : Pure f] → {α : Type ?u.46939} → αf α
pure
pure r: SimpM (?m.46680 y✝)
r: Result (ExSum ) e
r
-- Nothing algebraic for `eval` to use, but `norm_num` simplifies. let
r: ?m.47375
r
nctx: ?m.45241
nctx
.
simp:
simp
{ expr :=
a: Q(«\$α»)
a
, proof? :=
pa: Q(«\$e» = «\$a»)
pa
} if
withReducible: {n : TypeType ?u.47419} → [inst : ] → [inst : ] → {α : Type} → n αn α
withReducible
<|
isDefEq:
isDefEq
r: ?m.47375
r
.
expr:
expr
e: Q(«\$α»)
e
then return
.done:
.done
{ expr :=
r: ?m.47375
r
.
expr:
expr
}
pure: {f : Type ?u.48055 → Type ?u.48054} → [self : Pure f] → {α : Type ?u.48055} → αf α
pure
(
.done:
.done
r: ?m.47375
r
) catch
_: ?m.48539
_
=>
pure: {f : Type ?u.48582 → Type ?u.48581} → [self : Pure f] → {α : Type ?u.48582} → αf α
pure
<|
.visit:
.visit
{ expr :=
e: ?m.45269
e
} let
post: ?m.45278
post
:= (
Simp.postDefault: Expr(Expr) →
Simp.postDefault
· fun _ ↦
none: {α : Type ?u.45285} →
none
)
(·.1):
(·.1)
<\$>
Simp.main: ExprSimp.ContextoptParam Simp.Methods { pre := fun e => pure (Simp.Step.visit { expr := e, proof? := none, dischargeDepth := 0 }), post := fun e => pure (Simp.Step.done { expr := e, proof? := none, dischargeDepth := 0 }), discharge? := fun x => pure none }
Simp.main
parent: Expr
parent
nctx: ?m.45241
nctx
.
ctx:
ctx
(methods := {
pre: (e : ?m.45269) → ?m.45274 e
pre
,
post: ?m.45278
post
}) variable [
CommSemiring: Type ?u.102140 → Type ?u.102140
CommSemiring
R: ?m.102137
R
] theorem
add_assoc_rev: ∀ (a b c : R), a + (b + c) = a + b + c
(
a: R
a
b: R
b
c: R
c
:
R: ?m.71595
R
) :
a: R
a
+ (
b: R
b
+
c: R
c
) =
a: R
a
+
b: R
b
+
c: R
c
:= (
add_assoc: ∀ {G : Type ?u.72601} [inst : ] (a b c : G), a + b + c = a + (b + c)
..).
symm: ∀ {α : Sort ?u.72622} {a b : α}, a = bb = a
symm
theorem
mul_assoc_rev: ∀ (a b c : R), a * (b * c) = a * b * c
mul_assoc_rev
(
a: R
a
b: R
b
c: R
c
:
R: ?m.72889
R
) :
a: R
a
* (
b: R
b
*
c: R
c
) =
a: R
a
*
b: R
b
*
c: R
c
:= (
mul_assoc: ∀ {G : Type ?u.73918} [inst : ] (a b c : G), a * b * c = a * (b * c)
mul_assoc
..).
symm: ∀ {α : Sort ?u.73938} {a b : α}, a = bb = a
symm
theorem
mul_neg: ∀ {R : Type u_1} [inst : Ring R] (a b : R), a * -b = -(a * b)
mul_neg
{
R: ?m.74054
R
} [
Ring: Type ?u.74057 → Type ?u.74057
Ring
R: ?m.74054
R
] (
a: R
a
b: R
b
:
R: ?m.74054
R
) :
a: R
a
* -
b: R
b
= -(
a: R
a
*
b: R
b
) :=

Goals accomplished! 🐙
R✝: Type ?u.74051

inst✝¹:

R: Type u_1

inst✝: Ring R

a, b: R

a * -b = -(a * b)

Goals accomplished! 🐙
theorem
add_neg: ∀ {R : Type u_1} [inst : Ring R] (a b : R), a + -b = a - b
{
R: ?m.74406
R
} [
Ring: Type ?u.74409 → Type ?u.74409
Ring
R: ?m.74406
R
] (
a: R
a
b: R
b
:
R: ?m.74406
R
) :
a: R
a
+ -
b: R
b
=
a: R
a
-
b: R
b
:= (
sub_eq_add_neg: ∀ {G : Type ?u.74593} [inst : ] (a b : G), a - b = a + -b
..).
symm: ∀ {α : Sort ?u.74611} {a b : α}, a = bb = a
symm
theorem
nat_rawCast_0: = 0
nat_rawCast_0
: (
Nat.rawCast: {α : Type ?u.74686} → [inst : ] → α
Nat.rawCast
0: ?m.74702
0
:
R: ?m.74678
R
) =
0: ?m.74927
0
:=

Goals accomplished! 🐙
R: Type u_1

inst✝:

= 0

Goals accomplished! 🐙
theorem
nat_rawCast_1: = 1
nat_rawCast_1
: (
Nat.rawCast: {α : Type ?u.75551} → [inst : ] → α
Nat.rawCast
1: ?m.75567
1
:
R: ?m.75543
R
) =
1: ?m.75792
1
:=

Goals accomplished! 🐙
R: Type u_1

inst✝:

= 1

Goals accomplished! 🐙
theorem
nat_rawCast_2: ∀ {n : } [inst : ],
nat_rawCast_2
[
Nat.AtLeastTwo:
Nat.AtLeastTwo
n: ?m.76381
n
] : (
Nat.rawCast: {α : Type ?u.76388} → [inst : ] → α
Nat.rawCast
n: ?m.76381
n
:
R: ?m.76374
R
) =
OfNat.ofNat: {α : Type ?u.76617} → (x : ) → [self : OfNat α x] → α
OfNat.ofNat
n: ?m.76381
n
:=
rfl: ∀ {α : Sort ?u.76767} {a : α}, a = a
rfl
theorem
int_rawCast_1: ∀ {R : Type u_1} [inst : Ring R],
int_rawCast_1
{
R: Type u_1
R
} [
Ring: Type ?u.76792 → Type ?u.76792
Ring
R: ?m.76789
R
] : (
Int.rawCast: {α : Type ?u.76797} → [inst : Ring α] → α
Int.rawCast
(
.negOfNat:
.negOfNat
1: ?m.76809
1
) :
R: ?m.76789
R
) = -
1: ?m.76827
1
:=

Goals accomplished! 🐙
R✝: Type ?u.76786

inst✝¹:

R: Type u_1

inst✝: Ring R

Goals accomplished! 🐙
theorem
int_rawCast_2: ∀ {n : } {R : Type u_1} [inst : Ring R] [inst_1 : ],
int_rawCast_2
{
R: ?m.78198
R
} [
Ring: Type ?u.78191 → Type ?u.78191
Ring
R: ?m.78198
R
] [
Nat.AtLeastTwo:
Nat.AtLeastTwo
n: ?m.78195
n
] : (
Int.rawCast: {α : Type ?u.78208} → [inst : Ring α] → α
Int.rawCast
(
.negOfNat:
.negOfNat
n: ?m.78195
n
) :
R: ?m.78198
R
) = -
OfNat.ofNat: {α : Type ?u.78226} → (x : ) → [self : OfNat α x] → α
OfNat.ofNat
n: ?m.78195
n
:=

Goals accomplished! 🐙
R✝: Type ?u.78185

inst✝²:

n:

R: Type u_1

inst✝¹: Ring R

inst✝

Goals accomplished! 🐙
theorem
rat_rawCast_2: ∀ {n : } {d : } {R : Type u_1} [inst : ], = n / d
rat_rawCast_2
{
R: Type u_1
R
} [
DivisionRing: Type ?u.79745 → Type ?u.79745
DivisionRing
R: ?m.79742
R
] : (
Rat.rawCast: {α : Type ?u.79750} → [inst : ] → α
Rat.rawCast
n: ?m.79717
n
d: ?m.79739
d
:
R: ?m.79742
R
) =
n: ?m.79717
n
/
d: ?m.79739
d
:=

Goals accomplished! 🐙
R✝: Type ?u.79695

inst✝¹:

n:

d:

R: Type u_1

inst✝:

= n / d

Goals accomplished! 🐙
/-- 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: {α : Type} → ConfigM α
M.run
(
s
:
IO.Ref:
IO.Ref
AtomM.State: Type
AtomM.State
) (
cfg: Config
cfg
:
RingNF.Config: Type
RingNF.Config
) (
x: M α
x
:
M:
M
α: ?m.80628
α
) :
MetaM:
MetaM
α: ?m.80628
α
:= do let
ctx: ?m.80896
ctx
:= { simpTheorems :=
#[← Elab.Tactic.simpOnlyBuiltins.foldlM (·.addConst ·) {}]: Array ?m.82602
#[←
Elab.Tactic.simpOnlyBuiltins:
Elab.Tactic.simpOnlyBuiltins
#[← Elab.Tactic.simpOnlyBuiltins.foldlM (·.addConst ·) {}]: Array ?m.82602
.
foldlM: {m : Type ?u.80709 → Type ?u.80708} → [inst : ] → {s : Type ?u.80709} → {α : Type ?u.80707} → (sαm s) → sList αm s
foldlM
#[← Elab.Tactic.simpOnlyBuiltins.foldlM (·.addConst ·) {}]: Array ?m.82602
(·.
#[← Elab.Tactic.simpOnlyBuiltins.foldlM (·.addConst ·) {}]: Array ?m.82602
·)
{}
#[← Elab.Tactic.simpOnlyBuiltins.foldlM (·.addConst ·) {}]: Array ?m.82602
]
congrTheorems := ←
getSimpCongrTheorems:
getSimpCongrTheorems
} let
simp: ?m.80900
simp
match
cfg: Config
cfg
.
mode:
mode
with |
.raw: RingMode
.raw
=>
pure: {f : Type ?u.80955 → Type ?u.80954} → [self : Pure f] → {α : Type ?u.80955} → αf α
pure
pure pure: MetaM (?m.80904 y✝)
pure: {f : Type ?u.80980 → Type ?u.80979} → [self : Pure f] → {α : Type ?u.80980} → αf α
pure
|
.SOP: RingMode
.SOP
=> let thms :
SimpTheorems: Type
SimpTheorems
:= {} let
thms: ?m.81256
thms
← [``
add_zero: ∀ {M : Type u} [inst : ] (a : M), a + 0 = a
, ``
add_assoc_rev: ∀ {R : Type u_1} [inst : ] (a b c : R), a + (b + c) = a + b + c
, ``
_root_.mul_one: ∀ {M : Type u} [inst : ] (a : M), a * 1 = a
_root_.mul_one
, ``
mul_assoc_rev: ∀ {R : Type u_1} [inst : ] (a b c : R), a * (b * c) = a * b * c
mul_assoc_rev
, ``
_root_.pow_one: ∀ {M : Type u} [inst : ] (a : M), a ^ 1 = a
_root_.pow_one
, ``
mul_neg: ∀ {R : Type u_1} [inst : Ring R] (a b : R), a * -b = -(a * b)
mul_neg
, ``
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 : ] → {s : Type ?u.81199} → {α : Type ?u.81197} → (sαm s) → sList αm s
foldlM
(·.
·) thms let
thms: ?m.81373
thms
← [``
nat_rawCast_0: ∀ {R : Type u_1} [inst : ], = 0
nat_rawCast_0
, ``
nat_rawCast_1: ∀ {R : Type u_1} [inst : ], = 1
nat_rawCast_1
, ``
nat_rawCast_2: ∀ {R : Type u_1} [inst : ] {n : } [inst_1 : ],
nat_rawCast_2
, ``
int_rawCast_1: ∀ {R : Type u_1} [inst : Ring R],
int_rawCast_1
, ``
int_rawCast_2: ∀ {n : } {R : Type u_1} [inst : Ring R] [inst_1 : ],
int_rawCast_2
, ``
rat_rawCast_2: ∀ {n : } {d : } {R : Type u_1} [inst : ], = n / d
rat_rawCast_2
].
foldlM: {m : Type ?u.81316 → Type ?u.81315} → [inst : ] → {s : Type ?u.81316} → {α : Type ?u.81314} → (sαm s) → sList αm s
foldlM
(·.
· (post :=
false: Bool
false
))
thms: ?m.81256
thms
let
ctx': ?m.81376
ctx'
:= {
ctx: ?m.80896
ctx
with simpTheorems := #[
thms: ?m.81373
thms
] }
pure: {f : Type ?u.81422 → Type ?u.81421} → [self : Pure f] → {α : Type ?u.81422} → αf α
pure
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: Type
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:
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: ExprSimp.ContextoptParam Simp.Methods { pre := fun e => pure (Simp.Step.visit { expr := e, proof? := none, dischargeDepth := 0 }), post := fun e => pure (Simp.Step.done { expr := e, proof? := none, dischargeDepth := 0 }), discharge? := fun x => pure none }
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:
expr
(← Simp.main r'.expr ctx' (methods := Simp.DefaultMethods.methods)): ?m.82876
ctx': ?m.81376
ctx'
(← Simp.main r'.expr ctx' (methods := Simp.DefaultMethods.methods)): ?m.82876
(methods :=
Simp.DefaultMethods.methods: Simp.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} → α × βα
1
let
nctx: ?m.81812
nctx
:= {
ctx: ?m.80896
ctx
, simp } let rec /-- The recursive context. -/
rctx: ?m.81862
rctx
:= { red :=
cfg: Config
cfg
.
red:
red
,
evalAtom: ?m.81865
evalAtom
}, /-- The atom evaluator calls either `RingNF.rewrite` recursively, or nothing depending on `cfg.recursive`. -/
evalAtom:
evalAtom
:= if
cfg: Config
cfg
.
recursive:
recursive
then fun
e: ?m.81964
e
rewrite:
rewrite
e: ?m.81964
e
false: Bool
false
nctx: ?m.81812
nctx
rctx: ?m.81862
rctx
s
else fun
e: ?m.81974
e
pure: {f : Type ?u.81977 → Type ?u.81976} → [self : Pure f] → {α : Type ?u.81977} → αf α
pure
{ expr :=
e: ?m.81974
e
}
x: M α
x
nctx: ?m.81812
nctx
rctx: ?m.81862
rctx
s
/-- Overrides the default error message in `ring1` to use a prettified version of the goal. -/ initialize
ringCleanupRef: IO.Ref ()
ringCleanupRef
.
set: {σ : Type} → {m : } → [inst : MonadLiftT (ST σ) m] → {α : Type} → ST.Ref σ ααm Unit
set
fun
e: ?m.86768
e
=> do
M.run: {α : Type} → ConfigM α
M.run
(← IO.mkRef {}): ?m.87076
(←
IO.mkRef: {α : Type} → αBaseIO ()
IO.mkRef
(← IO.mkRef {}): ?m.87076
{}
(← IO.mkRef {}): ?m.87076
)
{ recursive :=
false: Bool
false
} fun
nctx: ?m.87089
nctx
_: ?m.87092
_
_: ?m.87095
_
=> return
(← nctx.simp { expr := e } nctx.ctx |>.run {}): ?m.87399
(←
nctx: ?m.87089
nctx
(← nctx.simp { expr := e } nctx.ctx |>.run {}): ?m.87399
.
simp:
simp
(← nctx.simp { expr := e } nctx.ctx |>.run {}): ?m.87399
{ expr :=
e: ?m.86768
e
(← nctx.simp { expr := e } nctx.ctx |>.run {}): ?m.87399
}
nctx: ?m.87089
nctx
(← nctx.simp { expr := e } nctx.ctx |>.run {}): ?m.87399
.
ctx:
ctx
(← nctx.simp { expr := e } nctx.ctx |>.run {}): ?m.87399
|>.
run: {ω σ : Type} → {m : } → [inst : ] → [inst : MonadLiftT (ST ω) m] → {α : Type} → StateRefT' ω σ m ασm (α × σ)
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} → α × βα
1
.
expr:
expr
open Elab.Tactic Parser.Tactic /-- Use `ring_nf` to rewrite the main goal. -/ def
ringNFTarget:
ringNFTarget
(
s
:
IO.Ref:
IO.Ref
AtomM.State: Type
AtomM.State
) (
cfg: Config
cfg
:
Config: Type
Config
) :
TacticM:
TacticM
Unit: Type
Unit
:=
withMainContext: {α : Type} →
withMainContext
do let
goal: ?m.89443
goal
getMainGoal:
getMainGoal
let
tgt: ?m.89801
tgt
instantiateMVars: {m : } → [inst : ] → [inst : ] → Exprm Expr
instantiateMVars
(← goal.getType): ?m.89672
(←
goal: ?m.89443
goal
(← goal.getType): ?m.89672
.
getType:
getType
(← goal.getType): ?m.89672
)
let
r: ?m.89891
r
M.run: {α : Type} → ConfigM α
M.run
s
cfg: Config
cfg
<|
rewrite:
rewrite
tgt: ?m.89801
tgt
if
r: ?m.89891
r
.
expr:
expr
.
isConstOf: Expr
isConstOf
``
True: Prop
True
then
goal: ?m.89443
goal
.
assign: {m : } → [inst : ] → MVarIdExprm Unit
assign
(← mkOfEqTrue (← r.getProof)): ?m.90105
(←
mkOfEqTrue:
mkOfEqTrue
(← mkOfEqTrue (← r.getProof)): ?m.90105
(← r.getProof): ?m.90045
(←
r: ?m.89891
r
(← r.getProof): ?m.90045
.
getProof:
getProof
(← r.getProof): ?m.90045
)
(← mkOfEqTrue (← r.getProof)): ?m.90105
)
replaceMainGoal:
replaceMainGoal
[]: List ?m.90178
[]
else
replaceMainGoal:
replaceMainGoal
[← applySimpResultToTarget goal tgt r]: List ?m.90306
[←
applySimpResultToTarget: MVarId
applySimpResultToTarget
[← applySimpResultToTarget goal tgt r]: List ?m.90306
goal: ?m.89443
goal
[← applySimpResultToTarget goal tgt r]: List ?m.90306
tgt: ?m.89801
tgt
[← applySimpResultToTarget goal tgt r]: List ?m.90306
r: ?m.89891
r
[← applySimpResultToTarget goal tgt r]: List ?m.90306
]
/-- Use `ring_nf` to rewrite hypothesis `h`. -/ def
ringNFLocalDecl:
ringNFLocalDecl
(
s
:
IO.Ref:
IO.Ref
AtomM.State: Type
AtomM.State
) (
cfg: Config
cfg
:
Config: Type
Config
) (
fvarId: FVarId
fvarId
:
FVarId: Type
FVarId
) :
TacticM:
TacticM
Unit: Type
Unit
:=
withMainContext: {α : Type} →
withMainContext
do let
tgt: ?m.92443
tgt
instantiateMVars: {m : } → [inst : ] → [inst : ] → Exprm Expr
instantiateMVars
(← fvarId.getType): ?m.92314
(←
fvarId: FVarId
fvarId
(← fvarId.getType): ?m.92314
.
getType:
getType
(← fvarId.getType): ?m.92314
)
let
goal: ?m.92497
goal
getMainGoal:
getMainGoal
let
myres: ?m.92587
myres
M.run: {α : Type} → ConfigM α
M.run
s
cfg: Config
cfg
<|
rewrite:
rewrite
tgt: ?m.92443
tgt
match
applySimpResultToLocalDecl: MVarIdFVarIdSimp.ResultBoolMetaM ()
applySimpResultToLocalDecl
goal: ?m.92497
goal
fvarId: FVarId
fvarId
myres: ?m.92587
myres
false: Bool
false
with |
none: {α : Type ?u.92668} →
none
=>
replaceMainGoal:
replaceMainGoal
[]: List ?m.92687
[]
|
some: {α : Type ?u.92698} → α
some
(_,
newGoal: MVarId
newGoal
) =>
replaceMainGoal:
replaceMainGoal
[
newGoal: MVarId
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: ParserDescr
ringNF
) "ring_nf"
tk: ?m.94473
tk
:"!"?
cfg: ?m.94466
cfg
:(
config: ParserDescr
config
?)
loc: ?m.94450
loc
:(
ppSpace: Parser.Parser
ppSpace
location: ParserDescr
location
)? : tactic => do let mut
cfg: ?m.94775
cfg
elabConfig:
elabConfig
cfg: ?m.94466
cfg
if
tk: ?m.94473
tk
.
isSome: {α : Type ?u.94790} → Bool
isSome
then
cfg: ?m.94775
cfg
:= {
cfg: ?m.94775
cfg
with red := .default } let
loc: ?m.95136
loc
:= (
loc: ?m.94450
loc
.
map: {α : Type ?u.95138} → {β : Type ?u.95137} → (αβ) →
map
expandLocation:
expandLocation
).
getD: {α : Type ?u.95269} → αα
getD
(
.targets:
.targets
#[]: Array ?m.95275
#[]
true: Bool
true
) let
s: ?m.95678
s
IO.mkRef: {α : Type} → αBaseIO ()
IO.mkRef
{}
withLocation: Location() → () →
withLocation
loc: ?m.95136
loc
(
ringNFLocalDecl:
ringNFLocalDecl
s: ?m.95678
s
cfg: Config
cfg
) (
ringNFTarget:
ringNFTarget
s: ?m.95678
s
cfg: Config
cfg
) fun
_: ?m.95729
_
throwError "ring_nf failed": ?m.95731 ?m.95732
throwError
throwError "ring_nf failed": ?m.95731 ?m.95732
"ring_nf failed"
@[inherit_doc
ringNF: ParserDescr
ringNF
] macro "ring_nf!"
cfg: ?m.99107
cfg
:(
config: ParserDescr
config
)?
loc: ?m.99091
loc
:(
ppSpace: Parser.Parser
ppSpace
location: ParserDescr
location
)? : tactic => `(tactic| ring_nf ! \$(
cfg: ?m.99107
cfg
)? \$(
loc: ?m.99091
loc
)?) @[inherit_doc
ringNF: ParserDescr
ringNF
] syntax (name :=
ringNFConv: ParserDescr
ringNFConv
) "ring_nf" "!"? (
config: ParserDescr
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: ParserDescr
ring1NF
) "ring1_nf"
tk: ?m.102199
tk
:"!"?
cfg: ?m.102190
cfg
:(
config: ParserDescr
config
?) : tactic => do let mut
cfg: ?m.102502
cfg
elabConfig:
elabConfig
cfg: ?m.102190
cfg
if
tk: ?m.102199
tk
.
isSome: {α : Type ?u.102517} → Bool
isSome
then
cfg: ?m.102595
cfg
:= {
cfg: ?m.102502
cfg
with red := .default } let
s: ?m.103260
s
IO.mkRef: {α : Type} → αBaseIO ()
IO.mkRef
{}
liftMetaMAtMain: {α : Type} → (MVarId) →
liftMetaMAtMain
fun
g: ?m.103273
g
M.run: {α : Type} → ConfigM α
M.run
s: ?m.103260
s
cfg: Config
cfg
<|
proveEq:
proveEq
g: ?m.103273
g
@[inherit_doc
ring1NF: ParserDescr
ring1NF
] macro "ring1_nf!"
cfg: ?m.105975
cfg
:(
config: ParserDescr
config
)? : tactic => `(tactic| ring1_nf ! \$(
cfg: ?m.105975
cfg
)?) /-- Elaborator for the `ring_nf` tactic. -/ @[tactic
ringNFConv: ParserDescr
ringNFConv
] def
elabRingNFConv: Tactic
elabRingNFConv
:
Tactic: Type
Tactic
:= fun
stx: ?m.108291
stx
match
stx: ?m.108291
stx
with | `(conv| ring_nf \$[!%\$
tk: ?m.108333 x✝
tk
]? \$(
_cfg: ?m.108737
_cfg
)?) =>
withMainContext: {α : Type} →
withMainContext
do let mut
cfg: ?m.109011
cfg
elabConfig:
elabConfig
stx: ?m.108291
stx
[
2: ?m.108845
2
] if
tk: ?m.108333 x✝
tk
.
isSome: {α : Type ?u.109026} → Bool
isSome
then
cfg: ?m.109096
cfg
:= {
cfg: ?m.109011
cfg
with red := .default } let
s: ?m.109759
s
IO.mkRef: {α : Type} → αBaseIO ()
IO.mkRef
{}
Conv.applySimpResult:
Conv.applySimpResult
(← M.run s cfg <| rewrite (← instantiateMVars (← Conv.getLhs))): ?m.110166
(←
M.run: {α : Type} → ConfigM α
M.run
(← M.run s cfg <| rewrite (← instantiateMVars (← Conv.getLhs))): ?m.110166
s: ?m.109759
s
(← M.run s cfg <| rewrite (← instantiateMVars (← Conv.getLhs))): ?m.110166
cfg: Config
cfg
(← M.run s cfg <| rewrite (← instantiateMVars (← Conv.getLhs))): ?m.110166
<|
rewrite:
rewrite
(← M.run s cfg <| rewrite (← instantiateMVars (← Conv.getLhs))): ?m.110166
(← instantiateMVars (← Conv.getLhs)): ?m.109942
(←
instantiateMVars: {m : } → [inst : ] → [inst : ] → Exprm Expr
instantiateMVars
(← instantiateMVars (← Conv.getLhs)): ?m.109942
(← Conv.getLhs): ?m.109813
(←
Conv.getLhs:
Conv.getLhs
(← Conv.getLhs): ?m.109813
)
(← instantiateMVars (← Conv.getLhs)): ?m.109942
)
(← M.run s cfg <| rewrite (← instantiateMVars (← Conv.getLhs))): ?m.110166
)
| _ =>
Elab.throwUnsupportedSyntax: {m : Type ?u.110297 → Type ?u.110296} → {α : Type ?u.110297} → [inst : ] → m α
Elab.throwUnsupportedSyntax
@[inherit_doc
ringNF: ParserDescr
ringNF
] macro "ring_nf!"
cfg: ?m.113406
cfg
:(
config: ParserDescr
config
)? : conv => `(conv| ring_nf ! \$(
cfg: ?m.113406
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|
`(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
"Try this: ring_nf")
@[inherit_doc ring] macro "ring!" : tactic =>
`(tactic| first | ring1! | ring_nf!; trace "Try this: ring_nf!"): ?m.118468 ?m.118471
`(tactic|
`(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
"Try this: ring_nf!")
/-- 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: ParserDescr
ringConv
) "ring" : conv =>
`(conv| first | discharge => ring1 | ring_nf; tactic => trace "Try this: ring_nf"): ?m.121060 ?m.121063
`(conv|
`(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
"Try this: ring_nf")
@[inherit_doc
ringConv: ParserDescr
ringConv
] macro "ring!" : conv =>
`(conv| first | discharge => ring1! | ring_nf!; tactic => trace "Try this: ring_nf!"): ?m.124091 ?m.124094
`(conv|
`(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
"Try this: ring_nf!")