tactic.push_neg - mathlib docs

source

theorem push_neg.not_not_eq (p : Prop) :

(¬¬p) = p

source

theorem push_neg.not_and_eq (p q : Prop) :

(¬(p ∧ q)) = (p → ¬q)

source

theorem push_neg.not_or_eq (p q : Prop) :

(¬(p ∨ q)) = (¬p ∧ ¬q)

source

theorem push_neg.not_forall_eq {α : Sort u} (s : α → Prop) :

(¬∀ (x : α), s x) = ∃ (x : α), ¬s x

source

theorem push_neg.not_exists_eq {α : Sort u} (s : α → Prop) :

(¬∃ (x : α), s x) = ∀ (x : α), ¬s x

source

theorem push_neg.not_implies_eq (p q : Prop) :

(¬(p → q)) = (p ∧ ¬q)

source

theorem push_neg.classical.implies_iff_not_or (p q : Prop) :

p → q ↔ ¬p ∨ q

source

theorem push_neg.not_eq {α : Sort u} (a b : α) :

¬a = b ↔ a ≠ b

source

theorem push_neg.not_le_eq {β : Type u} [linear_order β] (a b : β) :

(¬a ≤ b) = (b < a)

source

theorem push_neg.not_lt_eq {β : Type u} [linear_order β] (a b : β) :

(¬a < b) = (b ≤ a)

source

meta def push_neg.whnf_reducible (e : expr) :

tactic expr

source

meta def push_neg.normalize_negations (t : expr) :

tactic (expr × expr)

source

meta def push_neg.push_neg_at_hyp (h : name) :

tactic unit

source

meta def push_neg.push_neg_at_goal :

tactic unit

source

meta def tactic.interactive.push_neg :

interactive.parse interactive.types.location → tactic unit

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.

source

def tactic_doc.tactic.push_neg :

tactic_doc_entry

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.

source

theorem imp_of_not_imp_not (P Q : Prop) :

(¬Q → ¬P) → P → Q

source

meta def name_with_opt :

lean.parser (name × option name)

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

source

meta def tactic.interactive.contrapose (push : interactive.parse (optional (lean.parser.tk "!"))) :

interactive.parse (optional name_with_opt) → tactic unit

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

source

def tactic_doc.tactic.contrapose :

tactic_doc_entry

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