mathlib3 documentation

tactic.apply

This file provides an alternative implementation for apply to fix the so-called "apply bug".

The issue arises when the goals is a Π-type -- whether it is visible or hidden behind a definition.

For instance, consider the following proof:

example {α β} (x y z : α → β) (h₀ : x ≤ y) (h₁ : y ≤ z) : x ≤ z :=
begin
  apply le_trans,
end

Because x ≤ z is definitionally equal to ∀ i, x i ≤ z i, apply will fail. The alternative definition, apply' fixes this. When apply would work, apply is used and otherwise, a different strategy is deployed

source
def tactic.reorder_goals {α : Type u_1} (gs : list (bool × α)) :
tactic.new_goals → list α

With gs a list of proof goals, reorder_goals gs new_g will use the new_goals policy new_g to rearrange the dependent goals to either drop them, push them to the end of the list or leave them in place. The bool values in gs indicates whether the goal is dependent or not.

Equations
source
meta def tactic.apply' (e : expr) (cfg : tactic.apply_cfg := {md := tactic.transparency.semireducible, approx := bool.tt, new_goals := tactic.new_goals.non_dep_first, instances := bool.tt, auto_param := bool.tt, opt_param := bool.tt, unify := bool.tt}) :
tactic (list (name × expr))

apply' mimics the behavior of apply_core. When apply_core fails, it is retried by providing the term with meta variables as additional arguments. The meta variables can then become new goals depending on the cfg.new_goals policy.

apply' also finds instances and applies opt_params and auto_params.

source
meta def tactic.fapply' (e : expr) :
tactic (list (name × expr))

Same as apply' but all arguments that weren't inferred are added to goal list.

source
meta def tactic.eapply' (e : expr) :
tactic (list (name × expr))

Same as apply' but only goals that don't depend on other goals are added to goal list.

source
meta def tactic.reflexivity' (md : tactic.transparency := tactic.transparency.semireducible) :
tactic unit

Similar to reflexivity with the difference that apply' is used instead of apply

source
meta def tactic.symmetry' (md : tactic.transparency := tactic.transparency.semireducible) :
tactic unit

Similar to symmetry with the difference that apply' is used instead of apply

source
meta def tactic.transitivity' (md : tactic.transparency := tactic.transparency.semireducible) :
tactic unit

Similar to transitivity with the difference that apply' is used instead of apply

source
meta def tactic.interactive.apply' (q : interactive.parse interactive.types.texpr) :
tactic unit

Similarly to apply, the apply' tactic tries to match the current goal against the conclusion of the type of term.

It differs from apply in that it does not unfold definition in order to find out what the assumptions of the provided term is. It is especially useful when defining relations on function spaces (e.g. ≤) so that rules like transitivity on le : (α → β) → (α → β) → (α → β) will be considered to have three parameters and two assumptions (i.e. f g h : α → β, H₀ : f ≤ g, H₁ : g ≤ h) instead of three parameters, two assumptions and then one more parameter (i.e. f g h : α → β, H₀ : f ≤ g, H₁ : g ≤ h, x : α). Whereas apply would expect the goal f x ≤ h x, apply' will work with the goal f ≤ h.

source
meta def tactic.interactive.fapply' (q : interactive.parse interactive.types.texpr) :
tactic unit

Similar to the apply' tactic, but does not reorder goals.

source
meta def tactic.interactive.eapply' (q : interactive.parse interactive.types.texpr) :
tactic unit

Similar to the apply' tactic, but only creates subgoals for non-dependent premises that have not been fixed by type inference or type class resolution.

source
meta def tactic.interactive.apply_with' (q : interactive.parse (lean.parser.pexpr std.prec.max)) (cfg : tactic.apply_cfg) :
tactic unit

Similar to the apply' tactic, but allows the user to provide a apply_cfg configuration object.

source
meta def tactic.interactive.mapply' (q : interactive.parse interactive.types.texpr) :
tactic unit

Similar to the apply' tactic, but uses matching instead of unification. mapply' t is equivalent to apply_with' t {unify := ff}

source
meta def tactic.interactive.reflexivity'  :
tactic unit

Similar to reflexivity with the difference that apply' is used instead of apply.

source
meta def tactic.interactive.refl'  :
tactic unit

Shorter name for the tactic reflexivity'.

source
meta def tactic.interactive.symmetry'  :
interactive.parse interactive.types.location → tactic unit

symmetry' behaves like symmetry but also offers the option symmetry' at h to apply symmetry to assumption h

source
meta def tactic.interactive.transitivity' (q : interactive.parse (optional interactive.types.texpr)) :
tactic unit

Similar to transitivity with the difference that apply' is used instead of apply.