Lean4
/-- Given `(z1, e1, p1)` a lower bound on `e` and `(z2, e2, p2)` an upper bound on `e`, such that the
distance between the bounds matches the number of `cases` in the subarray (which must be positive),
proves the goal `g` using the metavariables in the array by recursive bisection.
This is the core of the tactic, producing a case tree of if statements which bottoms out
at the `cases`.
-/
partial def bisect (m : Methods) (g : MVarId) (cases : Subarray IntervalCasesSubgoal) (z1 z2 : Bound)
(e1 e2 p1 p2 e : Expr) : MetaM Unit :=
g.withContext
(do
if 1 < cases.size then
let tgt ← g.getType
let mid := cases.size / 2
let z3 := z1.asLower + mid
let e3 ← m.mkNumeral z3
let le ← mkAppM ``LE.le #[e3, e]
let g₁ ← mkFreshExprMVar (← mkArrow (mkNot le) tgt) .syntheticOpaque
let g₂ ← mkFreshExprMVar (← mkArrow le tgt) .syntheticOpaque
g.assign <| ← mkAppM ``dite #[le, g₂, g₁]
let (x₁, g₁) ← g₁.mvarId!.intro1
m.bisect g₁ cases[:mid] z1 (.lt z3) e1 e3 p1 (.fvar x₁) e
let (x₂, g₂) ← g₂.mvarId!.intro1
m.bisect g₂ cases[mid:] (.le z3) z2 e3 e2 (.fvar x₂) p2 e
else if _x : 0 < cases.size then
let { goal, rhs, .. } := cases[0]
let pf₁ ←
match z1 with
| .le _ =>
pure p1
| .lt _ =>
m.roundUp e1 e rhs p1
let pf₂ ←
match z2 with
| .le _ =>
pure p2
| .lt _ =>
m.roundDown e e2 rhs p2
g.assign (.app (.mvar goal) (← mkAppM ``le_antisymm #[pf₂, pf₁]))
else
panic! "no goals")
