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

source
theorem Mathlib.Tactic.Push.not_iff (p q : Prop) :
¬(p ↔ q) ↔ p ∧ ¬q ∨ ¬p ∧ q
source
theorem Mathlib.Tactic.Push.not_exists {α : Sort u_1} (s : α → Prop) :
¬Exists s ↔ ∀ (x : α), binderNameHint x s ¬s x
source
theorem Mathlib.Tactic.Push.not_and_eq (p q : Prop) :
(¬(p ∧ q)) = (p → ¬q)
source
theorem Mathlib.Tactic.Push.not_and_or_eq (p q : Prop) :
(¬(p ∧ q)) = (¬p ∨ ¬q)
source
theorem Mathlib.Tactic.Push.not_forall_eq {α : Sort u_1} (s : α → Prop) :
(¬∀ (x : α), s x) = ∃ (x : α), ¬s x
source
opaque Mathlib.Tactic.Push.push_neg.use_distrib :
Lean.Option Bool

Make `push_neg` use `not_and_or` rather than the default `not_and`.

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

The `simp` configuration used in `push`.

Equations

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

source
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]

Instances For

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

Instances For

source
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`.

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!`.

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.

Instances For

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

Instances For

source
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

Instances For

source
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

Instances For

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

Instances For

source
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`.

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!`.

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)

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For

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

Instances For