The push_neg tactic

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

theorem Mathlib.Tactic.PushNeg.not_not_eq (p : Prop) : (¬¬p) = p

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

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

theorem Mathlib.Tactic.PushNeg.not_or_eq (p q : Prop) : (¬(p ∨ q)) = (¬p ∧ ¬q)

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

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

theorem Mathlib.Tactic.PushNeg.not_implies_eq (p q : Prop) : (¬(p → q)) = (p ∧ ¬q)

theorem Mathlib.Tactic.PushNeg.not_ne_eq {α : Sort u_1} (x y : α) : (¬x ≠ y) = (x = y)

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

theorem Mathlib.Tactic.PushNeg.not_le_eq {β : Type u_2} [LinearOrder β] (a b : β) : (¬a ≤ b) = (b < a)

theorem Mathlib.Tactic.PushNeg.not_lt_eq {β : Type u_2} [LinearOrder β] (a b : β) : (¬a < b) = (b ≤ a)

theorem Mathlib.Tactic.PushNeg.not_ge_eq {β : Type u_2} [LinearOrder β] (a b : β) : (¬a ≥ b) = (a < b)

theorem Mathlib.Tactic.PushNeg.not_gt_eq {β : Type u_2} [LinearOrder β] (a b : β) : (¬a > b) = (a ≤ b)

theorem Mathlib.Tactic.PushNeg.not_nonempty_eq {β : Type u_2} (s : Set β) : (¬s.Nonempty) = (s = ∅)

theorem Mathlib.Tactic.PushNeg.ne_empty_eq_nonempty {β : Type u_2} (s : Set β) : (s ≠ ∅) = s.Nonempty

theorem Mathlib.Tactic.PushNeg.empty_ne_eq_nonempty {β : Type u_2} (s : Set β) : (∅ ≠ s) = s.Nonempty

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

Make push_neg use not_and_or rather than the default not_and.

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.

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.

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

Common entry point to push_neg as a conv.

def Mathlib.Tactic.PushNeg.pushNegConv : Lean.ParserDescr

Push negations into the conclusion of an expression. For instance, an expression ¬ ∀ x, ∃ y, x ≤ y will be transformed by push_neg into ∃ 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₀| ≤ ε)

writing push_neg will turn the target into

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

(The pretty printer does not use the abbreviations ∀ δ > 0 and ∃ ε > 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) into p → ¬q, whereas in distrib mode it produces ¬p ∨ ¬q. To use distrib mode, use set_option push_neg.use_distrib true.

def Mathlib.Tactic.PushNeg.elabPushNegConv : Lean.Elab.Tactic.Tactic

Execute push_neg as a conv tactic.

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.

def Mathlib.Tactic.PushNeg.pushNegTarget : Lean.Elab.Tactic.TacticM Unit

Execute main loop of push_neg at the main goal.

def Mathlib.Tactic.PushNeg.pushNegLocalDecl (fvarId : Lean.FVarId) : Lean.Elab.Tactic.TacticM Unit

Execute main loop of push_neg at a local hypothesis.

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 will be transformed by push_neg at h into h : ∃ 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₀| ≤ ε)

writing push_neg at h will turn h into

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

(The pretty printer does not use the abbreviations ∀ δ > 0 and ∃ ε > 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) into p → ¬q, whereas in distrib mode it produces ¬p ∨ ¬q. To use distrib mode, use set_option push_neg.use_distrib true.