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.
Make push_neg
use not_and_or
rather than the default not_and
.
The simp
configuration used in push
.
Instances For
Try to rewrite using a push
lemma.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Common entry point to the implementation of push
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Try to rewrite using a pull
lemma.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Common entry point to the implementation of pull
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
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
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
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
push
pushes the given constant away from the head of the expression. For example
push _ ∈ _
rewritesx ∈ {y} ∪ zᶜ
intox = y ∨ ¬ x ∈ z
.push (disch := positivity) Real.log
rewriteslog (a * b ^ 2)
intolog a + 2 * log b
.push ¬ _
is the same aspush_neg
orpush Not
, and it rewrites¬ ∀ ε > 0, ∃ δ > 0, δ < ε
into∃ ε > 0, ∀ δ > 0, ε ≤ δ
.
In addition to constants, push
can be used to push fun
and ∀
binders:
push fun _ ↦ _
rewritesfun x => f x ^ 2 + 5
intof ^ 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
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.
Instances For
pull
is the inverse tactic to push
.
It pulls the given constant towards the head of the expression. For example
pull _ ∈ _
rewritesx ∈ y ∨ ¬ x ∈ z
intox ∈ y ∪ zᶜ
.pull (disch := positivity) Real.log
rewriteslog a + 2 * log b
intolog (a * b ^ 2)
.pull fun _ ↦ _
rewritesf ^ 2 + 5
intofun x => f x ^ 2 + 5
wheref
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 apull
lemma, butnot_not : ¬ ¬ p ↔ p
is not.log_mul : log (x * y) = log x + log y
is apull
lemma, butlog_abs : log |x| = log x
is not.Pi.mul_def : f * g = fun (i : ι) => f i * g i
andPi.one_def : 1 = fun (x : ι) => 1
are bothpull
lemmas forfun
, because everypush fun _ ↦ _
lemma is also considered apull
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
A simproc variant of push fun _ ↦ _
, to be used as simp [↓pushFun]
.
Instances For
A simproc variant of pull fun _ ↦ _
, to be used as simp [pullFun]
.
Instances For
push
pushes the given constant away from the head of the expression. For example
push _ ∈ _
rewritesx ∈ {y} ∪ zᶜ
intox = y ∨ ¬ x ∈ z
.push (disch := positivity) Real.log
rewriteslog (a * b ^ 2)
intolog a + 2 * log b
.push ¬ _
is the same aspush_neg
orpush Not
, and it rewrites¬ ∀ ε > 0, ∃ δ > 0, δ < ε
into∃ ε > 0, ∀ δ > 0, ε ≤ δ
.
In addition to constants, push
can be used to push fun
and ∀
binders:
push fun _ ↦ _
rewritesfun x => f x ^ 2 + 5
intof ^ 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
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)
Instances For
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
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
pull
is the inverse tactic to push
.
It pulls the given constant towards the head of the expression. For example
pull _ ∈ _
rewritesx ∈ y ∨ ¬ x ∈ z
intox ∈ y ∪ zᶜ
.pull (disch := positivity) Real.log
rewriteslog a + 2 * log b
intolog (a * b ^ 2)
.pull fun _ ↦ _
rewritesf ^ 2 + 5
intofun x => f x ^ 2 + 5
wheref
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 apull
lemma, butnot_not : ¬ ¬ p ↔ p
is not.log_mul : log (x * y) = log x + log y
is apull
lemma, butlog_abs : log |x| = log x
is not.Pi.mul_def : f * g = fun (i : ι) => f i * g i
andPi.one_def : 1 = fun (x : ι) => 1
are bothpull
lemmas forfun
, because everypush fun _ ↦ _
lemma is also considered apull
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
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.