mathlib4/MathlibTest/byContra.lean at dfc464f8ca9e61c8fc256dbea579eb6d56a369fa · leanprover-community/mathlib4 · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
-- tests for by_contra! tactic
module
import Mathlib.Tactic.ByContra
import Mathlib.Tactic.Rename
import Mathlib.Tactic.Set
import Mathlib.Algebra.Notation.Defs
import Mathlib.Data.Nat.Basic
import Mathlib.Order.Basic

example (a b : ℕ) (foo : False) : a < b := by
  by_contra!
  guard_hyp this : b ≤ a
  exact foo

example (a b : ℕ) (h : False) : a < b := by
  by_contra! foo
  revert foo; change b ≤ a → False; intro;
  exact h

example (a b : ℕ) (h : False) : a < b := by
  by_contra! foo : ¬ a < b -- can avoid push Not
  guard_hyp foo : ¬ a < b
  exact h

example : 1 < 2 := by
  by_contra!
  guard_hyp this : 2 ≤ 1
  contradiction

example (p : Prop) (bar : False) : ¬ ¬ ¬ ¬ ¬ ¬ p := by
  by_contra! foo : ¬ ¬ ¬ p -- normalises to ¬ p, as does ¬ (goal).
  guard_hyp foo : ¬ ¬ ¬ p
  exact bar

example (p : Prop) (bar : False) : ¬ ¬ ¬ ¬ ¬ ¬ p := by
  by_contra! : ¬ ¬ ¬ p
  guard_hyp this : ¬ ¬ ¬ p
  exact bar

/--
error: Type mismatch
  h✝
has type
  b ≤ a
but is expected to have type
  a ≤ b
---
error: unsolved goals
a b : ℕ
this : a ≤ b
⊢ False
-/
#guard_msgs in
example (a b : ℕ) : a < b := by
  by_contra! : a ≤ b

example (P Q : Prop) (h' : False) : P ∧ Q := by
  fail_if_success by_contra! +fdsewfjdsk h
  by_contra! +distrib h
  guard_hyp h : ¬P ∨ ¬Q
  exact h'

section order

variable {α} [LinearOrder α] [One α] [Mul α]

example (x : α) (f : False) : x ≤ 1 := by
  set a := x * x
  by_contra! h
  guard_hyp h : 1 < x
  assumption

example (x : α) (f : False) : x ≤ 1 := by
  let _a := x * x
  by_contra! h
  guard_hyp h : 1 < x
  assumption

example (x : α) (f : False) : x ≤ 1 := by
  set a := x * x
  have : a ≤ a := le_rfl
  by_contra! h
  guard_hyp h : 1 < x
  assumption

end order

example (n : ℕ) (h : n ≠ 0) : n ≠ 0 := by
  by_contra rfl
  simp only [Ne, not_true_eq_false] at h

/-- warning: `push` made no progress at h._@.MathlibTest.byContra.2021293407._hygCtx._hyg.18 -/
#guard_msgs in
example (n : ℕ) (h : n ≠ 0) : n ≠ 0 := by
  by_contra! rfl
  simp only [Ne, not_true_eq_false] at h

example (p q : Prop) (hnp : ¬ p) : ¬ p ∨ ¬ q := by
  by_contra! ⟨hp, _⟩
  exact hnp hp

example (p q : Prop) (hnp : ¬ p) (hnq : ¬ q) : ¬ (p ∨ q) := by
  by_contra hp | hq
  · exact hnp hp
  · exact hnq hq

/-- warning: `push` made no progress at h._@.MathlibTest.byContra.2021293410._hygCtx._hyg.25 -/
#guard_msgs in
example (p q : Prop) (hnp : ¬ p) (hnq : ¬ q) : ¬ (p ∨ q) := by
  by_contra! hp | hq
  · exact hnp hp
  · exact hnq hq