Skip to content

Commit 0a4f768

Browse files
datokratdatokrat
authored
73 (#280)
This PR solves problem 73 and improves efficiency of 72.
1 parent 5e892ba commit 0a4f768

File tree

2 files changed

+242
-13
lines changed

2 files changed

+242
-13
lines changed

‎HumanEvalLean/HumanEval72.lean‎

Lines changed: 14 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -43,40 +43,44 @@ instance decidableBallLTImpl (n : Nat) (P : ∀ k, k < n → Prop) [∀ n h, Dec
4343

4444
attribute [- instance] Nat.decidableBallLT
4545

46+
theorem Array.ext_getElem_iff {l₁ l₂ : Array α} :
47+
l₁ = l₂ ↔ l₁.size = l₂.size ∧ ∀ (i : Nat) (h₁ : i < l₁.size) (h₂ : i < l₂.size), l₁[i]'h₁ = l₂[i]'h₂ := by
48+
simp [← Array.toList_inj, List.ext_getElem_iff]
49+
4650
/-!
4751
## Implementation
4852
-/
4953

5054
/--
5155
Efficient, short-circuiting
5256
-/
53-
def willItFly (q : List Nat) (w : Nat) : Bool :=
54-
q.sum ≤ w ∧ ∀ (i : Nat) (hi : i < q.length / 2), q[i] = q[q.length - 1 - i]
57+
def willItFly (q : Array Nat) (w : Nat) : Bool :=
58+
q.sum ≤ w ∧ ∀ (i : Nat) (hi : i < q.size / 2), q[i] = q[q.size - 1 - i]
5559

5660
/-!
5761
## Tests
5862
-/
5963

6064
set_option cbv.warning false
6165

62-
example : willItFly [3, 2, 3] 9 = true := by cbv
63-
example : willItFly [1, 2] 5 = false := by cbv
64-
example : willItFly [3] 5 = true := by cbv
65-
example : willItFly [3, 2, 3] 1 = false := by cbv
66-
example : willItFly [1, 2, 3] 6 = false := by cbv
67-
example : willItFly [5] 5 = true := by cbv
66+
example : willItFly #[3, 2, 3] 9 = true := by cbv
67+
example : willItFly #[1, 2] 5 = false := by cbv
68+
example : willItFly #[3] 5 = true := by cbv
69+
example : willItFly #[3, 2, 3] 1 = false := by cbv
70+
example : willItFly #[1, 2, 3] 6 = false := by cbv
71+
example : willItFly #[5] 5 = true := by cbv
6872

6973
/-!
7074
## Verification
7175
-/
7276

7377
theorem willItFly_iff_le_and_forall :
74-
willItFly q w ↔ q.sum ≤ w ∧ ∀ (i : Nat) (hi : i < q.length), q[i] = q[q.length - 1 - i] := by
78+
willItFly q w ↔ q.sum ≤ w ∧ ∀ (i : Nat) (hi : i < q.size), q[i] = q[q.size - 1 - i] := by
7579
grind [willItFly]
7680

7781
theorem willItFly_iff_le_and_reverse_eq_self :
7882
willItFly q w ↔ q.sum ≤ w ∧ q.reverse = q := by
79-
rw [List.ext_getElem_iff]
83+
rw [Array.ext_getElem_iff]
8084
grind [willItFly]
8185

8286
/-!

‎HumanEvalLean/HumanEval73.lean‎

Lines changed: 228 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,232 @@
11
module
22

3-
def smallest_change : Unit :=
4-
()
3+
public import Std
4+
import all Init.Data.Range.Polymorphic.UpwardEnumerable
5+
public meta import Lean -- TODO
6+
open Std
7+
8+
/-! ## Implementation -/
9+
10+
public section
11+
12+
instance : PRange.Least? (Fin n) where
13+
least? := if h : 0 < n then some ⟨0, by grind⟩ else none
14+
15+
instance : PRange.LawfulUpwardEnumerableLeast? (Fin n) where
16+
least?_le x := ⟨⟨0, by grind [x.isLt]⟩, by
17+
simp [PRange.least?, PRange.UpwardEnumerable.LE]
18+
constructor
19+
· grind [x.isLt]
20+
· refine ⟨x.val, by grind⟩⟩
21+
22+
def smallestChange (xs : Array Nat) : Nat :=
23+
(*...* : Rii (Fin (xs.size / 2))).iter.filter (fun i => xs[i.val] ≠ xs[xs.size - 1 - i.val]) |>.length
24+
25+
/-! ## Tests -/
26+
27+
example : smallestChange #[1,2,3,5,4,7,9,6] = 4 := by native_decide
28+
example : smallestChange #[1, 2, 3, 4, 3, 2, 2] = 1 := by native_decide
29+
example : smallestChange #[1, 4, 2] = 1 := by native_decide
30+
example : smallestChange #[1, 4, 4, 2] = 1 := by native_decide
31+
example : smallestChange #[1, 2, 3, 2, 1] = 0 := by native_decide
32+
example : smallestChange #[3, 1, 1, 3] = 0 := by native_decide
33+
example : smallestChange #[1] = 0 := by native_decide
34+
example : smallestChange #[0, 1] = 1 := by native_decide
35+
36+
/-! ## Missing API -/
37+
38+
theorem Vector.ext_getElem_iff {l₁ l₂ : Vector α n} :
39+
l₁ = l₂ ↔ ∀ (i : Nat) (h₁ : i < n) (h₂ : i < n), l₁[i]'h₁ = l₂[i]'h₂ := by
40+
simp [← Vector.toList_inj, List.ext_getElem_iff]
41+
42+
@[simp, grind =]
43+
theorem Fin.size_rii :
44+
(*...* : Rii (Fin n)).size = n := by
45+
simp only [Rii.size, PRange.least?, Rxi.HasSize.size]
46+
grind
47+
48+
attribute [grind =] Rii.length_toList
49+
50+
@[simp, grind =]
51+
theorem Fin.length_toList_rii :
52+
(*...* : Rii (Fin n)).size = n := by
53+
grind
54+
55+
attribute [grind .] Rii.mem Rii.mem_toList Rii.nodup_toList
56+
57+
theorem List.filter_false {xs : List α} :
58+
xs.filter (fun _ => false) = [] := by
59+
simp
60+
61+
theorem List.Nodup.countP_le_countP_add_one {xs : List α} (h : xs.Nodup)
62+
(h' : ∀ b ∈ xs, b = a ∨ p b = q b) :
63+
xs.countP p ≤ xs.countP q + 1 := by
64+
open Classical in
65+
have : xs.countP p ≤ (xs.erase a).countP p + 1 := by
66+
have := (xs.filter p).le_length_erase (a := a)
67+
grind
68+
have : (xs.erase a).countP p = (xs.erase a).countP q := by
69+
apply List.countP_congr
70+
grind
71+
have : (xs.erase a).countP q ≤ xs.countP q := by
72+
apply List.Sublist.countP_le
73+
apply List.erase_sublist
74+
grind
75+
76+
@[grind .]
77+
theorem List.Nodup.map (f : α → β) (h : ∀ a b : α, ¬ a = b → ¬ (f a) = (f b))
78+
(p : Nodup l) : Nodup (map f l) := by
79+
simp only [nodup_iff_pairwise_ne, ne_eq] at p ⊢
80+
exact Pairwise.map f h p
81+
82+
@[grind ←] theorem List.Nodup.filter (p : α → Bool) : Nodup l → Nodup (filter p l) :=
83+
Pairwise.sublist filter_sublist
84+
85+
theorem Array.getElem!_set {xs : Array Nat} {h} :
86+
(xs.set i v h)[j]! = if j = i then v else xs[j]! := by
87+
grind
88+
89+
theorem Fin.map_val_toList_roi {n : Nat} (m : Fin n) :
90+
(m<...* : Roi (Fin n)).toList.map (·.val) = (m.val<...n).toList := by
91+
induction h : n - m.val generalizing m
92+
· grind
93+
· rename_i ih
94+
have : m.val < n := by grind
95+
rw [Roi.toList_eq_match]
96+
split
97+
· simp only [List.map_nil, List.nil_eq, Nat.toList_roo_eq_nil_iff] at *
98+
grind
99+
· specialize ih ⟨m + 1, by grind⟩
100+
rw [Nat.toList_roo_eq_cons, ← ih] <;> grind
101+
102+
theorem Fin.map_val_toList_rci {n : Nat} (m : Fin n) :
103+
(m...* : Rci (Fin n)).toList.map (·.val) = (m.val...n).toList := by
104+
induction h : n - m.val generalizing m
105+
· grind
106+
· rename_i ih
107+
have : m.val < n := by grind
108+
rw [Rci.toList_eq_toList_roi, List.map_cons, Fin.map_val_toList_roi, Nat.toList_rco_eq_cons (by grind)]
109+
simp [Nat.toList_roo_eq_toList_rco]
110+
111+
theorem Fin.map_val_toList_rii {n : Nat} :
112+
(*...* : Rii (Fin n)).toList.map (·.val) = (*...n).toList := by
113+
simp only [Rii.toList_eq_match_rci, PRange.least?, Rio.toList_eq_match_rco]
114+
split
115+
· grind [Nat.toList_rco_eq_nil_iff]
116+
· grind [map_val_toList_rci]
117+
118+
/-! ## Verification -/
119+
120+
def IsPalindrome (xs : Vector Nat n) := xs.reverse = xs
121+
122+
theorem getElem_foldl_set {changes : List (Fin n × α)} {v : Vector α n}
123+
(h_nodup : (changes.map Prod.fst).Nodup) {j : Nat} (hj : j < n) :
124+
(changes.foldl (fun v' (i, x) => v'.set i x) v)[j] =
125+
match changes.find? (·.1.val == j) with
126+
| some (_, x) => x
127+
| none => v[j] := by
128+
rw [← List.reverse_reverse (as := changes)] at h_nodup ⊢
129+
generalize changes.reverse = revChanges at ⊢ h_nodup
130+
induction revChanges
131+
· simp
132+
· rename_i c cs ih
133+
simp only [List.foldl_reverse] at ih
134+
simp only [List.reverse_cons, List.foldl_append, List.foldl_reverse, List.foldl_cons,
135+
List.foldl_nil]
136+
rw [Vector.getElem_set, ih]
137+
split
138+
· split
139+
· simp only [List.reverse_cons, List.map_append] at h_nodup
140+
rw [List.nodup_append] at h_nodup
141+
replace h_nodup := h_nodup.2.2 c.fst
142+
grind
143+
· grind
144+
· grind
145+
· grind
146+
147+
/--
148+
First direction of the characterization:
149+
150+
There is a finite sequence of modifications that transforms `xs` into a palindrome, and the sequence
151+
consists of exactly `smallestChange xs` modifications..
152+
-/
153+
theorem exists_isPalindrome {xs : Array Nat} :
154+
∃ changes : List (Fin xs.size × Nat), changes.length = smallestChange xs ∧
155+
IsPalindrome (changes.foldl (fun xs' (i, v) => xs'.set i.val v) xs.toVector) := by
156+
refine ⟨(*...* : Rii (Fin (xs.size / 2))).iter.filter (fun i => xs[i.val] ≠ xs[xs.size - 1 - i.val]) |>.map (fun i => (⟨i.val, by grind⟩, xs[xs.size - 1 - i.val])) |>.toList, ?_⟩
157+
constructor
158+
· simp [smallestChange, ← Iter.length_toList_eq_length]
159+
· rw [IsPalindrome, Vector.ext_getElem_iff]
160+
intro i h₁ h₂
161+
simp only [Iter.toList_map, Iter.toList_filter, Rii.toList_iter, Vector.getElem_reverse]
162+
rw [getElem_foldl_set (by grind), getElem_foldl_set (by grind)]
163+
simp only [List.find?_map, Vector.getElem_mk]
164+
split <;> split
165+
· grind
166+
· grind [Option.map_eq_some_iff]
167+
· grind [Option.map_eq_some_iff]
168+
· simp only [Option.map_eq_none_iff, List.find?_eq_none] at *
169+
rename_i heq heq'
170+
match hcmp : compare i (xs.size - 1 - i) with
171+
| .lt =>
172+
specialize heq ⟨i, by grind⟩
173+
grind
174+
| .eq => grind
175+
| .gt =>
176+
specialize heq' ⟨xs.size - 1 - i, by grind⟩
177+
grind
178+
179+
/--
180+
An alternative, less efficient implementation of `smallestChange` that does not use `Fin`.
181+
It is less dependently typed and therefore lends itself better to verification.
182+
-/
183+
private def smallestChangeAux (xs : Array Nat) : Nat :=
184+
(*...(xs.size / 2)).iter.filter (fun i => xs[i]! ≠ xs[xs.size - 1 - i]!) |>.length
185+
186+
private theorem smallChange_eq_smallChangeAux {xs : Array Nat} :
187+
smallestChange xs = smallestChangeAux xs := by
188+
simp only [smallestChange, ← Iter.length_toList_eq_length, smallestChangeAux,
189+
Iter.toList_filter, Rii.toList_iter, Rio.toList_iter, ← Fin.map_val_toList_rii,
190+
List.filter_map, Function.comp_def]
191+
grind
192+
193+
/--
194+
Second part of the verification:
195+
196+
In order to transform `xs` into a palindrome, one needs at least `smallestChange xs` modifications.
197+
-/
198+
theorem smallestChange_le {xs : Array Nat} {changes : List (Fin xs.size × Nat)}
199+
(h : IsPalindrome (changes.foldl (fun xs' (i, v) => xs'.set i.val v) xs.toVector)) :
200+
smallestChange xs ≤ changes.length := by
201+
suffices ∀ ys : Vector Nat xs.size,
202+
IsPalindrome (changes.foldl (fun xs' (i, v) => xs'.set i.val v) ys) →
203+
(List.filter (fun i => !decide (ys.toArray[i]! = ys.toArray[ys.toArray.size - 1 - i]!))
204+
(*...ys.toArray.size / 2).iter.toList).length ≤ changes.length by
205+
rw [smallChange_eq_smallChangeAux, smallestChangeAux]
206+
simp only [ne_eq, decide_not, ← Iter.length_toList_eq_length, Iter.toList_filter]
207+
grind
208+
clear h
209+
intro ys h
210+
induction changes generalizing ys
211+
· simp only [Rio.toList_iter, List.length_nil, Nat.le_zero_eq, List.length_eq_zero_iff,
212+
List.filter_eq_nil_iff]
213+
intro a ha
214+
simp only [Rio.mem_toList_iff_mem, Rio.mem_iff] at ha
215+
grind [Vector.cast_mk, IsPalindrome, List.reverse_nil, Vector.reverse_mk, List.filter_false]
216+
· rename_i c cs ih
217+
specialize ih _ h
218+
simp only [List.foldl_cons] at h
219+
replace ih := Nat.add_le_add_right ih 1
220+
refine le_trans ?_ ih
221+
simp only [← List.countP_eq_length_filter, Vector.size_toArray]
222+
apply List.Nodup.countP_le_countP_add_one (a := min c.fst.val (xs.size - 1 - c.fst.val))
223+
· apply Rio.nodup_toList
224+
· intro b hb
225+
simp only [Vector.toArray_set, Array.getElem!_set]
226+
simp only [Rio.toList_iter, Rio.mem_toList_iff_mem, Rio.mem_iff] at hb
227+
split
228+
· grind
229+
· grind
5230

6231
/-!
7232
## Prompt
@@ -49,4 +274,4 @@ def check(candidate):
49274
assert candidate([0, 1]) == 1
50275
51276
```
52-
-/
277+
-/

0 commit comments

Comments
 (0)
⚡