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
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 gs tactic.new_goals.all = list.map prod.snd gs
- tactic.reorder_goals gs tactic.new_goals.non_dep_only = list.map prod.snd (list.filter (coe ∘ bnot ∘ prod.fst) gs)
- tactic.reorder_goals gs tactic.new_goals.non_dep_first = tactic.reorder_goals._match_1 (list.partition (coe ∘ prod.fst) gs)
- tactic.reorder_goals._match_1 (dep, non_dep) = list.map prod.snd non_dep ++ list.map prod.snd dep
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.
Similar to reflexivity with the difference that apply' is used instead of apply
Similar to symmetry with the difference that apply' is used instead of apply
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.
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.