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 is negative, returns a proof of `False`.
-/
def inconsistentBounds (m : Methods) (z1 z2 : Bound) (e1 e2 p1 p2 e : Expr) : MetaM Expr := do
match z1, z2 with
| .le lo, .lt hi =>
if lo == hi then
return p2.app p1
return p2.app (← mkAppM ``le_trans #[← m.proveLE e2 e1, p1])
| .lt lo, .le hi =>
if lo == hi then
return p1.app p2
return p1.app (← mkAppM ``le_trans #[p2, ← m.proveLE e2 e1])
| .le _, .le _ =>
return (← m.proveLT e2 e1).app (← mkAppM ``le_trans #[p1, p2])
| .lt lo, .lt hi =>
if hi ≤ lo then
return p1.app (← mkAppM ``le_of_not_le_of_le #[p2, ← m.proveLE e2 e1])
let e3 ← m.mkNumeral (hi - 1)
let p3 ← m.roundDown e e2 e3 p2
return p1.app (← mkAppM ``le_trans #[p3, ← m.proveLE e3 e1])
