Documentation

Mathlib.Tactic.PushNeg

theorem Mathlib.Tactic.PushNeg.not_and_eq (p : Prop) (q : Prop) :
(¬(p q)) = (p¬q)
theorem Mathlib.Tactic.PushNeg.not_or_eq (p : Prop) (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 : Prop) (q : Prop) :
(¬(pq)) = (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 : Prop) (q : Prop) :
(¬(p q)) = (p ¬q ¬p q)
theorem Mathlib.Tactic.PushNeg.not_le_eq {β : Type u} [LinearOrder β] (a : β) (b : β) :
(¬a b) = (b < a)
theorem Mathlib.Tactic.PushNeg.not_lt_eq {β : Type u} [LinearOrder β] (a : β) (b : β) :
(¬a < b) = (b a)
theorem Mathlib.Tactic.PushNeg.not_ge_eq {β : Type u} [LinearOrder β] (a : β) (b : β) :
(¬a b) = (a < b)
theorem Mathlib.Tactic.PushNeg.not_gt_eq {β : Type u} [LinearOrder β] (a : β) (b : β) :
(¬a > b) = (a b)

Make push_neg use not_and_or rather than the default not_and.

Push negations at the top level of the current expression.

Instances For

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

    Common entry point to push_neg as a conv.

    Instances For

      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.

      Instances For

        Execute push_neg as a conv tactic.

        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.

          Instances For

            Execute main loop of push_neg at the main goal.

            Instances For

              Execute main loop of push_neg at a local hypothesis.

              Instances For

                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.

                Instances For