The push and pull tactics

The push tactic pushes a given constant inside expressions: it can be applied to goals as well as local hypotheses and also works as a conv tactic.

The pull tactic does the reverse: it pulls the given constant towards the head of the expression.

theorem Mathlib.Tactic.Push.not_iff (p q : Prop) : ¬(p ↔ q) ↔ p ∧ ¬q ∨ ¬p ∧ q

theorem Mathlib.Tactic.Push.not_exists {α : Sort u_1} (s : α → Prop) : ¬Exists s ↔ ∀ (x : α), binderNameHint x s ¬s x

theorem Mathlib.Tactic.Push.not_and_eq (p q : Prop) : (¬(p ∧ q)) = (p → ¬q)

theorem Mathlib.Tactic.Push.not_and_or_eq (p q : Prop) : (¬(p ∧ q)) = (¬p ∨ ¬q)

theorem Mathlib.Tactic.Push.not_forall_eq {α : Sort u_1} (s : α → Prop) : (¬∀ (x : α), s x) = ∃ (x : α), ¬s x

opaque Mathlib.Tactic.Push.push_neg.use_distrib : Lean.Option Bool

Set distrib to true in push Not and related tactics.

structure Mathlib.Tactic.Push.Config : Type

The configuration options for the push tactic.

• distrib : Bool

  If true (default false), rewrite ¬ (p ∧ q) into ¬ p ∨ ¬ q instead of p → ¬ q.

def Mathlib.Tactic.Push.elabPushConfig : Lean.Syntax → Lean.Elab.Tactic.TacticM Config

Function elaborating Push.Config.

def Mathlib.Tactic.Push.pushSimpConfig : Lean.Meta.Simp.Config

The simp configuration used in push.

def Mathlib.Tactic.Push.pushStep (head : Head) (cfg : Config) : Lean.Meta.Simp.Simproc

Try to rewrite using a push lemma.

def Mathlib.Tactic.Push.pushCore (head : Head) (cfg : Config) (disch? : Option Lean.Meta.Simp.Discharge) (tgt : Lean.Expr) : Lean.MetaM Lean.Meta.Simp.Result

Common entry point to the implementation of push.

def Mathlib.Tactic.Push.pullStep (head : Head) : Lean.Meta.Simp.Simproc

Try to rewrite using a pull lemma.

def Mathlib.Tactic.Push.pullCore (head : Head) (tgt : Lean.Expr) (disch? : Option Lean.Meta.Simp.Discharge) : Lean.MetaM Lean.Meta.Simp.Result

Common entry point to the implementation of pull.

def Mathlib.Tactic.Push.isUnderscore : Lean.Term → Bool

Return true if stx is an underscore, i.e. _ or fun $_ => _/fun $_ ↦ _.

def Mathlib.Tactic.Push.resolvePushId? (stx : Lean.Term) : Lean.Elab.TermElabM (Option Lean.Expr)

resolvePushId? is a version of resolveId? that also supports notations like _ ∈ _, ∃ x, _ and ∑ x, _.

def Mathlib.Tactic.Push.elabHead (stx : Lean.Term) : Lean.Elab.TermElabM Head

Elaborator for the argument passed to push. It accepts a constant, or a function

def Mathlib.Tactic.Push.elabDischarger (stx : Lean.TSyntax `Lean.Parser.Tactic.discharger) : Lean.Elab.Tactic.TacticM Lean.Meta.Simp.Discharge

Elaborate the (disch := ...) syntax for a simp-like tactic.

def Mathlib.Tactic.Push.push (cfg : Config) (disch? : Option Lean.Meta.Simp.Discharge) (head : Head) (loc : Lean.Elab.Tactic.Location) (failIfUnchanged : Bool := true) : Lean.Elab.Tactic.TacticM Unit

Run the push tactic.

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

push c rewrites the goal by pushing the constant c deeper into an expression. For instance, push _ ∈ _ rewrites x ∈ {y} ∪ zᶜ into x = y ∨ ¬ x ∈ z. More precisely, the push tactic repeatedly rewrites an expression by applying lemmas of the form c ... = ... (c ...) (where c can appear 0 or more times on the right hand side). To extend the push tactic, you can tag a lemma of this form with the @[push] attribute.

To instead move a constant closer to the head of the expression, use the pull tactic.

push works as both a tactic and a conv tactic.

• push _ ~ _ pushes the (binary) operator ~, push ~ _ pushes the (unary) operator ~.
• push c at l1 l2 ... rewrites at the given locations.
• push c at * rewrites at all hypotheses and the goal.
• push +distrib Not rewrites ¬ (p ∧ q) into ¬ p ∨ ¬ q (without +distrib, it rewrites it into p → ¬ q instead).
• push (disch := tac) c uses the tactic tac to discharge any hypotheses for @[push] lemmas.

Examples:

• push Not is the same as push ¬ _, and it rewrites ¬ ∀ ε > 0, ∃ δ > 0, δ < ε into ∃ ε > 0, ∀ δ > 0, ε ≤ δ. Notably, this preserves the binder names.
• push _ ∈ _ rewrites x ∈ {y} ∪ zᶜ into x = y ∨ ¬ x ∈ z.
• push (disch := positivity) Real.log rewrites log (a * b ^ 2) into log a + 2 * log b.
• push fun _ ↦ _ rewrites fun x => f x ^ 2 + 5 into f ^ 2 + 5
• push ∀ _, _ rewrites ∀ a, p a ∧ q a into (∀ a, p a) ∧ (∀ a, q a).

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

push_neg rewrites the goal by pushing negations deeper into an expression. For instance, the goal ¬ ∀ x, ∃ y, x ≤ y will be transformed by push_neg into ∃ x, ∀ y, y < x. Binder names are preserved (contrary to what would happen with simp using the relevant lemmas). push_neg works as both a tactic and a conv tactic.

push_neg is a special case of the more general push tactic, namely push Not. The push tactic can be extended using the @[push] attribute. push has special-casing built in for push Not.

Tactics that introduce a negation usually have a version that automatically calls push_neg on that negation. These include by_cases!, contrapose! and by_contra!.

• push_neg at l1 l2 ... rewrites at the given locations.
• push_neg at * rewrites at each hypothesis and the goal.
• push_neg +distrib rewrites ¬ (p ∧ q) into ¬ p ∨ ¬ q (by default, the tactic rewrites it into p → ¬ q instead).

Example:

example (h : ¬ ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - y₀| ≤ ε) :
    ∃ ε > 0, ∀ δ > 0, ∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀| := by
  push_neg at h
  -- Now we have the hypothesis `h : ∃ ε > 0, ∀ δ > 0, ∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀|`
  exact h

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

pull c rewrites the goal by pulling the constant c closer to the head of the expression. For instance, pull _ ∈ _ rewrites x ∈ y ∨ ¬ x ∈ z into x ∈ y ∪ zᶜ. More precisely, the pull tactic repeatedly rewrites an expression by applying lemmas of the form ... (c ...) = c ... (where c can appear 1 or more times on the left hand side). pull is the inverse tactic to push. To extend the pull tactic, you can tag a lemma with the @[push] attribute. pull works as both a tactic and a conv tactic.

A lemma is considered a pull lemma if its reverse direction is a push lemma that actually moves the given constant away from the head. For example

• not_or : ¬ (p ∨ q) ↔ ¬ p ∧ ¬ q is a pull lemma, but not_not : ¬ ¬ p ↔ p is not.
• log_mul : log (x * y) = log x + log y is a pull lemma, but log_abs : log |x| = log x is not.
• Pi.mul_def : f * g = fun (i : ι) => f i * g i and Pi.one_def : 1 = fun (x : ι) => 1 are both pull lemmas for fun, because every push fun _ ↦ _ lemma is also considered a pull lemma.

TODO: define a @[pull] attribute for tagging pull lemmas that are not push lemmas.

• pull _ ~ _ pulls the operator or relation ~.
• pull c at l1 l2 ... rewrites at the given locations.
• pull c at * rewrites at all hypotheses and the goal.
• pull (disch := tac) c uses the tactic tac to discharge any hypotheses for @[push] lemmas.

Examples:

• pull _ ∈ _ rewrites x ∈ y ∨ ¬ x ∈ z into x ∈ y ∪ zᶜ.
• pull (disch := positivity) Real.log rewrites log a + 2 * log b into log (a * b ^ 2).
• pull fun _ ↦ _ rewrites f ^ 2 + 5 into fun x => f x ^ 2 + 5 where f is a function.

def pushFun : Lean.Meta.Simp.Simproc

A simproc variant of push fun _ ↦ _, to be used as simp [↓pushFun].

def pullFun : Lean.Meta.Simp.Simproc

A simproc variant of pull fun _ ↦ _, to be used as simp [pullFun].

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

push c rewrites the goal by pushing the constant c deeper into an expression. For instance, push _ ∈ _ rewrites x ∈ {y} ∪ zᶜ into x = y ∨ ¬ x ∈ z. More precisely, the push tactic repeatedly rewrites an expression by applying lemmas of the form c ... = ... (c ...) (where c can appear 0 or more times on the right hand side). To extend the push tactic, you can tag a lemma of this form with the @[push] attribute.

To instead move a constant closer to the head of the expression, use the pull tactic.

push works as both a tactic and a conv tactic.

• push _ ~ _ pushes the (binary) operator ~, push ~ _ pushes the (unary) operator ~.
• push c at l1 l2 ... rewrites at the given locations.
• push c at * rewrites at all hypotheses and the goal.
• push +distrib Not rewrites ¬ (p ∧ q) into ¬ p ∨ ¬ q (without +distrib, it rewrites it into p → ¬ q instead).
• push (disch := tac) c uses the tactic tac to discharge any hypotheses for @[push] lemmas.

Examples:

• push Not is the same as push ¬ _, and it rewrites ¬ ∀ ε > 0, ∃ δ > 0, δ < ε into ∃ ε > 0, ∀ δ > 0, ε ≤ δ. Notably, this preserves the binder names.
• push _ ∈ _ rewrites x ∈ {y} ∪ zᶜ into x = y ∨ ¬ x ∈ z.
• push (disch := positivity) Real.log rewrites log (a * b ^ 2) into log a + 2 * log b.
• push fun _ ↦ _ rewrites fun x => f x ^ 2 + 5 into f ^ 2 + 5
• push ∀ _, _ rewrites ∀ a, p a ∧ q a into (∀ a, p a) ∧ (∀ a, q a).

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

push_neg rewrites the goal by pushing negations deeper into an expression. For instance, the goal ¬ ∀ x, ∃ y, x ≤ y will be transformed by push_neg into ∃ x, ∀ y, y < x. Binder names are preserved (contrary to what would happen with simp using the relevant lemmas). push_neg works as both a tactic and a conv tactic.

push_neg is a special case of the more general push tactic, namely push Not. The push tactic can be extended using the @[push] attribute. push has special-casing built in for push Not.

Tactics that introduce a negation usually have a version that automatically calls push_neg on that negation. These include by_cases!, contrapose! and by_contra!.

• push_neg at l1 l2 ... rewrites at the given locations.
• push_neg at * rewrites at each hypothesis and the goal.
• push_neg +distrib rewrites ¬ (p ∧ q) into ¬ p ∨ ¬ q (by default, the tactic rewrites it into p → ¬ q instead).

Example:

example (h : ¬ ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - y₀| ≤ ε) :
    ∃ ε > 0, ∀ δ > 0, ∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀| := by
  push_neg at h
  -- Now we have the hypothesis `h : ∃ ε > 0, ∀ δ > 0, ∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀|`
  exact h

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

#push head e, where head is a constant and e is an expression, prints the push head form of e.

#push understands local variables, so you can use them to introduce parameters.

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

pull c rewrites the goal by pulling the constant c closer to the head of the expression. For instance, pull _ ∈ _ rewrites x ∈ y ∨ ¬ x ∈ z into x ∈ y ∪ zᶜ. More precisely, the pull tactic repeatedly rewrites an expression by applying lemmas of the form ... (c ...) = c ... (where c can appear 1 or more times on the left hand side). pull is the inverse tactic to push. To extend the pull tactic, you can tag a lemma with the @[push] attribute. pull works as both a tactic and a conv tactic.

A lemma is considered a pull lemma if its reverse direction is a push lemma that actually moves the given constant away from the head. For example

• not_or : ¬ (p ∨ q) ↔ ¬ p ∧ ¬ q is a pull lemma, but not_not : ¬ ¬ p ↔ p is not.
• log_mul : log (x * y) = log x + log y is a pull lemma, but log_abs : log |x| = log x is not.
• Pi.mul_def : f * g = fun (i : ι) => f i * g i and Pi.one_def : 1 = fun (x : ι) => 1 are both pull lemmas for fun, because every push fun _ ↦ _ lemma is also considered a pull lemma.

TODO: define a @[pull] attribute for tagging pull lemmas that are not push lemmas.

• pull _ ~ _ pulls the operator or relation ~.
• pull c at l1 l2 ... rewrites at the given locations.
• pull c at * rewrites at all hypotheses and the goal.
• pull (disch := tac) c uses the tactic tac to discharge any hypotheses for @[push] lemmas.

Examples:

• pull _ ∈ _ rewrites x ∈ y ∨ ¬ x ∈ z into x ∈ y ∪ zᶜ.
• pull (disch := positivity) Real.log rewrites log a + 2 * log b into log (a * b ^ 2).
• pull fun _ ↦ _ rewrites f ^ 2 + 5 into fun x => f x ^ 2 + 5 where f is a function.

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

The syntax is #pull head e, where head is a constant and e is an expression, which will print the pull head form of e.

#pull understands local variables, so you can use them to introduce parameters.

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

#push_discr_tree X shows the discrimination tree of all lemmas used by push X. This can be helpful when you are constructing a set of push lemmas for the constant X.

def Mathlib.Tactic.Push.elabPushTree : Lean.Elab.Command.CommandElab

#push_discr_tree X shows the discrimination tree of all lemmas used by push X. This can be helpful when you are constructing a set of push lemmas for the constant X.