Lean4
/-- Discharge strategy for the `field_simp` tactic. -/
partial def discharge (prop : Expr) : SimpM (Option Expr) :=
withTraceNode `Tactic.field_simp (dischargerTraceMessage prop)
(do
-- Discharge strategy 1: Use assumptions
if let some r← Simp.dischargeUsingAssumption? prop then
return some r
let prop : Q(Prop) ←
(do
pure prop)
let pf? ←
match prop with
| ~q(($e : $α) ≠ $b) =>
try
let res ← Mathlib.Meta.NormNum.derive prop
match res with
| .isTrue pf =>
pure (some pf)
| _ =>
pure none
catch _ =>
pure none
| _ =>
pure none
if let some pf := pf? then
return some pf
let pf? ←
try
some <$> Mathlib.Meta.Positivity.solve prop
catch _ =>
pure none
if let some pf := pf? then
return some pf
Simp.withIncDischargeDepth
(do
let ctx ← readThe Simp.Context
let lems :=
[``two_ne_zero, ``three_ne_zero, ``four_ne_zero, ``mul_ne_zero, ``pow_ne_zero, ``zpow_ne_zero,
``Nat.cast_add_one_ne_zero]
let ctx' :=
ctx.setSimpTheorems <|
ctx.simpTheorems.push <| ← lems.foldlM (SimpTheorems.addConst · · (post := false)) { }
let stats : Simp.Stats :=
{ (← get) with }
-- Porting note: mathlib3's analogous field_simp discharger `field_simp.ne_zero`
-- does not explicitly call `simp` recursively like this. It's unclear to me
-- whether this is because
-- 1) Lean 3 simp dischargers automatically call `simp` recursively. (Do they?),
-- 2) mathlib3 norm_num1 is able to handle any needed discharging, or
-- 3) some other reason?
let ⟨simpResult, stats'⟩ ← simp prop ctx' #[(← Simp.getSimprocs)] discharge stats
set { (← get) with usedTheorems := stats'.usedTheorems, diag := stats'.diag }
if simpResult.expr.isConstOf ``True then
try
return some (← mkOfEqTrue (← simpResult.getProof))
catch _ =>
return none
else
return none))
