The @[push] attribute for the push and pull tactics

This file defines the @[push] attribute, so that it can be used without importing the tactic itself.

inductive Mathlib.Tactic.Push.Head : Type

The type for a constant to be pushed by push.

• const (c : Lean.Name) : Head
• lambda : Head
• forall : Head

@[implicit_reducible]

instance Mathlib.Tactic.Push.instInhabitedHead : Inhabited Head

def Mathlib.Tactic.Push.instInhabitedHead.default : Head

def Mathlib.Tactic.Push.instBEqHead.beq : Head → Head → Bool

@[implicit_reducible]

instance Mathlib.Tactic.Push.instBEqHead : BEq Head

def Mathlib.Tactic.Push.Head.toString : Head → String

Converts a Head to a string.

@[implicit_reducible]

instance Mathlib.Tactic.Push.instToStringHead : ToString Head

def Mathlib.Tactic.Push.Head.ofExpr? : Lean.Expr → Option Head

Returns the head of an expression.

opaque Mathlib.Tactic.Push.pushExt : Lean.SimpleScopedEnvExtension Lean.Meta.SimpTheorem (Lean.Meta.DiscrTree Lean.Meta.SimpTheorem)

The push environment extension

def Mathlib.Tactic.Push.isPullThm (declName : Lean.Name) (inv : Bool) : Lean.MetaM (Option Head)

Checks if the theorem is suitable for the pull tactic. That is, check if it is of the form x = f ... where x contains the head f, but f is not the head of x.

@[reducible, inline]

abbrev Mathlib.Tactic.Push.PullTheorem : Type

A theorem for the pull tactic

opaque Mathlib.Tactic.Push.pullExt : Lean.SimpleScopedEnvExtension PullTheorem (Lean.Meta.DiscrTree PullTheorem)

The pull environment extension

def Mathlib.Tactic.Push.pushAttr : Lean.ParserDescr

The push attribute is used to tag lemmas that "push" a constant into an expression.

For example:

@[push] theorem log_mul (hx : x ≠ 0) (hy : y ≠ 0) : log (x * y) = log x + log y
@[push] theorem log_abs : log |x| = log x

@[push] theorem not_imp (p q : Prop) : ¬(p → q) ↔ p ∧ ¬q
@[push] theorem not_iff (p q : Prop) : ¬(p ↔ q) ↔ (p ∧ ¬q) ∨ (¬p ∧ q)
@[push] theorem not_not (p : Prop) : ¬ ¬p ↔ p
@[push] theorem not_le : ¬a ≤ b ↔ b < a

Note that some push lemmas don't push the constant away from the head (log_abs) and some push lemmas cancel the constant out (not_not and not_le). For the other lemmas that are "genuine" push lemmas, a pull attribute is automatically added in the reverse direction. To not add a pull tag, use @[push only].

To tag the reverse direction of the lemma, use @[push ←].