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.
/-
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: {a : Level} β†’ {arg : Q(Type a)} β†’ {sΞ± : Q(CommSemiring Β«$argΒ»)} β†’ {a_1 : Q(Β«$argΒ»)} β†’ ExBase sΞ± a_1 β†’ Bool
ExBase.isAtom
:
ExBase: {u : Level} β†’ {Ξ± : Q(Type u)} β†’ Q(CommSemiring Β«$Ξ±Β») β†’ Q(Β«$Ξ±Β») β†’ Type
ExBase
sΞ±: ?m.6
sΞ±
a: ?m.16
a
β†’
Bool: Type
Bool
|
.atom: {u : Level} β†’ {Ξ± : Q(Type u)} β†’ {sΞ± : Q(CommSemiring Β«$Ξ±Β»)} β†’ {e : Q(Β«$Ξ±Β»)} β†’ β„• β†’ ExBase sΞ± e
.atom
_ =>
true: Bool
true
| _ =>
false: Bool
false
/-- True if this represents an atomic expression. -/ def
ExProd.isAtom: {a : Level} β†’ {arg : Q(Type a)} β†’ {sΞ± : Q(CommSemiring Β«$argΒ»)} β†’ {a_1 : Q(Β«$argΒ»)} β†’ ExProd sΞ± a_1 β†’ Bool
ExProd.isAtom
:
ExProd: {u : Level} β†’ {Ξ± : Q(Type u)} β†’ Q(CommSemiring Β«$Ξ±Β») β†’ Q(Β«$Ξ±Β») β†’ Type
ExProd
sΞ±: ?m.1165
sΞ±
a: ?m.1175
a
β†’
Bool: Type
Bool
|
.mul: {u : Level} β†’ {Ξ± : Q(Type u)} β†’ {sΞ± : Q(CommSemiring Β«$Ξ±Β»)} β†’ {x : Q(Β«$Ξ±Β»)} β†’ {e : Q(β„•)} β†’ {b : Q(Β«$Ξ±Β»)} β†’ ExBase sΞ± x β†’ ExProd sβ„• e β†’ ExProd sΞ± b β†’ ExProd sΞ± q(Β«$xΒ» ^ Β«$eΒ» * Β«$bΒ»)
.mul
va₁: ExBase sΞ± x✝
va₁
(
.const: {u : Level} β†’ {Ξ± : Q(Type u)} β†’ {sΞ± : Q(CommSemiring Β«$Ξ±Β»)} β†’ {e : Q(Β«$Ξ±Β»)} β†’ β„š β†’ optParam (Option Expr) none β†’ ExProd sΞ± e
.const
1 _) (
.const: {u : Level} β†’ {Ξ± : Q(Type u)} β†’ {sΞ± : Q(CommSemiring Β«$Ξ±Β»)} β†’ {e : Q(Β«$Ξ±Β»)} β†’ β„š β†’ optParam (Option Expr) none β†’ ExProd sΞ± e
.const
1 _) =>
va₁: ExBase sΞ± x✝
va₁
.
isAtom: {a : Level} β†’ {arg : Q(Type a)} β†’ {sΞ± : Q(CommSemiring Β«$argΒ»)} β†’ {a_1 : Q(Β«$argΒ»)} β†’ ExBase sΞ± a_1 β†’ Bool
isAtom
| _ =>
false: Bool
false
/-- True if this represents an atomic expression. -/ def
ExSum.isAtom: {a : Level} β†’ {arg : Q(Type a)} β†’ {sΞ± : Q(CommSemiring Β«$argΒ»)} β†’ {a_1 : Q(Β«$argΒ»)} β†’ ExSum sΞ± a_1 β†’ Bool
ExSum.isAtom
:
ExSum: {u : Level} β†’ {Ξ± : Q(Type u)} β†’ Q(CommSemiring Β«$Ξ±Β») β†’ Q(Β«$Ξ±Β») β†’ Type
ExSum
sΞ±: ?m.31171
sΞ±
a: ?m.31181
a
β†’
Bool: Type
Bool
|
.add: {u : Level} β†’ {Ξ± : Q(Type u)} β†’ {sΞ± : Q(CommSemiring Β«$Ξ±Β»)} β†’ {a b : Q(Β«$Ξ±Β»)} β†’ ExProd sΞ± a β†’ ExSum sΞ± b β†’ ExSum sΞ± q(Β«$aΒ» + Β«$bΒ»)
.add
va₁: ExProd sΞ± a✝
va₁
vaβ‚‚: ExSum sΞ± b✝
vaβ‚‚
=> match
vaβ‚‚: ExSum sΞ± b✝
vaβ‚‚
with -- FIXME: this takes a while to compile as one match |
.zero: ExSum sΞ± q(0)
.zero
=>
va₁: ExProd sΞ± a✝
va₁
.
isAtom: {a : Level} β†’ {arg : Q(Type a)} β†’ {sΞ± : Q(CommSemiring Β«$argΒ»)} β†’ {a_1 : Q(Β«$argΒ»)} β†’ ExProd sΞ± a_1 β†’ Bool
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: TransparencyMode β†’ Bool β†’ RingMode β†’ Config
Config
where /-- the reducibility setting to use when comparing atoms for defeq -/ red :=
TransparencyMode.reducible: TransparencyMode
TransparencyMode.reducible
/-- if true, atoms inside ring expressions will be reduced recursively -/
recursive: Config β†’ Bool
recursive
:=
true: Bool
true
/-- The normalization style. -/
mode: Config β†’ RingMode
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: Syntax β†’ Elab.TermElabM Config
elabConfig
Config: Type
Config
/-- The read-only state of the `RingNF` monad. -/ structure
Context: Simp.Context β†’ (Simp.Result β†’ SimpM Simp.Result) β†’ Context
Context
where /-- A basically empty simp context, passed to the `simp` traversal in `RingNF.rewrite`. -/
ctx: Context β†’ Simp.Context
ctx
:
Simp.Context: Type
Simp.Context
/-- A cleanup routine, which simplifies normalized polynomials to a more human-friendly format. -/
simp: Context β†’ Simp.Result β†’ SimpM Simp.Result
simp
:
Simp.Result: Type
Simp.Result
β†’
SimpM: Type β†’ Type
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: Type β†’ Type
M
:=
ReaderT: Type ?u.45219 β†’ (Type ?u.45219 β†’ Type ?u.45218) β†’ Type ?u.45219 β†’ Type (max?u.45219?u.45218)
ReaderT
Context: Type
Context
AtomM: Type β†’ Type
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: Expr β†’ optParam Bool true β†’ M Simp.Result
rewrite
(
parent: Expr
parent
:
Expr: Type
Expr
) (root :=
true: Bool
true
) :
M: Type β†’ Type
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 : Type β†’ Type ?u.45722} β†’ [inst : Alternative f] β†’ (p : Prop) β†’ [inst : Decidable p] β†’ f Unit
guard
<| root ||
parent: Expr
parent
!=
e: ?m.45269
e
-- recursion guard let
e: ?m.46217
e
←
withReducible: {n : Type β†’ Type ?u.45933} β†’ [inst : MonadControlT MetaM n] β†’ [inst : Monad n] β†’ {Ξ± : Type} β†’ n Ξ± β†’ n Ξ±
withReducible
<|
whnf: Expr β†’ MetaM Expr
whnf
e: ?m.45269
e
guard: {f : Type β†’ Type ?u.46261} β†’ [inst : Alternative f] β†’ (p : Prop) β†’ [inst : Decidable p] β†’ f Unit
guard
e: ?m.46217
e
.
isApp: Expr β†’ Bool
isApp
-- all interesting ring expressions are applications let ⟨u,
Ξ±: let u := u; Q(Type u)
Ξ±
,
e: Q(Β«$Ξ±Β»)
e
⟩ ←
inferTypeQ': Expr β†’ MetaM ((u : Level) Γ— (Ξ± : let u := u; Q(Type u)) Γ— Q(Β«$Ξ±Β»))
inferTypeQ'
e: ?m.46217
e
let
sΞ±: ?m.46545
sΞ±
←
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)} β†’ (sΞ± : Q(CommSemiring Β«$Ξ±Β»)) β†’ MetaM (Ring.Cache sΞ±)
mkCache
sΞ±: ?m.46545
sΞ±
let ⟨
a: Q(Β«$Ξ±Β»)
a
, _,
pa: Q(Β«$eΒ» = Β«$aΒ»)
pa
⟩ ← match ←
isAtomOrDerivable: {u : Level} β†’ {Ξ± : Q(Type u)} β†’ (sΞ± : Q(CommSemiring Β«$Ξ±Β»)) β†’ Ring.Cache sΞ± β†’ (e : Q(Β«$Ξ±Β»)) β†’ AtomM (Option (Option (Result (ExSum sΞ±) e)))
isAtomOrDerivable
sΞ±: ?m.46545
sΞ±
c: ?m.46608
c
e: Q(Β«$Ξ±Β»)
e
rctx: ?m.45244
rctx
s: ?m.45247
s
with |
none: {Ξ± : Type ?u.45608} β†’ Option Ξ±
none
=>
eval: {u : Level} β†’ {Ξ± : Q(Type u)} β†’ (sΞ± : Q(CommSemiring Β«$Ξ±Β»)) β†’ Ring.Cache sΞ± β†’ (e : Q(Β«$Ξ±Β»)) β†’ AtomM (Result (ExSum sΞ±) e)
eval
eval sα c e rctx s: SimpM (?m.46680 y✝)
sΞ±: ?m.46545
sΞ±
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} β†’ Ξ± β†’ Option Ξ±
some
none: {Ξ± : Type ?u.45614} β†’ Option Ξ±
none
=>
failure: {f : Type ?u.46835 β†’ Type ?u.46834} β†’ [self : Alternative f] β†’ {Ξ± : Type ?u.46835} β†’ f Ξ±
failure
-- No point rewriting atoms |
some: {Ξ± : Type ?u.46877} β†’ Ξ± β†’ Option Ξ±
some
(
some: {Ξ± : Type ?u.46880} β†’ Ξ± β†’ Option Ξ±
some
r: Result (ExSum sΞ±) 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 sΞ±) e
r
-- Nothing algebraic for `eval` to use, but `norm_num` simplifies. let
r: ?m.47375
r
←
nctx: ?m.45241
nctx
.
simp: Context β†’ Simp.Result β†’ SimpM Simp.Result
simp
{ expr :=
a: Q(Β«$Ξ±Β»)
a
, proof? :=
pa: Q(Β«$eΒ» = Β«$aΒ»)
pa
} if ←
withReducible: {n : Type β†’ Type ?u.47419} β†’ [inst : MonadControlT MetaM n] β†’ [inst : Monad n] β†’ {Ξ± : Type} β†’ n Ξ± β†’ n Ξ±
withReducible
<|
isDefEq: Expr β†’ Expr β†’ MetaM Bool
isDefEq
r: ?m.47375
r
.
expr: Simp.Result β†’ Expr
expr
e: Q(Β«$Ξ±Β»)
e
then return
.done: Simp.Result β†’ Simp.Step
.done
{ expr :=
r: ?m.47375
r
.
expr: Simp.Result β†’ Expr
expr
}
pure: {f : Type ?u.48055 β†’ Type ?u.48054} β†’ [self : Pure f] β†’ {Ξ± : Type ?u.48055} β†’ Ξ± β†’ f Ξ±
pure
(
.done: Simp.Result β†’ Simp.Step
.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: Simp.Result β†’ Simp.Step
.visit
{ expr :=
e: ?m.45269
e
} let
post: ?m.45278
post
:= (
Simp.postDefault: Expr β†’ (Expr β†’ SimpM (Option Expr)) β†’ SimpM Simp.Step
Simp.postDefault
Β· fun _ ↦
none: {Ξ± : Type ?u.45285} β†’ Option Ξ±
none
) (Β·.1) <$>
Simp.main: Expr β†’ Simp.Context β†’ optParam Simp.UsedSimps βˆ… β†’ optParam 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 } β†’ MetaM (Simp.Result Γ— Simp.UsedSimps)
Simp.main
parent: Expr
parent
nctx: ?m.45241
nctx
.
ctx: Context β†’ Simp.Context
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
add_assoc_rev
(
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 : AddSemigroup G] (a b c : G), 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: 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 : Semigroup G] (a b c : G), a * b * c = a * (b * c)
mul_assoc
..).
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: ?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✝¹: CommSemiring R✝

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
add_neg
{
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 : SubNegMonoid G] (a b : G), 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 = 0
nat_rawCast_0
: (
Nat.rawCast: {Ξ± : Type ?u.74686} β†’ [inst : AddMonoidWithOne Ξ±] β†’ β„• β†’ Ξ±
Nat.rawCast
0: ?m.74702
0
:
R: ?m.74678
R
) =
0: ?m.74927
0
:=

Goals accomplished! πŸ™
R: Type u_1

inst✝: CommSemiring R



Goals accomplished! πŸ™
theorem
nat_rawCast_1: Nat.rawCast 1 = 1
nat_rawCast_1
: (
Nat.rawCast: {Ξ± : Type ?u.75551} β†’ [inst : AddMonoidWithOne Ξ±] β†’ β„• β†’ Ξ±
Nat.rawCast
1: ?m.75567
1
:
R: ?m.75543
R
) =
1: ?m.75792
1
:=

Goals accomplished! πŸ™
R: Type u_1

inst✝: CommSemiring R



Goals accomplished! πŸ™
theorem
nat_rawCast_2: βˆ€ {n : β„•} [inst : Nat.AtLeastTwo n], Nat.rawCast n = OfNat.ofNat n
nat_rawCast_2
[
Nat.AtLeastTwo: β„• β†’ Prop
Nat.AtLeastTwo
n: ?m.76381
n
] : (
Nat.rawCast: {Ξ± : Type ?u.76388} β†’ [inst : AddMonoidWithOne Ξ±] β†’ β„• β†’ Ξ±
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 (Int.negOfNat 1) = -1
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✝¹: CommSemiring R✝

R: Type u_1

inst✝: Ring R



Goals accomplished! πŸ™
theorem
int_rawCast_2: βˆ€ {n : β„•} {R : Type u_1} [inst : Ring R] [inst_1 : Nat.AtLeastTwo n], Int.rawCast (Int.negOfNat n) = -OfNat.ofNat n
int_rawCast_2
{
R: ?m.78198
R
} [
Ring: Type ?u.78191 β†’ Type ?u.78191
Ring
R: ?m.78198
R
] [
Nat.AtLeastTwo: β„• β†’ Prop
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✝²: CommSemiring R✝

n: β„•

R: Type u_1

inst✝¹: Ring R

inst✝: Nat.AtLeastTwo n



Goals accomplished! πŸ™
theorem
rat_rawCast_2: βˆ€ {n : β„€} {d : β„•} {R : Type u_1} [inst : DivisionRing R], Rat.rawCast n d = ↑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 : DivisionRing Ξ±] β†’ β„€ β†’ β„• β†’ Ξ±
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✝¹: CommSemiring R✝

n: β„€

d: β„•

R: Type u_1

inst✝: DivisionRing R


Rat.rawCast n d = ↑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} β†’ IO.Ref AtomM.State β†’ Config β†’ M Ξ± β†’ MetaM Ξ±
M.run
(s :
IO.Ref: Type β†’ Type
IO.Ref
AtomM.State: Type
AtomM.State
) (
cfg: Config
cfg
:
RingNF.Config: Type
RingNF.Config
) (
x: M Ξ±
x
:
M: Type β†’ Type
M
Ξ±: ?m.80628
Ξ±
) :
MetaM: Type β†’ Type
MetaM
Ξ±: ?m.80628
Ξ±
:= do let
ctx: ?m.80896
ctx
:= { simpTheorems :=
#[← Elab.Tactic.simpOnlyBuiltins.foldlM (Β·.addConst Β·) {}]: Array ?m.82602
#[←
Elab.Tactic.simpOnlyBuiltins: List Name
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
foldlM
#[← Elab.Tactic.simpOnlyBuiltins.foldlM (Β·.addConst Β·) {}]: Array ?m.82602
(Β·.
addConst: SimpTheorems β†’ Name β†’ optParam Bool true β†’ optParam Bool false β†’ optParam β„• 1000 β†’ MetaM SimpTheorems
addConst
#[← Elab.Tactic.simpOnlyBuiltins.foldlM (Β·.addConst Β·) {}]: Array ?m.82602
Β·)
{}
#[← Elab.Tactic.simpOnlyBuiltins.foldlM (Β·.addConst Β·) {}]: Array ?m.82602
]
congrTheorems := ←
getSimpCongrTheorems: MetaM SimpCongrTheorems
getSimpCongrTheorems
} let
simp: ?m.80900
simp
← match
cfg: Config
cfg
.
mode: Config β†’ RingMode
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 : AddZeroClass M] (a : M), a + 0 = a
add_zero
, ``
add_assoc_rev: βˆ€ {R : Type u_1} [inst : CommSemiring R] (a b c : R), a + (b + c) = a + b + c
add_assoc_rev
, ``
_root_.mul_one: βˆ€ {M : Type u} [inst : MulOneClass M] (a : M), a * 1 = a
_root_.mul_one
, ``
mul_assoc_rev: βˆ€ {R : Type u_1} [inst : CommSemiring R] (a b c : R), a * (b * c) = a * b * c
mul_assoc_rev
, ``
_root_.pow_one: βˆ€ {M : Type u} [inst : Monoid M] (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
add_neg
].
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: SimpTheorems β†’ Name β†’ optParam Bool true β†’ optParam Bool false β†’ optParam β„• 1000 β†’ MetaM SimpTheorems
addConst
Β·) thms let
thms: ?m.81373
thms
← [``
nat_rawCast_0: βˆ€ {R : Type u_1} [inst : CommSemiring R], Nat.rawCast 0 = 0
nat_rawCast_0
, ``
nat_rawCast_1: βˆ€ {R : Type u_1} [inst : CommSemiring R], Nat.rawCast 1 = 1
nat_rawCast_1
, ``
nat_rawCast_2: βˆ€ {R : Type u_1} [inst : CommSemiring R] {n : β„•} [inst_1 : Nat.AtLeastTwo n], Nat.rawCast n = OfNat.ofNat n
nat_rawCast_2
, ``
int_rawCast_1: βˆ€ {R : Type u_1} [inst : Ring R], Int.rawCast (Int.negOfNat 1) = -1
int_rawCast_1
, ``
int_rawCast_2: βˆ€ {n : β„•} {R : Type u_1} [inst : Ring R] [inst_1 : Nat.AtLeastTwo n], Int.rawCast (Int.negOfNat n) = -OfNat.ofNat n
int_rawCast_2
, ``
rat_rawCast_2: βˆ€ {n : β„€} {d : β„•} {R : Type u_1} [inst : DivisionRing R], Rat.rawCast n d = ↑n / ↑d
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: SimpTheorems β†’ Name β†’ optParam Bool true β†’ optParam Bool false β†’ optParam β„• 1000 β†’ MetaM SimpTheorems
addConst
Β· (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.Result β†’ Simp.Result β†’ MetaM Simp.Result
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: Expr β†’ Simp.Context β†’ optParam Simp.UsedSimps βˆ… β†’ optParam 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 } β†’ MetaM (Simp.Result Γ— Simp.UsedSimps)
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.Result β†’ 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,
evalAtom: ?m.81865
evalAtom
}, /-- The atom evaluator calls either `RingNF.rewrite` recursively, or nothing depending on `cfg.recursive`. -/
evalAtom: IO.Ref AtomM.State β†’ Config β†’ Context β†’ Expr β†’ MetaM Simp.Result
evalAtom
:= if
cfg: Config
cfg
.
recursive: Config β†’ Bool
recursive
then fun
e: ?m.81964
e
↦
rewrite: Expr β†’ optParam Bool true β†’ M Simp.Result
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 (Expr β†’ MetaM Expr)
ringCleanupRef
.
set: {Οƒ : Type} β†’ {m : Type β†’ Type} β†’ [inst : MonadLiftT (ST Οƒ) m] β†’ {Ξ± : Type} β†’ ST.Ref Οƒ Ξ± β†’ Ξ± β†’ m Unit
set
fun
e: ?m.86768
e
=> do
M.run: {Ξ± : Type} β†’ IO.Ref AtomM.State β†’ Config β†’ M Ξ± β†’ MetaM Ξ±
M.run
(← IO.mkRef {}): ?m.87076
(←
IO.mkRef: {Ξ± : Type} β†’ Ξ± β†’ BaseIO (IO.Ref Ξ±)
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: Context β†’ Simp.Result β†’ SimpM Simp.Result
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: Context β†’ Simp.Context
ctx
(← nctx.simp { expr := e } nctx.ctx |>.run {}): ?m.87399
|>.
run: {Ο‰ Οƒ : Type} β†’ {m : Type β†’ Type} β†’ [inst : Monad m] β†’ [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: Simp.Result β†’ Expr
expr
open Elab.Tactic Parser.Tactic /-- Use `ring_nf` to rewrite the main goal. -/ def
ringNFTarget: IO.Ref AtomM.State β†’ Config β†’ TacticM Unit
ringNFTarget
(s :
IO.Ref: Type β†’ Type
IO.Ref
AtomM.State: Type
AtomM.State
) (
cfg: Config
cfg
:
Config: Type
Config
) :
TacticM: Type β†’ Type
TacticM
Unit: Type
Unit
:=
withMainContext: {Ξ± : Type} β†’ TacticM Ξ± β†’ TacticM Ξ±
withMainContext
do let
goal: ?m.89443
goal
←
getMainGoal: TacticM MVarId
getMainGoal
let
tgt: ?m.89801
tgt
←
instantiateMVars: {m : Type β†’ Type} β†’ [inst : Monad m] β†’ [inst : MonadMCtx m] β†’ Expr β†’ m Expr
instantiateMVars
(← goal.getType): ?m.89672
(←
goal: ?m.89443
goal
(← goal.getType): ?m.89672
.
getType: MVarId β†’ MetaM Expr
getType
(← goal.getType): ?m.89672
)
let
r: ?m.89891
r
←
M.run: {Ξ± : Type} β†’ IO.Ref AtomM.State β†’ Config β†’ M Ξ± β†’ MetaM Ξ±
M.run
s
cfg: Config
cfg
<|
rewrite: Expr β†’ optParam Bool true β†’ M Simp.Result
rewrite
tgt: ?m.89801
tgt
if
r: ?m.89891
r
.
expr: Simp.Result β†’ Expr
expr
.
isConstOf: Expr β†’ Name β†’ Bool
isConstOf
``
True: Prop
True
then
goal: ?m.89443
goal
.
assign: {m : Type β†’ Type} β†’ [inst : MonadMCtx m] β†’ MVarId β†’ Expr β†’ m Unit
assign
(← mkOfEqTrue (← r.getProof)): ?m.90105
(←
mkOfEqTrue: Expr β†’ MetaM Expr
mkOfEqTrue
(← mkOfEqTrue (← r.getProof)): ?m.90105
(← r.getProof): ?m.90045
(←
r: ?m.89891
r
(← r.getProof): ?m.90045
.
getProof: Simp.Result β†’ MetaM Expr
getProof
(← r.getProof): ?m.90045
)
(← mkOfEqTrue (← r.getProof)): ?m.90105
)
replaceMainGoal: List MVarId β†’ TacticM Unit
replaceMainGoal
[]: List ?m.90178
[]
else
replaceMainGoal: List MVarId β†’ TacticM Unit
replaceMainGoal
[← applySimpResultToTarget goal tgt r]: List ?m.90306
[←
applySimpResultToTarget: MVarId β†’ Expr β†’ Simp.Result β†’ MetaM 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: IO.Ref AtomM.State β†’ Config β†’ FVarId β†’ TacticM Unit
ringNFLocalDecl
(s :
IO.Ref: Type β†’ Type
IO.Ref
AtomM.State: Type
AtomM.State
) (
cfg: Config
cfg
:
Config: Type
Config
) (
fvarId: FVarId
fvarId
:
FVarId: Type
FVarId
) :
TacticM: Type β†’ Type
TacticM
Unit: Type
Unit
:=
withMainContext: {Ξ± : Type} β†’ TacticM Ξ± β†’ TacticM Ξ±
withMainContext
do let
tgt: ?m.92443
tgt
←
instantiateMVars: {m : Type β†’ Type} β†’ [inst : Monad m] β†’ [inst : MonadMCtx m] β†’ Expr β†’ m Expr
instantiateMVars
(← fvarId.getType): ?m.92314
(←
fvarId: FVarId
fvarId
(← fvarId.getType): ?m.92314
.
getType: FVarId β†’ MetaM Expr
getType
(← fvarId.getType): ?m.92314
)
let
goal: ?m.92497
goal
←
getMainGoal: TacticM MVarId
getMainGoal
let
myres: ?m.92587
myres
←
M.run: {Ξ± : Type} β†’ IO.Ref AtomM.State β†’ Config β†’ M Ξ± β†’ MetaM Ξ±
M.run
s
cfg: Config
cfg
<|
rewrite: Expr β†’ optParam Bool true β†’ M Simp.Result
rewrite
tgt: ?m.92443
tgt
match ←
applySimpResultToLocalDecl: MVarId β†’ FVarId β†’ Simp.Result β†’ Bool β†’ MetaM (Option (FVarId Γ— MVarId))
applySimpResultToLocalDecl
goal: ?m.92497
goal
fvarId: FVarId
fvarId
myres: ?m.92587
myres
false: Bool
false
with |
none: {Ξ± : Type ?u.92668} β†’ Option Ξ±
none
=>
replaceMainGoal: List MVarId β†’ TacticM Unit
replaceMainGoal
[]: List ?m.92687
[]
|
some: {Ξ± : Type ?u.92698} β†’ Ξ± β†’ Option Ξ±
some
(_,
newGoal: MVarId
newGoal
) =>
replaceMainGoal: List MVarId β†’ TacticM Unit
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: Syntax β†’ Elab.TermElabM Config
elabConfig
cfg: ?m.94466
cfg
if
tk: ?m.94473
tk
.
isSome: {Ξ± : Type ?u.94790} β†’ Option Ξ± β†’ 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} β†’ (Ξ± β†’ Ξ²) β†’ Option Ξ± β†’ Option Ξ²
map
expandLocation: Syntax β†’ Location
expandLocation
).
getD: {Ξ± : Type ?u.95269} β†’ Option Ξ± β†’ Ξ± β†’ Ξ±
getD
(
.targets: Array Syntax β†’ Bool β†’ Location
.targets
#[]: Array ?m.95275
#[]
true: Bool
true
) let
s: ?m.95678
s
←
IO.mkRef: {Ξ± : Type} β†’ Ξ± β†’ BaseIO (IO.Ref Ξ±)
IO.mkRef
{}
withLocation: Location β†’ (FVarId β†’ TacticM Unit) β†’ TacticM Unit β†’ (MVarId β†’ TacticM Unit) β†’ TacticM Unit
withLocation
loc: ?m.95136
loc
(
ringNFLocalDecl: IO.Ref AtomM.State β†’ Config β†’ FVarId β†’ TacticM Unit
ringNFLocalDecl
s: ?m.95678
s
cfg: Config
cfg
) (
ringNFTarget: IO.Ref AtomM.State β†’ Config β†’ TacticM Unit
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: Syntax β†’ Elab.TermElabM Config
elabConfig
cfg: ?m.102190
cfg
if
tk: ?m.102199
tk
.
isSome: {Ξ± : Type ?u.102517} β†’ Option Ξ± β†’ Bool
isSome
then
cfg: ?m.102595
cfg
:= {
cfg: ?m.102502
cfg
with red := .default } let
s: ?m.103260
s
←
IO.mkRef: {Ξ± : Type} β†’ Ξ± β†’ BaseIO (IO.Ref Ξ±)
IO.mkRef
{}
liftMetaMAtMain: {Ξ± : Type} β†’ (MVarId β†’ MetaM Ξ±) β†’ TacticM Ξ±
liftMetaMAtMain
fun
g: ?m.103273
g
↦
M.run: {Ξ± : Type} β†’ IO.Ref AtomM.State β†’ Config β†’ M Ξ± β†’ MetaM Ξ±
M.run
s: ?m.103260
s
cfg: Config
cfg
<|
proveEq: MVarId β†’ AtomM Unit
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} β†’ TacticM Ξ± β†’ TacticM Ξ±
withMainContext
do let mut
cfg: ?m.109011
cfg
←
elabConfig: Syntax β†’ Elab.TermElabM Config
elabConfig
stx: ?m.108291
stx
[
2: ?m.108845
2
] if
tk: ?m.108333 x✝
tk
.
isSome: {Ξ± : Type ?u.109026} β†’ Option Ξ± β†’ Bool
isSome
then
cfg: ?m.109096
cfg
:= {
cfg: ?m.109011
cfg
with red := .default } let
s: ?m.109759
s
←
IO.mkRef: {Ξ± : Type} β†’ Ξ± β†’ BaseIO (IO.Ref Ξ±)
IO.mkRef
{}
Conv.applySimpResult: Simp.Result β†’ TacticM Unit
Conv.applySimpResult
(← M.run s cfg <| rewrite (← instantiateMVars (← Conv.getLhs))): ?m.110166
(←
M.run: {Ξ± : Type} β†’ IO.Ref AtomM.State β†’ Config β†’ M Ξ± β†’ MetaM Ξ±
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: Expr β†’ optParam Bool true β†’ M Simp.Result
rewrite
(← M.run s cfg <| rewrite (← instantiateMVars (← Conv.getLhs))): ?m.110166
(← instantiateMVars (← Conv.getLhs)): ?m.109942
(←
instantiateMVars: {m : Type β†’ Type} β†’ [inst : Monad m] β†’ [inst : MonadMCtx m] β†’ Expr β†’ m Expr
instantiateMVars
(← instantiateMVars (← Conv.getLhs)): ?m.109942
(← Conv.getLhs): ?m.109813
(←
Conv.getLhs: TacticM Expr
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 : MonadExceptOf Exception m] β†’ 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!")