Documentation

Mathlib.Tactic.PushNeg

source
ink
theorem Mathlib.Tactic.PushNeg.not_not_eq (p : Prop) :
(¬¬p) = p
source
ink
theorem Mathlib.Tactic.PushNeg.not_and_eq (p : Prop) (q : Prop) :
(¬(p ∧ q)) = (p → ¬q)
source
ink
theorem Mathlib.Tactic.PushNeg.not_and_or_eq (p : Prop) (q : Prop) :
(¬(p ∧ q)) = (¬p ∨ ¬q)
source
ink
theorem Mathlib.Tactic.PushNeg.not_or_eq (p : Prop) (q : Prop) :
(¬(p ∨ q)) = (¬p ∧ ¬q)
source
ink
theorem Mathlib.Tactic.PushNeg.not_forall_eq {α : Sort u_1} (s : α → Prop) :
(¬((x : α) → s x)) = ∃ x, ¬s x
source
ink
theorem Mathlib.Tactic.PushNeg.not_exists_eq {α : Sort u_1} (s : α → Prop) :
(¬∃ x, s x) = ∀ (x : α), ¬s x
source
ink
theorem Mathlib.Tactic.PushNeg.not_implies_eq (p : Prop) (q : Prop) :
(¬(p → q)) = (p ∧ ¬q)
source
ink
theorem Mathlib.Tactic.PushNeg.not_ne_eq {α : Sort u_1} (x : α) (y : α) :
(¬x ≠ y) = (x = y)
source
ink
theorem Mathlib.Tactic.PushNeg.not_le_eq {β : Type u} [inst : LinearOrder β] (a : β) (b : β) :
(¬a ≤ b) = (b < a)
source
ink
theorem Mathlib.Tactic.PushNeg.not_lt_eq {β : Type u} [inst : LinearOrder β] (a : β) (b : β) :
(¬a < b) = (b ≤ a)
source
ink
opaque Mathlib.Tactic.PushNeg.push_neg.use_distrib :
Lean.Option Bool

Make push_neg use not_and_distrib rather than the default not_and.

source
ink
def Mathlib.Tactic.PushNeg.transformNegationStep (e : Lean.Expr) :
Lean.Meta.SimpM (Option Lean.Meta.Simp.Step)

Push negations at the top level of the current expression.

Equations
  • One or more equations did not get rendered due to their size.
source
ink
partial def Mathlib.Tactic.PushNeg.transformNegation (e : Lean.Expr) :
Lean.Meta.SimpM Lean.Meta.Simp.Step

Recursively push negations at the top level of the current expression. This is needed to handle e.g. triple negation.

source
ink
def Mathlib.Tactic.PushNeg.pushNegCore (tgt : Lean.Expr) :
Lean.MetaM Lean.Meta.Simp.Result

Common entry point to push_neg as a conv.

Equations
  • One or more equations did not get rendered due to their size.
source
ink
def Mathlib.Tactic.PushNeg.pushNegConv :
Lean.ParserDescr

Push negations into the conclusion of an expression. For instance, an expression ¬ ∀ x, ∃ y, x ≤ y¬ ∀ x, ∃ y, x ≤ y∀ x, ∃ y, x ≤ y∃ y, x ≤ y≤ y will be transformed by push_neg into ∃ x, ∀ y, y < x∃ x, ∀ y, y < x∀ y, y < x. Variable names are conserved. This tactic pushes negations inside expressions. For instance, given a hypothesis

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

writing push_neg will turn the target into

| ∃ ε, ε > 0 ∧ ∀ δ, δ > 0 → (∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀|),
∃ ε, ε > 0 ∧ ∀ δ, δ > 0 → (∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀|),
∧ ∀ δ, δ > 0 → (∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀|),
∀ δ, δ > 0 → (∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀|),
→ (∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀|),
∃ x, |x - x₀| ≤ δ ∧ ε < |f x - y₀|),
≤ δ ∧ ε < |f x - y₀|),
∧ ε < |f x - y₀|),

(The pretty printer does not use the abreviations ∀ δ > 0∀ δ > 0 and ∃ ε > 0∃ ε > 0 but this issue has nothing to do with push_neg).

Note that names are conserved by this tactic, contrary to what would happen with simp using the relevant lemmas.

This tactic has two modes: in standard mode, it transforms ¬(p ∧ q)¬(p ∧ q)∧ q) into p → ¬q→ ¬q¬q, whereas in distrib mode it produces ¬p ∨ ¬q¬p ∨ ¬q∨ ¬q¬q. To use distrib mode, use set_option push_neg.use_distrib true.

Equations
source
ink
def Mathlib.Tactic.PushNeg.elabPushNegConv :
Lean.Elab.Tactic.Tactic

Execute push_neg as a conv tactic.

Equations
  • One or more equations did not get rendered due to their size.
source
ink
def Mathlib.Tactic.PushNeg.pushNeg :
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.
source
ink
def Mathlib.Tactic.PushNeg.pushNegTarget :
Lean.Elab.Tactic.TacticM Unit

Execute main loop of push_neg at the main goal.

Equations
  • One or more equations did not get rendered due to their size.
source
ink
def Mathlib.Tactic.PushNeg.pushNegLocalDecl (fvarId : Lean.FVarId) :
Lean.Elab.Tactic.TacticM Unit

Execute main loop of push_neg at a local hypothesis.

Equations
  • One or more equations did not get rendered due to their size.
source
ink
def Mathlib.Tactic.PushNeg.tacticPush_neg__ :
Lean.ParserDescr

Push negations into the conclusion of a hypothesis. For instance, a hypothesis h : ¬ ∀ x, ∃ y, x ≤ y¬ ∀ x, ∃ y, x ≤ y∀ x, ∃ y, x ≤ y∃ y, x ≤ y≤ y will be transformed by push_neg at h into h : ∃ x, ∀ y, y < x∃ x, ∀ y, y < x∀ y, y < x. Variable names are conserved. This tactic pushes negations inside expressions. For instance, given a hypothesis

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

writing push_neg at h will turn h into

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

(The pretty printer does not use the abreviations ∀ δ > 0∀ δ > 0 and ∃ ε > 0∃ ε > 0 but this issue has nothing to do with push_neg).

Note that names are conserved by this tactic, contrary to what would happen with simp using the relevant lemmas. One can also 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.

This tactic has two modes: in standard mode, it transforms ¬(p ∧ q)¬(p ∧ q)∧ q) into p → ¬q→ ¬q¬q, whereas in distrib mode it produces ¬p ∨ ¬q¬p ∨ ¬q∨ ¬q¬q. To use distrib mode, use set_option push_neg.use_distrib true.

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