The @[push] attribute for the push, push_neg 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

instance Mathlib.Tactic.Push.instInhabitedHead : Inhabited Head

Equations

• Mathlib.Tactic.Push.instInhabitedHead = { default := Mathlib.Tactic.Push.instInhabitedHead.default }

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

Equations

• Mathlib.Tactic.Push.instInhabitedHead.default = Mathlib.Tactic.Push.Head.const default

instance Mathlib.Tactic.Push.instBEqHead : BEq Head

Equations

• Mathlib.Tactic.Push.instBEqHead = { beq := Mathlib.Tactic.Push.instBEqHead.beq }

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

Equations

• Mathlib.Tactic.Push.instBEqHead.beq (Mathlib.Tactic.Push.Head.const a) (Mathlib.Tactic.Push.Head.const b) = (a == b)
• Mathlib.Tactic.Push.instBEqHead.beq Mathlib.Tactic.Push.Head.lambda Mathlib.Tactic.Push.Head.lambda = true
• Mathlib.Tactic.Push.instBEqHead.beq Mathlib.Tactic.Push.Head.forall Mathlib.Tactic.Push.Head.forall = true
• Mathlib.Tactic.Push.instBEqHead.beq x✝¹ x✝ = false

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

Converts a Head to a string.

Equations

• (Mathlib.Tactic.Push.Head.const c).toString = c.toString
• Mathlib.Tactic.Push.Head.lambda.toString = "fun"
• Mathlib.Tactic.Push.Head.forall.toString = "Forall"

instance Mathlib.Tactic.Push.instToStringHead : ToString Head

Equations

• Mathlib.Tactic.Push.instToStringHead = { toString := Mathlib.Tactic.Push.Head.toString }

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

Returns the head of an expression.

Equations

• Mathlib.Tactic.Push.Head.ofExpr? (f.app arg) = Option.map Mathlib.Tactic.Push.Head.const f.getAppFn.constName?
• Mathlib.Tactic.Push.Head.ofExpr? (Lean.Expr.lam binderName binderType body binderInfo) = some Mathlib.Tactic.Push.Head.lambda
• Mathlib.Tactic.Push.Head.ofExpr? (Lean.Expr.forallE binderName binderType body binderInfo) = some Mathlib.Tactic.Push.Head.forall
• Mathlib.Tactic.Push.Head.ofExpr? x✝ = none

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.

Equations

• One or more equations did not get rendered due to their size.

def Mathlib.Tactic.Push.isPullThm.containsHead (e : Lean.Expr) : Head → Bool

Checks if the expression has the head in any subexpression. We don't need to check this for .lambda, because the term being a function is sufficient for pull fun _ ↦ _ to be applicable.

Equations

• One or more equations did not get rendered due to their size.
• Mathlib.Tactic.Push.isPullThm.containsHead e (Mathlib.Tactic.Push.Head.const c) = e.containsConst fun (x : Lean.Name) => x == c
• Mathlib.Tactic.Push.isPullThm.containsHead e Mathlib.Tactic.Push.Head.lambda = true

@[reducible, inline]

abbrev Mathlib.Tactic.Push.PullTheorem : Type

A theorem for the pull tactic

Equations

• Mathlib.Tactic.Push.PullTheorem = (Lean.Meta.SimpTheorem × Mathlib.Tactic.Push.Head)

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 ←].

Equations

• One or more equations did not get rendered due to their size.