tactic.monotonicity.interactive

(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

source

meta def tactic.interactive.check_ac :

expr → tactic (bool × bool × option (expr × expr × expr) × expr)

source

meta def tactic.interactive.parse_assoc_chain' (f : expr) :

expr → tactic (dlist expr)

source

meta def tactic.interactive.parse_assoc_chain (f : expr) :

expr → tactic (list expr)

source

meta def tactic.interactive.fold_assoc (op : expr) :

option (expr × expr × expr) → list expr → option (expr × list expr)

source

meta def tactic.interactive.fold_assoc1 (op : expr) :

list expr → option expr

source

meta def tactic.interactive.same_function_aux :

list expr → list expr → expr → expr → tactic (expr × list expr × list expr)

source

meta def tactic.interactive.same_function :

expr → expr → tactic (expr × list expr × list expr)

source

meta def tactic.interactive.parse_ac_mono_function (opt : tactic.interactive.mono_cfg) (l r : expr) :

tactic (expr × expr × list expr × tactic.interactive.mono_function)

source

meta def tactic.interactive.parse_ac_mono_function' (opt : tactic.interactive.mono_cfg) (l r : pexpr) :

tactic (expr × expr × list expr × tactic.interactive.mono_function)

source

meta def tactic.interactive.ac_monotonicity_goal (opt : tactic.interactive.mono_cfg) :

expr → tactic (expr × expr × list expr × tactic.interactive.ac_mono_ctx)

source

meta def tactic.interactive.bin_op_left (f : expr) :

option expr → expr → expr

source

meta def tactic.interactive.bin_op (f a b : expr) :

expr

source

meta def tactic.interactive.bin_op_right (f : expr) :

expr → option expr → expr

source

meta def tactic.interactive.mk_fun_app :

tactic.interactive.mono_function → expr → expr

source

meta inductive tactic.interactive.mono_law :

Type

assoc : expr × expr → expr × expr → tactic.interactive.mono_law
congr : expr → tactic.interactive.mono_law
other : expr → tactic.interactive.mono_law

source

meta def tactic.interactive.mono_law.to_tactic_format :

tactic.interactive.mono_law → tactic format

source

@[protected, instance]

meta def tactic.interactive.has_to_tactic_format_mono_law :

has_to_tactic_format tactic.interactive.mono_law

source

meta def tactic.interactive.mk_rel (ctx : tactic.interactive.ac_mono_ctx_ne) (f : expr → expr) :

expr

source

meta def tactic.interactive.mk_congr_args (fn : expr) (xs₀ xs₁ : list expr) (l r : expr) :

tactic expr

source

meta def tactic.interactive.mk_congr_law (ctx : tactic.interactive.ac_mono_ctx) :

tactic expr

source

meta def tactic.interactive.mk_pattern (ctx : tactic.interactive.ac_mono_ctx) :

tactic tactic.interactive.mono_law

source

meta def tactic.interactive.match_rule (asms : list expr) (pat : expr) (r : name) :

tactic expr

source

meta def tactic.interactive.find_lemma (asms : list expr) (pat : expr) :

list name → tactic (list expr)

source

meta def tactic.interactive.match_chaining_rules (asms : list expr) (ls : list name) (x₀ x₁ : expr) :

tactic (list expr)

source

meta def tactic.interactive.find_rule (asms : list expr) (ls : list name) :

tactic.interactive.mono_law → tactic (list expr)

source

def tactic.interactive.apply_rel {α : Sort u} (R : α → α → Sort v) {x y : α} (x' y' : α) (h : R x y) (hx : x = x') (hy : y = y') :

R x' y'

Equations

tactic.interactive.apply_rel R x' y' h hx hy = _.mpr (_.mpr h)

source

meta def tactic.interactive.ac_refine (e : expr) :

tactic unit

source

meta def tactic.interactive.one_line (e : expr) :

tactic format

source

meta def tactic.interactive.side_conditions (e : expr) :

tactic format

source

meta def tactic.interactive.hide_meta_vars' (tac : tactic.interactive.itactic) :

tactic.interactive.itactic

source

meta def tactic.interactive.solve_mvar (v : expr) (tac : tactic unit) :

tactic unit

source

def tactic.interactive.list.minimum_on {α : Type u_1} {β : Type u_2} [linear_order β] (f : α → β) :

list α → list α

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))

source

meta def tactic.interactive.best_match {β : Type} (xs : list expr) (tac : expr → tactic β) :

tactic unit

source

meta def tactic.interactive.mono_aux (dir : interactive.parse tactic.interactive.side) :

tactic unit

source

meta def tactic.interactive.mono (many : interactive.parse (lean.parser.tk "*")?) (dir : interactive.parse tactic.interactive.side) (hyps : interactive.parse (lean.parser.tk "with" *> interactive.types.pexpr_list_or_texpr <|> pure list.nil)) (simp_rules : interactive.parse (lean.parser.tk "using" *> tactic.simp_arg_list <|> pure list.nil)) :

tactic unit

mono applies a monotonicity rule.
mono* applies monotonicity rules repetitively.
mono with x ≤ y or mono with [0 ≤ x,0 ≤ y] creates an assertion for the listed propositions. Those help to select the right monotonicity rule.
mono left or mono right is useful when proving strict orderings: for x + y < w + z could be broken down into either
- left: x ≤ w and y < z or
- right: x < w and y ≤ z
mono using [rule1,rule2] calls simp [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*

source

meta def tactic.interactive.ac_mono_aux (cfg : tactic.interactive.mono_cfg := {unify := ff}) :

tactic unit

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

source

meta def tactic.interactive.repeat_until_or_at_most :

ℕ → tactic unit → tactic unit → tactic unit

(repeat_until_or_at_most n t u): repeat tactic t at most n times or until u succeeds

source

meta def tactic.interactive.repeat_until :

tactic unit → tactic unit → tactic unit

source

@[protected, instance]

def tactic.interactive.rep_arity.inhabited :

inhabited tactic.interactive.rep_arity

source

inductive tactic.interactive.rep_arity :

Type

one : tactic.interactive.rep_arity
exactly : ℕ → tactic.interactive.rep_arity
many : tactic.interactive.rep_arity

source

@[protected, instance]

meta def tactic.interactive.rep_arity.has_reflect :

has_reflect tactic.interactive.rep_arity

source

meta def tactic.interactive.repeat_or_not :

tactic.interactive.rep_arity → tactic unit → option (tactic unit) → tactic unit

source

meta def tactic.interactive.assert_or_rule :

lean.parser (pexpr ⊕ pexpr)

source

meta def tactic.interactive.arity :

lean.parser tactic.interactive.rep_arity

source

meta def tactic.interactive.ac_mono (rep : interactive.parse tactic.interactive.arity) :

interactive.parse tactic.interactive.assert_or_rule ? → (tactic.interactive.mono_cfg := {unify := ff}) → tactic unit

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.