Skip to content

Commit 2d6dc1f

Browse files
mfornetmfornet
committed
close few more sorries
1 parent f3a22cc commit 2d6dc1f

File tree

1 file changed

+75
-20
lines changed

1 file changed

+75
-20
lines changed

‎HumanEvalLean/HumanEval75.lean‎

Lines changed: 75 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -61,7 +61,13 @@ example : isMultiplyPrime (9 * 9 * 9) = false := by native_decide
6161
example : isMultiplyPrime (11 * 9 * 9) = false := by native_decide
6262
example : isMultiplyPrime (11 * 13 * 7) = true := by native_decide
6363

64-
theorem Nat.isPrime_ne_zero (hp : Nat.IsPrime p) : p ≠ 0 := by sorry
64+
theorem Nat.isPrime_ne_zero (hp : Nat.IsPrime p) : p ≠ 0 := by
65+
intro h
66+
have h2 : 2 ∣ p := by simp [h]
67+
apply Or.elim (hp.right 2 h2)
68+
trivial
69+
rw [h]
70+
trivial
6571

6672
def IsMultiplyPrimeIff (solution : Nat → Bool) : Prop :=
6773
(a : Nat) → solution a ↔ ∃ (p₁ p₂ p₃ : Nat), p₁ * p₂ * p₃ = a ∧ Nat.IsPrime p₁ ∧ Nat.IsPrime p₂ ∧ Nat.IsPrime p₃
@@ -70,7 +76,17 @@ def IsMultiplyPrimeIff (solution : Nat → Bool) : Prop :=
7076
def List.prod {α} [Mul α] [One α] : List α → α :=
7177
List.foldr (· * ·) 1
7278

73-
theorem List.prod_ne_zero {α} [Mul α] [One α] [Zero α] (l : List α) (h : ∀ x ∈ l, x ≠ 0) : l.prod ≠ 0 := by sorry
79+
theorem List.prod_head_eq_mul {α} [Mul α] [One α] (a : α) (l : List α) : (a :: l).prod = a * l.prod := by
80+
simp [List.prod]
81+
82+
theorem List.prod_ne_zero {α} [Mul α] [One α] [Zero α] (l : List α) (h : ∀ x ∈ l, x ≠ 0) : l.prod ≠ 0 := by
83+
induction l with
84+
| nil =>
85+
simp [List.prod]
86+
intro h
87+
sorry
88+
| cons x xs ih =>
89+
sorry
7490

7591
theorem List.prod_nil {α} [Mul α] [One α] : ([] : List α).prod = 1 :=
7692
rfl
@@ -84,16 +100,26 @@ structure PrimeDecomposition (n : Nat) where
84100
def PrimeDecomposition.length (d : PrimeDecomposition n) : Nat := d.ps.length
85101

86102
def PrimeDecomposition.push (d : PrimeDecomposition n) (p : Nat) (hp : p.IsPrime) : PrimeDecomposition (n * p) :=
87-
⟨p :: d.ps, by sorry, by sorry⟩
103+
⟨p :: d.ps,
104+
by
105+
intro p1 h
106+
simp at h
107+
apply Or.elim h
108+
· intro t; rw[t]; exact hp
109+
· exact (d.all_prime p1 ·),
110+
by
111+
simp [List.prod_head_eq_mul]
112+
rw [d.is_decomposition, Nat.mul_comm]
113+
⟩
88114

89115
def PrimeDecomposition.erase (d : PrimeDecomposition n) (p : Nat) (hp : p.IsPrime) (hd : p ∣ n) : PrimeDecomposition (n / p) :=
90116
⟨d.ps.erase p, by sorry, by sorry⟩
91117

92-
theorem PrimeDecomposition.push_length_eq_length_plus_one (d : PrimeDecomposition n) (p : Nat) (hp : p.IsPrime) : (d.push p hp).length = d.length + 1 := by sorry
93-
94-
theorem PrimeDecomposition.push_simp {d : PrimeDecomposition n} : (d.push p hp).length = d.length + 1 := by sorry
118+
theorem PrimeDecomposition.push_length_eq_length_plus_one {d : PrimeDecomposition n} : (d.push p hp).length = d.length + 1 := by
119+
simp [PrimeDecomposition.push, PrimeDecomposition.length]
95120

96-
theorem PrimeDecomposition.erase_length_eq_length_minus_one (d : PrimeDecomposition n) (p : Nat) (hp : p.IsPrime) (hd : p ∣ n) : (d.erase p hp hd).length = d.length - 1 := by sorry
121+
theorem PrimeDecomposition.erase_length_eq_length_minus_one (d : PrimeDecomposition n) (p : Nat) (hp : p.IsPrime) (hd : p ∣ n) : (d.erase p hp hd).length = d.length - 1 := by
122+
sorry
97123

98124
def PrimeDecomposition.one : PrimeDecomposition 1 := ⟨[], by simp, (by simp [List.prod_nil])⟩
99125

@@ -105,11 +131,14 @@ theorem PrimeDecomposition.zero_does_not_exist (d : PrimeDecomposition 0) : Fals
105131

106132
theorem PrimeDecomposition.one_unique (d : PrimeDecomposition 1) : d = PrimeDecomposition.one := by
107133
simp [PrimeDecomposition.one]
108-
sorry
109-
110-
theorem PrimeDecomposition.length_eq_zero_iff (n : Nat) (d : PrimeDecomposition n) : d.length = 0 ↔ n = 1 := by sorry
134+
if h : d.ps = [] then
135+
sorry
136+
else
137+
sorry
111138

112-
theorem PrimeDecomposition.one_length_eq_zero (d : PrimeDecomposition 1) : d.length = 0 := by sorry
139+
theorem PrimeDecomposition.one_length_eq_zero (d : PrimeDecomposition 1) : d.length = 0 := by
140+
rw [PrimeDecomposition.one_unique d]
141+
simp [PrimeDecomposition.length, PrimeDecomposition.one]
113142

114143
theorem isMultipleOfKPrimes_primeDecompositionLength {n k : Nat} :
115144
isMultipleOfKPrimes n k ↔ ∃ (d : PrimeDecomposition n), d.length = k := by
@@ -123,34 +152,60 @@ theorem isMultipleOfKPrimes_primeDecompositionLength {n k : Nat} :
123152
simp [hn₀]
124153
if hk : k = 0 then
125154
simp [hk]
126-
sorry
155+
constructor
156+
· intro h1
157+
rw [h1]
158+
exact ⟨PrimeDecomposition.one, by simp [PrimeDecomposition.one_length_eq_zero]⟩
159+
· intro ⟨d, hd⟩
160+
simp [PrimeDecomposition.length] at hd
161+
symm
162+
let x := d.is_decomposition
163+
simp [hd, List.prod] at x
164+
trivial
127165
else
128166
simp [hk]
129167
constructor
130168
· intro ⟨hn₁, hrec⟩
131169
let ⟨d, hd⟩ := isMultipleOfKPrimes_primeDecompositionLength.mp hrec
132-
have hn_ge_1 : 1 < n := by sorry
170+
have hn_ge_1 : 1 < n := by match n with
171+
| 0 => trivial
172+
| 1 => trivial
173+
| n + 2 => simp
133174
let d₁ := d.push (smallestPrimeFactor n) (smallestPrimeFactor_isPrime hn_ge_1)
134175
rw [← Nat.div_mul_cancel (smallestPrimeFactor_div_n n hn_ge_1)]
135176
suffices d₁.length = k by
136177
exact ⟨d₁, by simp [this]⟩
137-
let x := PrimeDecomposition.push_length_eq_length_plus_one d (smallestPrimeFactor n) (smallestPrimeFactor_isPrime hn_ge_1)
138-
rw [x, hd]
178+
rw [PrimeDecomposition.push_length_eq_length_plus_one, hd]
139179
have hk₀ : 1 ≤ k := by match k with
140180
| 0 => contradiction
141181
| k + 1 => simp
142182
rw [← Nat.sub_add_comm hk₀, Nat.add_sub_cancel]
143183
· intro ⟨d, hd⟩
144-
have hn_ge_1 : 1 < n := by sorry
184+
have hn_ge_1 : 1 < n := by match n with
185+
| 0 => trivial
186+
| 1 =>
187+
exfalso
188+
rw [PrimeDecomposition.one_length_eq_zero d] at hd
189+
symm at hd
190+
contradiction
191+
| n + 2 => simp
145192
constructor
146-
· sorry
147-
· let d2 := d.erase (smallestPrimeFactor n) (by sorry) (by sorry)
193+
· intro h1
194+
revert hd d
195+
rw [h1]
196+
intro d hd
197+
rw [PrimeDecomposition.one_length_eq_zero d] at hd
198+
symm at hd
199+
contradiction
200+
· let d2 := d.erase (smallestPrimeFactor n) (smallestPrimeFactor_isPrime hn_ge_1) (smallestPrimeFactor_div_n n hn_ge_1)
148201
suffices d2.length = k - 1 by
149202
exact isMultipleOfKPrimes_primeDecompositionLength.mpr ⟨d2, by simp [this]⟩
150203
let x := PrimeDecomposition.erase_length_eq_length_minus_one d (smallestPrimeFactor n) (smallestPrimeFactor_isPrime hn_ge_1) (smallestPrimeFactor_div_n n hn_ge_1)
151204
rw [x, hd]
152205

153-
theorem List.prod_3_mul {a b c : Nat} : [a, b, c].prod = a * b * c := by sorry
206+
theorem List.prod_3_mul {a b c : Nat} : [a, b, c].prod = a * b * c := by
207+
simp [List.prod]
208+
rw [Nat.mul_assoc]
154209

155210
theorem primeDecomposition_length_3 (n : Nat) :
156211
(∃ (p₁ p₂ p₃ : Nat), p₁ * p₂ * p₃ = n ∧ Nat.IsPrime p₁ ∧ Nat.IsPrime p₂ ∧ Nat.IsPrime p₃)
@@ -167,7 +222,7 @@ theorem primeDecomposition_length_3 (n : Nat) :
167222
suffices d.length = 3 by
168223
exact ⟨d, this⟩
169224

170-
repeat rw [PrimeDecomposition.push_simp]
225+
repeat rw [PrimeDecomposition.push_length_eq_length_plus_one]
171226
rw [PrimeDecomposition.one_length_eq_zero]
172227
· intro ⟨⟨ps, hp, ha⟩, hd⟩
173228
simp [PrimeDecomposition.length] at hd

0 commit comments

Comments
 (0)
⚡