The push, push_neg 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. push_neg is a macro for push Not.

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) : (¬∃ (x : α), s x) ↔ ∀ (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

Make push_neg use not_and_or rather than the default not_and.

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

The simp configuration used in push.

Equations

• Mathlib.Tactic.Push.pushSimpConfig = { zeta := false, proj := false }

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

Try to rewrite using a push lemma.

Equations

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

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

Common entry point to the implementation of push.

Equations

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

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

Try to rewrite using a pull lemma.

Equations

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

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.

Equations

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

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

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

Equations

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

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, _.

Equations

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

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

Equations

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

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.

Equations

• Mathlib.Tactic.Push.elabDischarger stx = (fun (x : IO.Ref Lean.Elab.Term.State × Lean.Meta.Simp.Discharge) => x.snd) <$> Lean.Elab.Tactic.tacticToDischarge stx.raw[3]

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

push pushes the given constant away from the head of the expression. For example

• 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 ¬ _ is the same as push_neg or push Not, and it rewrites ¬ ∀ ε > 0, ∃ δ > 0, δ < ε into ∃ ε > 0, ∀ δ > 0, ε ≤ δ.

In addition to constants, push can be used to push fun and ∀ binders:

• 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).

The push tactic can be extended using the @[push] attribute.

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

To push a constant at a hypothesis, use the push ... at h or push ... at * syntax.

Equations

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

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

Push negations into the conclusion or a hypothesis. For instance, a hypothesis h : ¬ ∀ x, ∃ y, x ≤ y will be transformed by push_neg at h into h : ∃ x, ∀ y, y < x. Binder names are preserved.

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, so that it can preserve binder names, and so that ¬ (p ∧ q) can be transformed to either p → ¬ q (the default) or ¬ p ∨ ¬ q. To get ¬ p ∨ ¬ q, use set_option push_neg.use_distrib true.

Another example: given a hypothesis

h : ¬ ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - y₀| ≤ ε

writing push_neg at h will turn h into

h : ∃ ε > 0, ∀ δ > 0, ∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀|

Note that binder names are preserved by this tactic, contrary to what would happen with simp using the relevant lemmas. One can use this tactic at the goal using push_neg, at every hypothesis and the goal using push_neg at * or at selected hypotheses and the goal using say push_neg at h h' ⊢, as usual.

Equations

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

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

pull is the inverse tactic to push. It pulls the given constant towards the head of the expression. For example

• 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.

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.

Equations

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

def pushFun : Lean.Meta.Simp.Simproc

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

Equations

• pushFun = Mathlib.Tactic.Push.pushStep Mathlib.Tactic.Push.Head.lambda

def pullFun : Lean.Meta.Simp.Simproc

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

Equations

• pullFun = Mathlib.Tactic.Push.pullStep Mathlib.Tactic.Push.Head.lambda

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

push pushes the given constant away from the head of the expression. For example

• 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 ¬ _ is the same as push_neg or push Not, and it rewrites ¬ ∀ ε > 0, ∃ δ > 0, δ < ε into ∃ ε > 0, ∀ δ > 0, ε ≤ δ.

In addition to constants, push can be used to push fun and ∀ binders:

• 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).

The push tactic can be extended using the @[push] attribute.

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

To push a constant at a hypothesis, use the push ... at h or push ... at * syntax.

Equations

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

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

Push negations into the conclusion or a hypothesis. For instance, a hypothesis h : ¬ ∀ x, ∃ y, x ≤ y will be transformed by push_neg at h into h : ∃ x, ∀ y, y < x. Binder names are preserved.

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, so that it can preserve binder names, and so that ¬ (p ∧ q) can be transformed to either p → ¬ q (the default) or ¬ p ∨ ¬ q. To get ¬ p ∨ ¬ q, use set_option push_neg.use_distrib true.

Another example: given a hypothesis

h : ¬ ∀ ε > 0, ∃ δ > 0, ∀ x, |x - x₀| ≤ δ → |f x - y₀| ≤ ε

writing push_neg at h will turn h into

h : ∃ ε > 0, ∀ δ > 0, ∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀|

Note that binder names are preserved by this tactic, contrary to what would happen with simp using the relevant lemmas. One can use this tactic at the goal using push_neg, at every hypothesis and the goal using push_neg at * or at selected hypotheses and the goal using say push_neg at h h' ⊢, as usual.

Equations

• Mathlib.Tactic.Push.convPush_neg = Lean.ParserDescr.node `Mathlib.Tactic.Push.convPush_neg 1024 (Lean.ParserDescr.nonReservedSymbol "push_neg" false)

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

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

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

Equations

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

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

The syntax is #push_neg e, where e is an expression, which will print the push_neg form of e.

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

Equations

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

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

pull is the inverse tactic to push. It pulls the given constant towards the head of the expression. For example

• 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.

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.

Equations

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

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.

Equations

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

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.

Equations

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

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.

Equations

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