ac_mono reduces the f x ⊑ f y, for some relation ⊑ and a
monotonic function f to x ≺ y.
ac_mono* unwraps monotonic functions until it can't.
ac_mono^k, for some literal number k applies monotonicity k
ac_mono := h, with h a hypothesis, unwraps monotonic functions and
uses h to solve the remaining goal. Can be combined with * or ^k:
ac_mono* := h
ac_mono : p asserts p and uses it to discharge the goal result
unwrapping a series of monotonic functions. Can be combined with * or
^k: ac_mono* : p
In the case where f is an associative or commutative operator,
ac_mono will consider any possible permutation of its arguments and
use the one the minimizes the difference between the left-hand side
and the right-hand side.
To use it, first import tactic.monotonicity.
ac_mono can be used as follows:
example(xyzkmn:ℕ)(h₀:z≥0)(h₁:x≤y):(m+x+n)*z+k≤z*(y+n+m)+k:=beginac_mono,-- ⊢ (m + x + n) * z ≤ z * (y + n + m)ac_mono,-- ⊢ m + x + n ≤ y + n + mac_mono,end
As with mono*, ac_mono* solves the goal in one go and so does
ac_mono* := h₁. The latter syntax becomes especially interesting in the