Lean4
/-- Given a proof `pf`, attempts to parse it as an upper (`lb = false`) or lower (`lb = true`)
bound on `n`. If successful, it returns `(bound, n, pf')` where `n` is a numeral and
`pf'` proves `n ≤ e` or `n ≱ e` (as described by `bound`).
-/
def getBound (m : Methods) (e : Expr) (pf : Expr) (lb : Bool) : MetaM (Bound × Expr × Expr) := do
let (e', c) ←
match ← parseBound (← inferType pf), lb with
| (b, a, false, false), false =>
let (z, a', eq) ← m.eval a;
pure (b, .le z, a', ← mkAppM ``of_not_lt_left #[pf, eq])
| (b, a, false, false), true =>
let (z, b', eq) ← m.eval b;
pure (a, .le z, b', ← mkAppM ``of_not_lt_right #[pf, eq])
| (a, b, false, true), false =>
let (z, b', eq) ← m.eval b;
pure (a, .le z, b', ← mkAppM ``of_le_right #[pf, eq])
| (a, b, false, true), true =>
let (z, a', eq) ← m.eval a;
pure (b, .le z, a', ← mkAppM ``of_le_left #[pf, eq])
| (b, a, true, false), false =>
let (z, a', eq) ← m.eval a;
pure (b, .lt z, a', ← mkAppM ``of_not_le_left #[pf, eq])
| (b, a, true, false), true =>
let (z, b', eq) ← m.eval b;
pure (a, .lt z, b', ← mkAppM ``of_not_le_right #[pf, eq])
| (a, b, true, true), false =>
let (z, b', eq) ← m.eval b;
pure (a, .lt z, b', ← mkAppM ``of_lt_right #[pf, eq])
| (a, b, true, true), true =>
let (z, a', eq) ← m.eval a;
pure (b, .lt z, a', ← mkAppM ``of_lt_left #[pf, eq])
let .true ← withNewMCtxDepth <| withReducible <| isDefEq e e' |
failure
pure c
