mathlib documentation

tactic.push_neg

A tactic pushing negations into an expression #

theorem push_neg.not_not_eq (p : Prop) :
(¬¬p) = p
theorem push_neg.not_and_eq (p q : Prop) :
(¬(p q)) = (p ¬q)
theorem push_neg.not_and_distrib_eq (p q : Prop) :
(¬(p q)) = (¬p ¬q)
theorem push_neg.not_or_eq (p q : Prop) :
(¬(p q)) = (¬p ¬q)
theorem push_neg.not_forall_eq {α : Sort u} (s : α Prop) :
(¬ (x : α), s x) = (x : α), ¬s x
theorem push_neg.not_exists_eq {α : Sort u} (s : α Prop) :
(¬ (x : α), s x) = (x : α), ¬s x
theorem push_neg.not_implies_eq (p q : Prop) :
(¬(p q)) = (p ¬q)
theorem push_neg.classical.implies_iff_not_or (p q : Prop) :
p q ¬p q
theorem push_neg.not_eq {α : Sort u} (a b : α) :
¬a = b a b
theorem push_neg.not_le_eq {β : Type u} [linear_order β] (a b : β) :
(¬a b) = (b < a)
theorem push_neg.not_lt_eq {β : Type u} [linear_order β] (a b : β) :
(¬a < b) = (b a)

Push negations in the goal of some assumption.

For instance, a hypothesis h : ¬ ∀ x, ∃ y, x ≤ y will be transformed by push_neg at h into h : ∃ x, ∀ y, y < x. Variables names are conserved.

This tactic pushes negations inside expressions. For instance, given an assumption

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 abreviations ∀ δ > 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 assumption and the goal using push_neg at * or at selected assumptions and the goal using say push_neg at h h' ⊢ as usual.

Push negations in the goal of some assumption.

For instance, a hypothesis h : ¬ ∀ x, ∃ y, x ≤ y will be transformed by push_neg at h into h : ∃ x, ∀ y, y < x. Variables names are conserved.

This tactic pushes negations inside expressions. For instance, given an assumption

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 abreviations ∀ δ > 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 assumption and the goal using push_neg at * or at selected assumptions and the goal using say push_neg at h h' ⊢ as usual.

theorem imp_of_not_imp_not (P Q : Prop) :
(¬Q ¬P) P Q

Matches either an identifier "h" or a pair of identifiers "h with k"

Transforms the goal into its contrapositive.

  • contrapose turns a goal P → Q into ¬ Q → ¬ P
  • contrapose! turns a goal P → Q into ¬ Q → ¬ P and pushes negations inside P and Q using push_neg
  • contrapose h first reverts the local assumption h, and then uses contrapose and intro h
  • contrapose! h first reverts the local assumption h, and then uses contrapose! and intro h
  • contrapose h with new_h uses the name new_h for the introduced hypothesis

Transforms the goal into its contrapositive.

  • contrapose turns a goal P → Q into ¬ Q → ¬ P
  • contrapose! turns a goal P → Q into ¬ Q → ¬ P and pushes negations inside P and Q using push_neg
  • contrapose h first reverts the local assumption h, and then uses contrapose and intro h
  • contrapose! h first reverts the local assumption h, and then uses contrapose! and intro h
  • contrapose h with new_h uses the name new_h for the introduced hypothesis

#push_neg command #

A user command to run push_neg. Mostly copied from the #norm_num and #simp commands.

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.

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.