forked from ImperialCollegeLondon/M40001_lean
-
Notifications
You must be signed in to change notification settings - Fork 0
/
sheet4.lean
209 lines (158 loc) · 4.33 KB
/
sheet4.lean
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
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
/- Math40001 : Introduction to university mathematics.
Problem Sheet 4, October 2019.
This is a Lean file. It can be read with the Lean theorem prover.
You can work on this file online at
https://tinyurl.com/Lean-M40001-Example-Sheet-4
or you can install Lean and its maths library following the
instructions at
https://github.com/leanprover-community/mathlib#installation
There are advantages to installing Lean on your own computer
(for example it's faster), but it's more hassle than
just using it online.
In the below, delete "sorry" and replace it with some
tactics which prove the result.
-/
import data.real.basic -- the real numbers
/- Question 1.
For each of the sets~$X$ and binary relations~$R$ below, figure out whether~$R$ is (a) reflexive, (b) symmetric, (c) antisymmetric, (d) transitive.
\begin{enumerate}
\item Let $X$ be the set $\{1,2\}$ and define~$R$ like this: $R(1,1)$ is true, $R(1,2)$ is true, $R(2,1)$ is true and $R(2,2)$ is false.
\item Let~$X=\R$ and define $R(a,b)$ to be the proposition $a=-b$.
\item Let~$X=\R$ and define $R(a,b)$ to be false for all real numbers~$a$ and~$b$.
\item Let~$X$ be the empty set and define~$R$ to be the empty binary relation (we don't have to say what its value is on any pair $(a,b)$ because no such pairs exist).
\end{enumerate}
-/
namespace Q1a
inductive X : Type
| one : X
| two : X
namespace X
def R : X → X → Prop
| one one := true
| one two := true
| two one := true
| two two := false
-- insert "¬" if you think it's not reflexive
lemma Q1a_refl : reflexive R :=
begin
sorry
end
-- insert "¬" if you think it's not symmetric
lemma Q1a_symm : symmetric R :=
begin
sorry
end
-- insert "¬" if you think it's not transitive
lemma Q1a_trans : transitive R :=
begin
sorry
end
-- insert "¬" if you think it's not an equiv reln
lemma Q1a_equiv : equivalence R :=
begin
sorry
end
end X
end Q1a
namespace Q1b
def R (a b : ℝ) : Prop := a = -b
-- insert "¬" if you think it's not reflexive
lemma Q1b_refl : reflexive R :=
begin
sorry
end
-- insert "¬" if you think it's not symmetric
lemma Q1b_symm : symmetric R :=
begin
sorry
end
-- insert "¬" if you think it's not transitive
lemma Q1b_trans : transitive R :=
begin
sorry
end
-- insert "¬" if you think it's not an equiv reln
lemma Q1b_equiv : equivalence R :=
begin
sorry
end
end Q1b
namespace Q1c
def R (a b : ℝ) : Prop := false
-- insert "¬" if you think it's not reflexive
lemma Q1c_refl : reflexive R :=
begin
sorry
end
-- insert "¬" if you think it's not symmetric
lemma Q1c_symm : symmetric R :=
begin
sorry
end
-- insert "¬" if you think it's not transitive
lemma Q1c_trans : transitive R :=
begin
sorry
end
-- insert "¬" if you think it's not an equiv reln
lemma Q1c_equiv : equivalence R :=
begin
sorry
end
end Q1c
namespace Q1d
def R (a b : empty) : Prop := by cases a -- i.e. "I'll define it in all cases -- oh look there are no cases"
-- insert "¬" if you think it's not reflexive
lemma Q1d_refl : reflexive R :=
begin
sorry
end
-- insert "¬" if you think it's not symmetric
lemma Q1d_symm : symmetric R :=
begin
sorry
end
-- insert "¬" if you think it's not transitive
lemma Q1d_trans : transitive R :=
begin
sorry
end
-- insert "¬" if you think it's not an equiv reln
lemma Q1d_equiv : equivalence R :=
begin
sorry
end
end Q1d
-- `set ℤ` is the type of subsets of the integers.
def Q2a : partial_order (set ℤ) :=
{ le := λ A B, A ⊆ B,
le_refl := begin sorry end,
le_antisymm := begin sorry end,
le_trans := begin sorry end
}
-- insert ¬ at the beginning if you think it's wrong
lemma Q2b : is_total (set ℤ) (λ A B, A ⊆ B) :=
begin
sorry
end
-- put ¬ in front if you think it's wrong
lemma Q3a : symmetric (λ a b : ℝ, a < b) :=
begin
sorry
end
-- put ¬ in front if you think it's wrong
lemma Q3b : symmetric (λ a b : (∅ : set ℝ), a < b) :=
begin
sorry
end
-- type in the proof in the question. Where do you get stuck?
lemma Q4 (X : Type) (R : X → (X → Prop)) (hs : symmetric R) (ht : transitive R) : reflexive R :=
begin
sorry
end
open function
definition pals {X Y Z : Type} (f : X → Y) (g : X → Z) := ∃ h : Y → Z, bijective h ∧ g = h ∘ f
lemma Q5 (X Y Z: Type) (f : X → Y) (g : X → Z) (hf : surjective f) (hg : surjective g) : pals f g ↔ ∀ a b : X, (f a = f b) ↔ (g a = g b) :=
begin
sorry
end