- non_assoc : Π (elab : bool := bool.tt), expr elab → list (expr elab) → list (expr elab) → tactic.interactive.mono_function elab
- assoc : Π (elab : bool := bool.tt), expr elab → option (expr elab) → option (expr elab) → tactic.interactive.mono_function elab
- assoc_comm : Π (elab : bool := bool.tt), expr elab → expr elab → tactic.interactive.mono_function elab
- to_rel : rel
- function : tactic.interactive.mono_function
- left : expr
- right : expr
- rel_def : expr
(prefix,left,right,suffix) ← match_assoc unif l r finds the
longest prefix and suffix common to l and r and
returns them along with the differences
- assoc : expr × expr → expr × expr → tactic.interactive.mono_law
- congr : expr → tactic.interactive.mono_law
- other : expr → tactic.interactive.mono_law
Equations
- tactic.interactive.apply_rel R x' y' h hx hy = _.mpr (_.mpr h)
Equations
- tactic.interactive.list.minimum_on f (x :: xs) = (list.foldl (λ (_x : β × list α), tactic.interactive.list.minimum_on._match_1 f _x) (f x, [x]) xs).snd
- tactic.interactive.list.minimum_on f list.nil = list.nil
- tactic.interactive.list.minimum_on._match_1 f (k, a) = λ (b : α), let k' : β := f b in ite (k < k') (k, a) (ite (k' < k) (k', [b]) (k, b :: a))
monoapplies a monotonicity rule.mono*applies monotonicity rules repetitively.mono with x ≤ yormono with [0 ≤ x,0 ≤ y]creates an assertion for the listed propositions. Those help to select the right monotonicity rule.mono leftormono rightis useful when proving strict orderings: forx + y < w + zcould be broken down into either- left:
x ≤ wandy < zor - right:
x < wandy ≤ z
- left:
mono using [rule1,rule2]callssimp [rule1,rule2]before applying mono.- The general syntax is `mono '*'? ('with' hyp | 'with' [hyp1,hyp2])? ('using' [hyp1,hyp2])? mono_cfg?
To use it, first import tactic.monotonicity.
Here is an example of mono:
example (x y z k : ℤ)
(h : 3 ≤ (4 : ℤ))
(h' : z ≤ y) :
(k + 3 + x) - y ≤ (k + 4 + x) - z :=
begin
mono, -- unfold `(-)`, apply add_le_add
{ -- ⊢ k + 3 + x ≤ k + 4 + x
mono, -- apply add_le_add, refl
-- ⊢ k + 3 ≤ k + 4
mono },
{ -- ⊢ -y ≤ -z
mono /- apply neg_le_neg -/ }
end
More succinctly, we can prove the same goal as:
example (x y z k : ℤ)
(h : 3 ≤ (4 : ℤ))
(h' : z ≤ y) :
(k + 3 + x) - y ≤ (k + 4 + x) - z :=
by mono*
transforms a goal of the form f x ≼ f y into x ≤ y using lemmas
marked as monotonic.
Special care is taken when f is the repeated application of an
associative operator and if the operator is commutative
- one : tactic.interactive.rep_arity
- exactly : ℕ → tactic.interactive.rep_arity
- many : tactic.interactive.rep_arity
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
times.
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 (x y z k m n : ℕ)
(h₀ : z ≥ 0)
(h₁ : x ≤ y) :
(m + x + n) * z + k ≤ z * (y + n + m) + k :=
begin
ac_mono,
-- ⊢ (m + x + n) * z ≤ z * (y + n + m)
ac_mono,
-- ⊢ m + x + n ≤ y + n + m
ac_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
following example:
example (x y z k m n : ℕ)
(h₀ : z ≥ 0)
(h₁ : m + x + n ≤ y + n + m) :
(m + x + n) * z + k ≤ z * (y + n + m) + k :=
by ac_mono* h₁.
By giving ac_mono the assumption h₁, we are asking ac_refl to
stop earlier than it would normally would.