# mathlibdocumentation

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

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

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
• = tactic.reorder_goals._match_1 gs)
• tactic.reorder_goals._match_1 (dep, non_dep) = non_dep ++ dep
meta def tactic.apply' (e : expr) (cfg : tactic.apply_cfg := ) :

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.

meta def tactic.fapply' (e : expr) :

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

meta def tactic.eapply' (e : expr) :

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

meta def tactic.reflexivity'  :

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

meta def tactic.symmetry'  :

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

meta def tactic.transitivity'  :

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

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.

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

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.

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

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

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

Shorter name for the tactic reflexivity'.

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

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