this repo has no description
initial commit
+806
+8
leanpkg.toml
+8
leanpkg.toml
+151
src/ch12.lean
+151
src/ch12.lean
···
1
+
section
2
+
variable {U : Type}
3
+
variables {A B C : set U}
4
+
5
+
example : ∀ x, x ∈ A ∩ C → x ∈ A ∪ B :=
6
+
assume x : U,
7
+
assume : x ∈ A ∩ C,
8
+
show x ∈ A ∪ B, from or.inl (and.left this)
9
+
10
+
example : ∀ x, x ∈ -(A ∪ B) → x ∈ -A :=
11
+
assume x,
12
+
assume h1 : x ∈ -(A ∪ B),
13
+
show x ∈ -A, from
14
+
assume : x ∈ A,
15
+
show false, from h1 (or.inl this)
16
+
end
17
+
18
+
---
19
+
20
+
import data.set
21
+
open set
22
+
23
+
section
24
+
variable {U : Type}
25
+
26
+
example (A B C : set U) : ∀ x, x ∈ A ∩ C → x ∈ A ∪ B :=
27
+
assume x,
28
+
assume : x ∈ A ∩ C,
29
+
show x ∈ A ∪ B, from or.inl this.left
30
+
31
+
example (A B : set U) : ∀ x, x ∈ -(A ∪ B) → x ∈ -A :=
32
+
assume x,
33
+
assume : x ∈ -(A ∪ B),
34
+
show x ∈ -A, from
35
+
assume : x ∈ A,
36
+
show false, from ‹ x ∈ -(A ∪ B) › (or.inl this)
37
+
38
+
/- defining "disjoint" -/
39
+
40
+
def disj (A B : set U) : Prop := ∀ ⦃x⦄, x ∈ A → x ∈ B → false
41
+
42
+
example (A B : set U) (h : ∀ x, ¬ (x ∈ A ∧ x ∈ B)) :
43
+
disj A B :=
44
+
assume x,
45
+
assume h1 : x ∈ A,
46
+
assume h2 : x ∈ B,
47
+
have h3 : x ∈ A ∧ x ∈ B, from and.intro h1 h2,
48
+
show false, from h x h3
49
+
50
+
-- notice that we do not have to mention x when applying
51
+
-- h : disj A B
52
+
example (A B : set U) (h1 : disj A B) (x : U)
53
+
(h2 : x ∈ A) (h3 : x ∈ B) :
54
+
false :=
55
+
h1 h2 h3
56
+
57
+
-- the same is true of ⊆
58
+
example (A B : set U) (x : U) (h : A ⊆ B) (h1 : x ∈ A) :
59
+
x ∈ B :=
60
+
h h1
61
+
62
+
example (A B C D : set U) (h1 : disj A B) (h2 : C ⊆ A)
63
+
(h3 : D ⊆ B) :
64
+
disj C D :=
65
+
assume x,
66
+
assume : x ∈ C,
67
+
assume : x ∈ D,
68
+
show false, from h1 (h2 ‹ x ∈ C › ) (h3 ‹ x ∈ D ›)
69
+
end
70
+
71
+
---
72
+
73
+
import data.set
74
+
open set
75
+
76
+
section
77
+
variables {I U : Type}
78
+
variables {A B : I → set U}
79
+
80
+
theorem Inter.intro {x : U} (h : ∀ i, x ∈ A i) : x ∈ ⋂ i, A i :=
81
+
by simp; assumption
82
+
83
+
@[elab_simple]
84
+
theorem Inter.elim {x : U} (h : x ∈ ⋂ i, A i) (i : I) : x ∈ A i :=
85
+
by simp at h; apply h
86
+
87
+
theorem Union.intro {x : U} (i : I) (h : x ∈ A i) : x ∈ ⋃ i, A i :=
88
+
by {simp, existsi i, exact h}
89
+
90
+
theorem Union.elim {b : Prop} {x : U}
91
+
(h₁ : x ∈ ⋃ i, A i) (h₂ : ∀ (i : I), x ∈ A i → b) : b :=
92
+
by {simp at h₁, cases h₁ with i h, exact h₂ i h}
93
+
94
+
end
95
+
96
+
-- BEGIN
97
+
variables {I U : Type}
98
+
variables (A : I → set U) (B : I → set U) (C : set U)
99
+
100
+
example : (⋂ i, A i) ∩ (⋂ i, B i) ⊆ (⋂ i, A i ∩ B i) :=
101
+
assume x,
102
+
assume h1 : x ∈ (⋂ i, A i) ∩ (⋂ i, B i),
103
+
show x ∈ (⋂ i, A i ∩ B i), from
104
+
have h2 : ∀ i, x ∈ A i ∩ B i, from
105
+
assume i : I,
106
+
have x ∈ A i, from Inter.elim (h1.left) i,
107
+
have x ∈ B i, from Inter.elim (h1.right) i,
108
+
⟨ ‹ x ∈ A i › , ‹ x ∈ B i › ⟩,
109
+
Inter.intro h2
110
+
111
+
example : C ∩ (⋃i, A i) ⊆ ⋃i, C ∩ A i :=
112
+
assume x,
113
+
assume h,
114
+
have h2 : ∀ (i : I), x ∈ A i → x ∈ ⋃i, C ∩ A i, from
115
+
assume i : I,
116
+
assume h1,
117
+
have x ∈ C ∩ A i, from ⟨ h.left , h1 ⟩,
118
+
Union.intro i ‹ x ∈ C ∩ A i › ,
119
+
120
+
Union.elim h.right h2
121
+
122
+
-- END
123
+
124
+
---
125
+
126
+
import data.set
127
+
open set
128
+
129
+
-- BEGIN
130
+
variable {U : Type}
131
+
variables A B C : set U
132
+
133
+
-- For this exercise these two facts are useful
134
+
example (h1 : A ⊆ B) (h2 : B ⊆ C) : A ⊆ C :=
135
+
subset.trans h1 h2
136
+
137
+
example : A ⊆ A :=
138
+
subset.refl A
139
+
140
+
example (h : A ⊆ B) : powerset A ⊆ powerset B :=
141
+
assume x,
142
+
assume : x ∈ powerset A,
143
+
have x ⊆ A, from ‹ x ∈ powerset A ›,
144
+
have x ⊆ B, from subset.trans ‹ x ⊆ A › h,
145
+
show x ∈ powerset B, from ‹ x ⊆ B ›
146
+
147
+
example (h : powerset A ⊆ powerset B) : A ⊆ B :=
148
+
assume x,
149
+
assume : x ∈ A,
150
+
h (subset.refl A) ‹ x ∈ A ›
151
+
-- END
+83
src/ch14.lean
+83
src/ch14.lean
···
1
+
2
+
---
3
+
4
+
section
5
+
parameters {A : Type} {R : A → A → Prop}
6
+
parameter (irreflR : irreflexive R)
7
+
parameter (transR : transitive R)
8
+
9
+
local infix < := R
10
+
11
+
def R' (a b : A) : Prop := R a b ∨ a = b
12
+
local infix ≤ := R'
13
+
14
+
theorem reflR' (a : A) : a ≤ a := or.inr (refl a)
15
+
16
+
theorem transR' {a b c : A} (h1 : a ≤ b) (h2 : b ≤ c):
17
+
a ≤ c :=
18
+
or.elim h1
19
+
(assume : a < b,
20
+
show a ≤ c, from
21
+
or.elim h2
22
+
(assume : b < c, or.inl (transR ‹ a < b › ‹ b < c ›))
23
+
(assume : b = c, or.inl (eq.subst ‹ b = c › ‹ a < b ›)))
24
+
(assume : a = b,
25
+
show a ≤ c, from
26
+
or.elim h2
27
+
(assume : b < c, or.inl (eq.symm ‹ a = b › ▸ ‹ b < c ›))
28
+
(assume : b = c, or.inr (‹ b = c › ▸ ‹ a = b ›)))
29
+
30
+
theorem antisymmR' {a b : A} (h1 : a ≤ b) (h2 : b ≤ a) :
31
+
a = b :=
32
+
or.elim h1
33
+
(assume : a < b,
34
+
or.elim h2
35
+
(assume : b < a, have false, from (irreflR a) (transR ‹ a < b › ‹ b < a ›), ‹ false ›.elim)
36
+
(assume : b = a, eq.symm this)
37
+
)
38
+
(assume : a = b, eq.symm (eq.symm this))
39
+
end
40
+
41
+
---
42
+
43
+
section
44
+
parameters {A : Type} {R : A → A → Prop}
45
+
parameter (reflR : reflexive R)
46
+
parameter (transR : transitive R)
47
+
48
+
def S (a b : A) : Prop := R a b ∧ R b a
49
+
50
+
example : transitive S :=
51
+
assume a b c,
52
+
assume h1 h2,
53
+
⟨ transR h1.left h2.left , transR h2.right h1.right ⟩
54
+
55
+
end
56
+
57
+
---
58
+
59
+
section
60
+
parameters {A : Type} {a b c : A} {R : A → A → Prop}
61
+
parameter (Rab : R a b)
62
+
parameter (Rbc : R b c)
63
+
parameter (nRac : ¬ R a c)
64
+
65
+
-- Prove one of the following two theorems:
66
+
67
+
theorem R_is_strict_partial_order :
68
+
irreflexive R ∧ transitive R :=
69
+
sorry
70
+
71
+
theorem R_is_not_strict_partial_order :
72
+
¬(irreflexive R ∧ transitive R) :=
73
+
assume h : irreflexive R ∧ transitive R,
74
+
show false, from
75
+
nRac (h.right Rab Rbc)
76
+
end
77
+
78
+
---
79
+
80
+
open nat
81
+
82
+
example : 1 ≤ 4 :=
83
+
le_succ_of_le $ le_succ_of_le $ le_succ 1
+117
src/ch16.lean
+117
src/ch16.lean
···
1
+
open function int algebra
2
+
3
+
def f (x : ℤ) : ℤ := x + 3
4
+
def g (x : ℤ) : ℤ := -x
5
+
def h (x : ℤ) : ℤ := 2 * x + 3
6
+
7
+
example : injective f :=
8
+
assume x1 x2,
9
+
assume h1 : x1 + 3 = x2 + 3, -- Lean knows this is the same as f x1 = f x2
10
+
show x1 = x2, from eq_of_add_eq_add_right h1
11
+
12
+
example : surjective f :=
13
+
assume y,
14
+
have h1 : f (y - 3) = y, from calc
15
+
f (y - 3) = (y - 3) + 3 : rfl
16
+
... = y : by rw sub_add_cancel,
17
+
show ∃ x, f x = y, from exists.intro (y - 3) h1
18
+
19
+
example (x y : ℤ) (h : 2 * x = 2 * y) : x = y :=
20
+
have h1 : 2 ≠ (0 : ℤ), from dec_trivial, -- this tells Lean to figure it out itself
21
+
show x = y, from eq_of_mul_eq_mul_left h1 h
22
+
23
+
example (x : ℤ) : -(-x) = x := neg_neg x
24
+
25
+
example (A B : Type) (u : A → B) (v : B → A) (h : left_inverse u v) :
26
+
∀ x, u (v x) = x :=
27
+
h
28
+
29
+
example (A B : Type) (u : A → B) (v : B → A) (h : left_inverse u v) :
30
+
right_inverse v u :=
31
+
h
32
+
33
+
-- fill in the sorry's in the following proofs
34
+
35
+
example : injective h :=
36
+
assume x₁ x₂,
37
+
assume : 2 * x₁ + 3 = 2 * x₂ + 3,
38
+
have 2 * x₁ = 2 * x₂ , from eq_of_add_eq_add_right this,
39
+
have 2 ≠ (0 : ℤ), from dec_trivial,
40
+
show x₁ = x₂ , from eq_of_mul_eq_mul_left this ‹ 2 * x₁ = 2 * x₂ ›
41
+
42
+
example : surjective g :=
43
+
assume y,
44
+
have h₁ : g (-y) = y, from calc
45
+
g (-y) = -(-y): rfl
46
+
... = y: by rw neg_neg,
47
+
show ∃ x, g x = y, from exists.intro (-y) h₁
48
+
49
+
example (A B : Type) (u : A → B) (v1 : B → A) (v2 : B → A)
50
+
(h1 : left_inverse v1 u) (h2 : right_inverse v2 u) : v1 = v2 :=
51
+
funext
52
+
(assume x,
53
+
calc
54
+
v1 x = v1 (u (v2 x)) : by rw (h2 x)
55
+
... = v2 x : by rw (h1 (v2 x)))
56
+
57
+
---
58
+
59
+
import data.set
60
+
open function set
61
+
62
+
variables {X Y : Type}
63
+
variable f : X → Y
64
+
variables A B : set X
65
+
66
+
example : f '' (A ∪ B) = f '' A ∪ f '' B :=
67
+
eq_of_subset_of_subset
68
+
(assume y,
69
+
assume h1 : y ∈ f '' (A ∪ B),
70
+
exists.elim h1 $
71
+
assume x h,
72
+
have h2 : x ∈ A ∪ B, from h.left,
73
+
have h3 : f x = y, from h.right,
74
+
or.elim h2
75
+
(assume h4 : x ∈ A,
76
+
have h5 : y ∈ f '' A, from ⟨x, h4, h3⟩,
77
+
show y ∈ f '' A ∪ f '' B, from or.inl h5)
78
+
(assume h4 : x ∈ B,
79
+
have h5 : y ∈ f '' B, from ⟨x, h4, h3⟩,
80
+
show y ∈ f '' A ∪ f '' B, from or.inr h5))
81
+
(assume y,
82
+
assume h2 : y ∈ f '' A ∪ f '' B,
83
+
or.elim h2
84
+
(assume h3 : y ∈ f '' A,
85
+
exists.elim h3 $
86
+
assume x h,
87
+
have h4 : x ∈ A, from h.left,
88
+
have h5 : f x = y, from h.right,
89
+
have h6 : x ∈ A ∪ B, from or.inl h4,
90
+
show y ∈ f '' (A ∪ B), from ⟨x, h6, h5⟩)
91
+
(assume h3 : y ∈ f '' B,
92
+
exists.elim h3 $
93
+
assume x h,
94
+
have h4 : x ∈ B, from h.left,
95
+
have h5 : f x = y, from h.right,
96
+
have h6 : x ∈ A ∪ B, from or.inr h4,
97
+
show y ∈ f '' (A ∪ B), from ⟨x, h6, h5⟩))
98
+
99
+
-- remember, x ∈ A ∩ B is the same as x ∈ A ∧ x ∈ B
100
+
example (x : X) (h1 : x ∈ A) (h2 : x ∈ B) : x ∈ A ∩ B :=
101
+
and.intro h1 h2
102
+
103
+
example (x : X) (h1 : x ∈ A ∩ B) : x ∈ A :=
104
+
and.left h1
105
+
106
+
-- Fill in the proof below.
107
+
-- (It should take about 8 lines.)
108
+
109
+
example : f '' (A ∩ B) ⊆ f '' A ∩ f '' B :=
110
+
assume y,
111
+
assume h1 : y ∈ f '' (A ∩ B),
112
+
show y ∈ f '' A ∩ f '' B, from
113
+
exists.elim h1 $
114
+
assume x h,
115
+
have y ∈ f '' A, from ⟨ x, h.left.left, h.right ⟩,
116
+
have y ∈ f '' B, from ⟨ x, h.left.right, h.right ⟩,
117
+
⟨ ‹ y ∈ f '' A › , ‹ y ∈ f '' B › ⟩
+109
src/ch18.lean
+109
src/ch18.lean
···
1
+
open nat
2
+
3
+
namespace hidden
4
+
5
+
theorem add_distrib (m n k: nat) : m * (n + k) = m * n + m * k :=
6
+
nat.rec_on k
7
+
(show m * (n + 0) = m * n + m * 0, by rw [mul_zero , add_zero, add_zero])
8
+
(assume k,
9
+
assume ih : m * (n + k) = m * n + m * k,
10
+
show m * (n + succ k) = m * n + m * succ k, from calc
11
+
m * (n + succ k) = m * succ (n + k) : by rw add_succ
12
+
... = m * (n + k) + m : by rw mul_succ
13
+
... = m * n + m * k + m : by rw ih
14
+
... = m * n + (m * k + m) : by rw add_assoc
15
+
... = m * n + m * succ k : by rw mul_succ
16
+
)
17
+
18
+
theorem zero_mul (n : nat) : 0 * n = 0 :=
19
+
nat.rec_on n
20
+
(show 0 * 0 = 0, from rfl)
21
+
(assume n,
22
+
assume ih : 0 * n = 0,
23
+
show 0 * succ n = 0, from calc
24
+
0 * succ n = 0 * n + 0 : by rw mul_succ
25
+
... = 0 + 0 : by rw ih
26
+
... = 0 : by rw zero_add)
27
+
28
+
theorem one_mul (n : nat) : 1 * n = n :=
29
+
nat.rec_on n
30
+
(show 1 * 0 = 0, by rw mul_zero)
31
+
(assume n,
32
+
assume ih: 1 * n = n,
33
+
show 1 * succ n = succ n, from calc
34
+
1 * succ n = 1 * n + 1 : by rw mul_succ
35
+
... = n + 1 : by rw ih
36
+
... = succ n : rfl)
37
+
38
+
39
+
theorem mul_assoc (m n k : nat) : m * (n * k) = (m * n) * k :=
40
+
nat.rec_on k
41
+
(show m * (n * 0) = (m * n) * 0, by rw [mul_zero, mul_zero, mul_zero])
42
+
(assume k,
43
+
assume ih : m * (n * k) = (m * n) * k,
44
+
show m * (n * succ k) = (m * n) * succ k, from calc
45
+
m * (n * succ k) = m * (n * k + n) : by rw mul_succ
46
+
... = m * (n * k) + m * n : by rw add_distrib
47
+
... = (m * n) * k + m * n : by rw ih
48
+
... = (m * n) * succ k : by rw mul_succ)
49
+
50
+
theorem mul_comm (m n : nat) : m * n = n * m :=
51
+
nat.rec_on n
52
+
(show m * 0 = 0 * m, by rw [zero_mul,mul_zero])
53
+
(assume n,
54
+
assume ih: m * n = n * m,
55
+
show m * succ n = succ n * m, from calc
56
+
m * succ n = m * n + m : by rw mul_succ
57
+
... = n * m + m : by rw ih
58
+
... = succ n * m : by rw succ_mul)
59
+
60
+
-- END
61
+
end hidden
62
+
63
+
64
+
open nat
65
+
66
+
namespace hidden
67
+
68
+
69
+
-- BEGIN
70
+
theorem T1 : ∀ m n : nat, m > n → (m = n + 1) ∨ (m > n + 1) :=
71
+
assume m n,
72
+
assume h,
73
+
have h1: succ n ≤ m, from succ_le_of_lt h,
74
+
have h2 : n + 1 < m ∨ n + 1 = m, from iff.elim_left le_iff_lt_or_eq h1,
75
+
or.elim h2
76
+
(assume : n + 1 < m,
77
+
show m = n + 1 ∨ m > n + 1, from or.inr this)
78
+
(assume : n + 1 = m,
79
+
have m = n + 1, from eq.symm this,
80
+
show m = n + 1 ∨ m > n + 1, from or.inl this)
81
+
82
+
83
+
theorem T2: ∀ n : nat, n = 0 ∨ n > 0 :=
84
+
assume n,
85
+
have 0 = n ∨ 0 < n, from or.swap $ iff.elim_left le_iff_lt_or_eq $ zero_le n,
86
+
or.elim this
87
+
(assume h1, or.inl (eq.symm h1))
88
+
(assume h1, or.inr h1)
89
+
90
+
91
+
theorem T3 (m n : nat) : n + m = 0 → n = 0 ∧ m = 0 :=
92
+
assume h,
93
+
have h1: n ≥ 0, from zero_le n,
94
+
have h2: m ≥ 0, from zero_le m,
95
+
iff.elim_left (add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg h1 h2) h
96
+
97
+
theorem T4 (n m k : nat) : n * k < m * k → k > 0 ∧ n < m :=
98
+
assume h,
99
+
have h1 : k ≥ 0, from zero_le k,
100
+
have h2 : n < m, from lt_of_mul_lt_mul_right h h1,
101
+
have h3: k ≠ 0, from
102
+
assume : k = 0,
103
+
have n * 0 < m * 0, from (this ▸ h),
104
+
lt_le_antisymm this (zero_le 0),
105
+
have h4: k > 0, from lt_of_le_of_ne h1 h3.symm,
106
+
⟨ h4 , h2 ⟩
107
+
108
+
-- END
109
+
end hidden
+22
src/ch19.lean
+22
src/ch19.lean
···
1
+
import data.int.basic
2
+
3
+
open int
4
+
open nat
5
+
6
+
-- quotient / remainder theorem
7
+
theorem qt : ∀ n m : ℤ, m > 0 → ∃ q r : ℤ, n = m * q + r ∧ (0 ≤ r ∧ r < m) :=
8
+
assume n m h,
9
+
10
+
exists.intro (n / m) $ exists.intro (n % m) $
11
+
12
+
have HH: n = m * (n / m) + (n % m), from calc
13
+
n = n % m + m * (n / m) : by rw [int.mod_add_div]
14
+
... = m * (n / m) + (n % m) : by rw add_comm,
15
+
16
+
have HH1: 0 ≤ (n % m), from int.mod_nonneg n (ne_of_gt h),
17
+
18
+
have HH2: (n % m) < m, from calc
19
+
(n % m) < abs m : int.mod_lt n (ne_of_gt h)
20
+
... = m : abs_of_pos h,
21
+
22
+
⟨ HH , ⟨ HH1 , HH2 ⟩ ⟩
+32
src/ch4.lean
+32
src/ch4.lean
···
1
+
variables A B C D : Prop
2
+
3
+
example : A ∧ (A → B) → B :=
4
+
assume h,
5
+
show B, from h.right h.left
6
+
7
+
8
+
example : A → ¬ (¬ A ∧ B) :=
9
+
assume h1 : A,
10
+
assume h2: ¬ A ∧ B,
11
+
show false, from h2.left h1
12
+
13
+
example : ¬ (A ∧ B) → (A → ¬ B) :=
14
+
λ h1 h2 h3, h1 (⟨ h2 , h3 ⟩)
15
+
16
+
example (h₁ : A ∨ B) (h₂ : A → C) (h₃ : B → D) : C ∨ D :=
17
+
or.elim h₁
18
+
(assume h₄ : A, show C ∨ D, from or.inl (h₂ h₄))
19
+
(assume h₄ : B, show C ∨ D, from or.inr (h₃ h₄))
20
+
21
+
example (h : ¬ A ∧ ¬ B) : ¬ (A ∨ B) :=
22
+
assume h1 : A ∨ B,
23
+
or.elim h1
24
+
(assume h2 : A, show false, from h.left h2)
25
+
(assume h3 : B, show false, from h.right h3)
26
+
27
+
example : ¬ (A ↔ ¬ A) :=
28
+
assume h,
29
+
have h1 : ¬ A, from
30
+
assume a : A,
31
+
show false, from (h.mp a) a,
32
+
show false, from h1 (h.mpr h1)
+49
src/ch5.lean
+49
src/ch5.lean
···
1
+
variables A B : Prop
2
+
open classical
3
+
4
+
example : ¬ A → false → A :=
5
+
sorry
6
+
7
+
example : ¬ A ∨ ¬ B → ¬ (A ∧ B) :=
8
+
assume h,
9
+
show ¬ (A ∧ B), from
10
+
assume h1 : A ∧ B,
11
+
show false, from
12
+
or.elim h
13
+
(assume na : ¬ A,
14
+
show false, from na h1.left)
15
+
(assume nb : ¬ B,
16
+
show false, from nb h1.right)
17
+
18
+
19
+
-- Prove ¬ (A ∧ B) → ¬ A ∨ ¬ B by replacing the sorry's below
20
+
-- by proofs.
21
+
22
+
lemma step1 (h₁ : ¬ (A ∧ B)) (h₂ : A) : ¬ A ∨ ¬ B :=
23
+
have ¬ B, from
24
+
assume b : B,
25
+
show false, from h₁ (and.intro h₂ b),
26
+
show ¬ A ∨ ¬ B, from or.inr this
27
+
28
+
lemma step2 (h₁ : ¬ (A ∧ B)) (h₂ : ¬ (¬ A ∨ ¬ B)) : false :=
29
+
have ¬ A, from
30
+
assume : A,
31
+
have ¬ A ∨ ¬ B, from step1 h₁ ‹A›,
32
+
show false, from h₂ this,
33
+
show false, from h₂ (or.inl this)
34
+
35
+
theorem step3 (h : ¬ (A ∧ B)) : ¬ A ∨ ¬ B :=
36
+
by_contradiction
37
+
(assume h' : ¬ (¬ A ∨ ¬ B),
38
+
show false, from step2 h h')
39
+
40
+
example (h : ¬ B → ¬ A) : A → B :=
41
+
assume a,
42
+
by_contradiction (assume h1 : ¬ B, show false, from h h1 a)
43
+
44
+
example (h : A → B) : ¬ A ∨ B :=
45
+
by_contradiction
46
+
(assume h1 : ¬ (¬ A ∨ B),
47
+
show false, from
48
+
have a : ¬ A, from assume aa : A, show false, from h1 (or.inr (h aa)),
49
+
h1 (or.inl a))
+232
src/ch9.lean
+232
src/ch9.lean
···
1
+
section
2
+
variable A : Type
3
+
variable f : A → A
4
+
variable P : A → Prop
5
+
variable h : ∀ x, P x → P (f x)
6
+
7
+
-- Show the following:
8
+
example : ∀ y, P y → P (f (f y)) :=
9
+
assume x,
10
+
assume h1: P x,
11
+
have h2 : P x → P (f x), from h x,
12
+
have h3: P (f x), from h2 h1,
13
+
have h4 : P (f x) → P (f (f x)), from h (f x),
14
+
show P (f (f x)), from h4 h3
15
+
end
16
+
17
+
section
18
+
variable U : Type
19
+
variables A B : U → Prop
20
+
21
+
example : (∀ x, A x ∧ B x) → ∀ x, A x :=
22
+
assume h : ∀ x, A x ∧ B x,
23
+
assume y,
24
+
have h1 : A y ∧ B y, from h y,
25
+
show A y, from and.left h1
26
+
end
27
+
28
+
---
29
+
30
+
section
31
+
variable U : Type
32
+
variables A B C : U → Prop
33
+
34
+
variable h1 : ∀ x, A x ∨ B x
35
+
variable h2 : ∀ x, A x → C x
36
+
variable h3 : ∀ x, B x → C x
37
+
38
+
example : ∀ x, C x :=
39
+
assume y,
40
+
or.elim (h1 y)
41
+
(assume ha1, show C y, from (h2 y) ha1)
42
+
(assume ha2, show C y, from (h3 y) ha2)
43
+
end
44
+
45
+
---
46
+
47
+
open classical -- not needed, but you can use it
48
+
49
+
-- This is an exercise from Chapter 4. Use it as an axiom here.
50
+
axiom not_iff_not_self (P : Prop) : ¬ (P ↔ ¬ P)
51
+
52
+
example (Q : Prop) : ¬ (Q ↔ ¬ Q) :=
53
+
not_iff_not_self Q
54
+
55
+
section
56
+
variable Person : Type
57
+
variable shaves : Person → Person → Prop
58
+
variable barber : Person
59
+
variable h : ∀ x, shaves barber x ↔ ¬ shaves x x
60
+
61
+
-- Show the following:
62
+
example : false :=
63
+
show false, from
64
+
(not_iff_not_self (shaves barber barber)) (h barber)
65
+
end
66
+
67
+
---
68
+
69
+
section
70
+
variable U : Type
71
+
variables A B : U → Prop
72
+
73
+
example : (∃ x, A x) → ∃ x, A x ∨ B x :=
74
+
assume h,
75
+
exists.elim h
76
+
(assume y (h1 : A y),
77
+
exists.intro y (or.inl h1))
78
+
end
79
+
80
+
---
81
+
82
+
section
83
+
variable U : Type
84
+
variables A B : U → Prop
85
+
86
+
variable h1 : ∀ x, A x → B x
87
+
variable h2 : ∃ x, A x
88
+
89
+
example : ∃ x, B x :=
90
+
exists.elim h2
91
+
(assume y h3,
92
+
exists.intro y (h1 y h3))
93
+
end
94
+
95
+
---
96
+
97
+
variable U : Type
98
+
variables A B C : U → Prop
99
+
100
+
example (h1 : ∃ x, A x ∧ B x) (h2 : ∀ x, B x → C x) :
101
+
∃ x, A x ∧ C x :=
102
+
exists.elim h1
103
+
(assume y h3,
104
+
exists.intro y ⟨ and.left h3, h2 y (and.right h3) ⟩ )
105
+
106
+
---
107
+
108
+
variable U : Type
109
+
variables A B C : U → Prop
110
+
111
+
example : (¬ ∃ x, A x) → ∀ x, ¬ A x :=
112
+
λ h1 y h3, h1 (exists.intro y h3)
113
+
114
+
example : (∀ x, ¬ A x) → ¬ ∃ x, A x :=
115
+
λ h1 h2, exists.elim h2 (λ y h3, h1 y h3)
116
+
117
+
---
118
+
119
+
variable U : Type
120
+
variables R : U → U → Prop
121
+
122
+
example : (∃ x, ∀ y, R x y) → ∀ y, ∃ x, R x y :=
123
+
assume h1 y,
124
+
exists.elim h1
125
+
(assume x (h2 : ∀ x1, R x x1),
126
+
exists.intro x (h2 y))
127
+
128
+
---
129
+
130
+
theorem foo {A : Type} {a b c : A} : a = b → c = b → a = c :=
131
+
assume h1 : a = b,
132
+
assume h2 : c = b,
133
+
show a = c, by rw [h2,h1]
134
+
-- notice that you can now use foo as a rule. The curly braces mean that
135
+
-- you do not have to give A, a, b, or c
136
+
137
+
section
138
+
variable A : Type
139
+
variables a b c : A
140
+
141
+
example (h1 : a = b) (h2 : c = b) : a = c :=
142
+
foo h1 h2
143
+
end
144
+
145
+
section
146
+
variable {A : Type}
147
+
variables {a b c : A}
148
+
149
+
-- replace the sorry with a proof, using foo and rfl, without using eq.symm.
150
+
theorem my_symm (h : b = a) : a = b :=
151
+
have h1 : a = a, from eq.refl a,
152
+
foo h1 h
153
+
154
+
-- now use foo, rfl, and my_symm to prove transitivity
155
+
theorem my_trans (h1 : a = b) (h2 : b = c) : a = c :=
156
+
foo h1 (my_symm h2)
157
+
end
158
+
159
+
---
160
+
161
+
-- these are the axioms for a commutative ring
162
+
163
+
#check @add_assoc
164
+
#check @add_comm
165
+
#check @add_zero
166
+
#check @zero_add
167
+
#check @mul_assoc
168
+
#check @mul_comm
169
+
#check @mul_one
170
+
#check @one_mul
171
+
#check @left_distrib
172
+
#check @right_distrib
173
+
#check @add_left_neg
174
+
#check @add_right_neg
175
+
#check @sub_eq_add_neg
176
+
177
+
variables x y z : int
178
+
179
+
theorem t1 : x - x = 0 :=
180
+
calc
181
+
x - x = x + -x : by rw sub_eq_add_neg
182
+
... = 0 : by rw add_right_neg
183
+
184
+
theorem t2 (h : x + y = x + z) : y = z :=
185
+
calc
186
+
y = 0 + y : by rw zero_add
187
+
... = (-x + x) + y : by rw add_left_neg
188
+
... = -x + (x + y) : by rw add_assoc
189
+
... = -x + (x + z) : by rw h
190
+
... = (-x + x) + z : by rw add_assoc
191
+
... = 0 + z : by rw add_left_neg
192
+
... = z : by rw zero_add
193
+
194
+
theorem t3 (h : x + y = z + y) : x = z :=
195
+
calc
196
+
x = x + 0 : by rw add_zero
197
+
... = x + (y + -y) : by rw add_right_neg
198
+
... = (x + y) + -y : by rw add_assoc
199
+
... = (z + y) + -y : by rw h
200
+
... = z + (y + -y) : by rw add_assoc
201
+
... = z + 0 : by rw add_right_neg
202
+
... = z : by rw add_zero
203
+
204
+
theorem t4 (h : x + y = 0) : x = -y :=
205
+
calc
206
+
x = x + 0 : by rw add_zero
207
+
... = x + (y + -y) : by rw add_right_neg
208
+
... = (x + y) + -y : by rw add_assoc
209
+
... = 0 + -y : by rw h
210
+
... = -y : by rw zero_add
211
+
212
+
theorem t5 : x * 0 = 0 :=
213
+
have h1 : x * 0 + x * 0 = x * 0 + 0, from
214
+
calc
215
+
x * 0 + x * 0 = x * (0 + 0) : by rw left_distrib
216
+
... = x * 0 : by rw add_zero
217
+
... = x * 0 + 0 : by rw add_zero,
218
+
show x * 0 = 0, from t2 _ _ _ h1
219
+
220
+
theorem t6 : x * (-y) = -(x * y) :=
221
+
have h1 : x * (-y) + x * y = 0, from
222
+
calc
223
+
x * (-y) + x * y = x * (-y + y) : by rw left_distrib
224
+
... = x * 0 : by rw add_left_neg
225
+
... = 0 : by rw t5 x,
226
+
show x * (-y) = -(x * y), from t4 _ _ h1
227
+
228
+
theorem t7 : x + x = 2 * x :=
229
+
calc
230
+
x + x = 1 * x + 1 * x : by rw one_mul
231
+
... = (1 + 1) * x : by rw right_distrib
232
+
... = 2 * x : rfl