If the target of the main goal is a proposition p,
by_contra' reduces the goal to proving False using the additional hypothesis this : ¬ p¬ p.
by_contra' h can be used to name the hypothesis h : ¬ p¬ p.
The hypothesis ¬ p¬ p will be negation normalized using push_neg.
For instance, ¬ a < b¬ a < b will be changed to b ≤ a≤ a.
by_contra' h : q will normalize negations in ¬ p¬ p, normalize negations in q,
and then check that the two normalized forms are equal.
The resulting hypothesis is the pre-normalized form, q.
If the name h is not explicitly provided, then this will be used as name.
This tactic uses classical reasoning.
It is a variant on the tactic by_contra.
Examples:
example : 1 < 2 := by
by_contra' h
-- h : 2 ≤ 1 ⊢ False
example : 1 < 2 := by
by_contra' h : ¬ 1 < 2
-- h : ¬ 1 < 2 ⊢ False
≤ 1 ⊢ False
example : 1 < 2 := by
by_contra' h : ¬ 1 < 2
-- h : ¬ 1 < 2 ⊢ False
⊢ False
example : 1 < 2 := by
by_contra' h : ¬ 1 < 2
-- h : ¬ 1 < 2 ⊢ False
¬ 1 < 2
-- h : ¬ 1 < 2 ⊢ False
¬ 1 < 2 ⊢ False
⊢ False
Equations
- One or more equations did not get rendered due to their size.