Documentation

Mathlib.Tactic.PushNeg

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_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_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

Make push_neg use not_and_or rather than the default not_and.

Push negations at the top level of the current expression.

Equations
  • One or more equations did not get rendered due to their size.
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.

    Equations
    • One or more equations did not get rendered due to their size.
    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.

      Equations
      Instances For

        Execute push_neg as a conv tactic.

        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

            Execute main loop of push_neg at the main goal.

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

              Execute main loop of push_neg at a local hypothesis.

              Equations
              • One or more equations did not get rendered due to their size.
              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.

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