-
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
import Std.Tactic.Do
import Mathlib
open Std.Do
/-
# Pset 3
## 3.1
Prove the following lemma.
-/
lemma bounded_by_reciprocals (x : ℝ) (hx : 0 ≤ x) (h : ∀ n, x ≤ 1 / n) : x = 0 := by
sorry
/-
## 3.2
Prove the following lemmas.
-/
lemma imo1964_p1b (n : ℕ) : (2 ^ n + 1) % 7 ≠ 0 := by
sorry
abbrev SolutionSet : Set <| Vector ℕ 14 := sorry
lemma usa1979_p1 : ∀ e, e ∈ SolutionSet ↔ (e.map (· ^ 4)).sum = 1599 := by
sorry
/-
## 3.3
Here's a weird sorting algorithm:
-/
namespace Sorting
variable [LinearOrder α] (A : Array α)
def ICan'tBelieveItCanSort := Id.run do
let N := A.size
let mut A := A.toVector
for hi : i in [:N] do
for hj : j in [:N] do
if A[i] < A[j] then
A := A.swap i j
return A.toArray
#eval ICan'tBelieveItCanSort #[69, 420, 1, 1, 13, 1, 65536]
/-
First, write a natural language proof for why this algorithm is correct.
Next, prove in Lean that the algorithm returns a permutation of its input.
-/
theorem perm : ICan'tBelieveItCanSort A |>.Perm A := by
generalize h : ICan'tBelieveItCanSort A = x
apply Id.of_wp_run_eq h
mvcgen
sorry
/-
Now for the fun part!
-/
theorem sorted : ICan'tBelieveItCanSort A |>.Pairwise (· ≤ ·) := by
generalize h : ICan'tBelieveItCanSort A = x
apply Id.of_wp_run_eq h
mvcgen
sorry
/-
Now we can declare victory!
-/
theorem ICan'tBelieveICanProveItCanSort : (ICan'tBelieveItCanSort A).Perm A
∧ (ICan'tBelieveItCanSort A).Pairwise (· ≤ ·) :=
⟨perm A, sorted A⟩
end Sorting
/-
## 3.4
Implement the function below that returns `42` if the input string is `"lean"` and otherwise leaves it unchanged. Since the type of this function is pretty complicated, we'll implement it using tactics mode, which isn't just for proofs!
-/
def leanTo42Type (x : String) : Type :=
if x = "lean" then ℕ else String
def leanTo42 (x : String) : leanTo42Type x := by
sorry
/-
## 3.5
Prove the following lemma.
-/
lemma crazy_lemma [DecidableEq β] {A : Finset α} {g : α → Finset β}
(hin : ∀ y, x ∈ g y → g (f y) ⊂ g y)
(hnin : ∀ y, x ∉ g y → g (f y) = g y)
(hf : ∀ y, x ∉ g (f y))
(hA : ∃ a ∈ A, x ∈ g a)
: (A.map f).biUnion g ⊂ A.biUnion g :=
sorry
/-
## 3.6
Implement these functions by looking carefully at the type signatures of what you're given.
-/
def yoneda (f : Type u → Type v) [Functor f] (g : {β : Type u} → (α → β) → f β) : f α :=
sorry
def yoneda' (f : Type u → Type v) [Functor f] (y : f α) : {β : Type u} → (α → β) → f β :=
sorry
/-
## 3.7
-/
/-
## 3.8
-/
/-
## 3.9
-/
def solution : String := sorry
open Nat Real Quaternion CoxeterMatrix Lean in
example : minFac '⓫'.toNat|>λ_11↦(·+97)<$>[0/0,_11,-(⟨1,0,2,4⟩:ℍ[ℤ])^2|>.re.toNat,defaultMaxRecDepth%101,catalan 4,_11,(φ∘φ∘φ∘φ∘φ∘φ<|4‼‼)!,↑((4:Fin 24)-6),⌈deriv (sin ·^69) π⌉₊,_11,Nat.card<|Aₙ 2|>.Group]
= solution.toList.map Char.toNat := by
sorry
/-
## 3.10
fenwick
-/
namespace Fenwick
end Fenwick