core / init.meta.injection_tactic

source

meta def tactic.injection_with (h : expr) (ns : list name) (base : name := name.mk_string "h" name.anonymous) (offset : option ℕ := some 1) :

tactic (list expr × list name)

source

meta def tactic.injection (h : expr) (base : name := name.mk_string "h" name.anonymous) (offset : option ℕ := some 1) :

tactic (list expr)

Simplify the equation h using injectivity of constructors. See injection_with. Returns the hypotheses that were added to the context, or an empty list if the goal was solved by contradiction.

source

meta def tactic.injections_with (ns : list name) (base : name := name.mk_string "h" name.anonymous) (offset : option ℕ := some 1) :

tactic unit

Simplifies equations in the context using injectivity of constructors. For each equation h : C x₁ ... xₙ = D y₁ ... yₘ in the context, where C and D are constructors of the same data type, injections_with does the following:

If C = D, it adds equations x₁ = y₁, ..., xₙ = yₙ.
If C ≠ D, it solves the goal by contradiction.

See injection_with for details, including information about base and offset.

injections_with also recurses into the new equations xᵢ = yᵢ. If it has to recurse more than five times, it fails.