Lean4
/-- `bound` tactic for proving inequalities via straightforward recursion on expression structure.
An example use case is
```
-- Calc example: A weak lower bound for `z ↦ z^2 + c`
lemma le_sqr_add (c z : ℝ) (cz : ‖c‖ ≤ ‖z‖) (z3 : 3 ≤ ‖z‖) :
2 * ‖z‖ ≤ ‖z^2 + c‖ := by
calc ‖z^2 + c‖
_ ≥ ‖z^2‖ - ‖c‖ := by bound
_ ≥ ‖z^2‖ - ‖z‖ := by bound
_ ≥ (‖z‖ - 1) * ‖z‖ := by
rw [mul_comm, mul_sub_one, ← pow_two, ← norm_pow]
_ ≥ 2 * ‖z‖ := by bound
```
`bound` is built on top of `aesop`, and uses
1. Apply lemmas registered via the `@[bound]` attribute
2. Forward lemmas registered via the `@[bound_forward]` attribute
3. Local hypotheses from the context
4. Optionally: additional hypotheses provided as `bound [h₀, h₁]` or similar. These are added to the
context as if by `have := hᵢ`.
The functionality of `bound` overlaps with `positivity` and `gcongr`, but can jump back and forth
between `0 ≤ x` and `x ≤ y`-type inequalities. For example, `bound` proves
`0 ≤ c → b ≤ a → 0 ≤ a * c - b * c`
by turning the goal into `b * c ≤ a * c`, then using `mul_le_mul_of_nonneg_right`. `bound` also
contains lemmas for goals of the form `1 ≤ x, 1 < x, x ≤ 1, x < 1`. Conversely, `gcongr` can prove
inequalities for more types of relations, supports all `positivity` functionality, and is likely
faster since it is more specialized (not built atop `aesop`). -/
@[tactic_parser 1000]
public meta def «tacticBound[_]» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `«tacticBound[_]» 1022
(ParserDescr.binary✝ `andthen (ParserDescr.nonReservedSymbol✝ "bound " false✝)
(ParserDescr.unary✝ `optional
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " [")
((with_annotate_term"sepBy(" @ParserDescr.sepBy✝) (ParserDescr.cat✝ `term 0) "," (ParserDescr.symbol✝ ", ")
Bool.false✝))
(ParserDescr.symbol✝ "]"))))
