Submission Details
Challenge: twoSum
Submitted by: Nangos
Submitted at: 2026-02-10 07:12:30
Code:
def twoSum (nums : Array Int) (target : Int) : Option (Nat × Nat)import Std.Data.HashMap
open Std
/-- The `i`-th iteration of `twoSum`,
pairing `nums[i]` with all previous elements stored in `map`. -/
def twoSumLoop
(nums : Array Int) (target : Int) (i : Nat) (map : HashMap Int Nat) :
Option (Nat × Nat) :=
if _ : i < nums.size then
let x := nums[i]
let complement := target - x
match map[complement]? with
| some j => some (j, i)
| none => twoSumLoop nums target (i + 1) (map.insert x i)
else
none
/-- The main function that finds two indices in `nums`
whose values add up to `target`. -/
def twoSum (nums : Array Int) (target : Int) : Option (Nat × Nat) :=
twoSumLoop nums target 0 {}First Theorem Proof:
/-- Specifies when a pair of indices `(i, j)` is a solution
to the two-sum problem: `i` and `j` are distinct indices in bound. -/
def is_solution (nums : Array Int) (target : Int) (i j : Nat) : Prop :=
∃ (_ : i < nums.size) (_ : j < nums.size) (_ : i ≠ j),
nums[i] + nums[j] = target
/-- `twoSum` takes an array of integers and a target integer,
and returns a pair of indices (or `none`). -/
def TwoSumSignature : Type := Array Int → Int → Option (Nat × Nat)
/-- Specifies when a function `twoSum_fun` correctly solves the two-sum problem:
- If there exists a solution, then `twoSum_fun` will find it.
- If there exists multiple solutions, then `twoSum_fun` will find one of them.
- For simplicity, the no-solution case is not covered.
-/
def twoSum_correct (twoSum_fun : TwoSumSignature) : Prop :=
∀ (nums : Array Int) (target : Int),
(∃ i j, is_solution nums target i j) →
(∃ i j, twoSum_fun nums target = some (i, j) ∧ is_solution nums target i j)
/-- Finally, the statement that `twoSum` is correct. -/
theorem twoSum_is_correct : twoSum_correct twoSum/-- Loop invariant (right before `i`-th iteration of `twoSumLoop`):
- `i ≤ nums.size` (the `=` may be reached once the entire array is processed).
- *`map` is complete*: forall `i' < i`, `nums[i']` is in `map`.
- *`map` is sound*: `∀ x` in `map`, `map[x] < i` and `nums[map[x]] = x`.
- No solution has been found in the first `i` iterations, i.e.,
there are no `i' < i` and `j' < i` such that `nums[i'] + nums[j'] = target`.
-/
def loop_invariant
(nums : Array Int) (target : Int) (i : Nat) (map : HashMap Int Nat) :
Prop :=
i ≤ nums.size ∧
(∀ i' < i, ∃ x, nums[i']? = some x ∧ map.contains x) ∧
(∀ x i', map[x]? = some i' → i' < i ∧ nums[i']? = some x) ∧
(∀ i' < i, ∀ j' < i, ¬ is_solution nums target i' j')
/-- Shows that `loop_invariant` holds before the first iteration. -/
theorem loop_invariant_initialization (nums : Array Int) (target : Int)
(h_pre : ∃ i j, is_solution nums target i j) :
loop_invariant nums target 0 {} := by
-- Sorry for the messy proof!!
-- I am still learning Lean, there is a lot of trial-and-error stuff...
unfold loop_invariant
constructor
· let ⟨i, j, h_sol⟩ := h_pre
let ⟨hi, hj, hne, hsum⟩ := h_sol
exact Nat.zero_le nums.size
· constructor
· intros i' hi'
contradiction
· constructor
· intros x i' hget
have h : (∅ : HashMap Int Nat)[x]? = none := by
exact HashMap.getElem?_empty
rw [h] at hget
contradiction
· intros i' j' hi' hj'
contradiction
/-- Recursively shows that if `loop_invariant` holds before some iteration,
the loop will finally exit with a correct answer. -/
theorem loop_invariant_recursion (nums : Array Int) (target : Int)
(i : Nat) (map : HashMap Int Nat)
(h_pre : ∃ i j, is_solution nums target i j)
(h_inv : loop_invariant nums target i map) :
∃ i' j', twoSumLoop nums target i map = some (i', j')
∧ is_solution nums target i' j' := by
-- Sorry again for the messy and unreasonably long proof!! (But it works!!)
induction i, map using twoSumLoop.induct nums target
case case1 i map hi x complement j hget =>
let ⟨_, _, hmap_correct, _⟩ := h_inv
exists j, i
constructor
· unfold twoSumLoop
simp [hi]
rw [hget]
· unfold is_solution
let ⟨hj_lt, hj_val⟩ := hmap_correct complement j hget
have hj_get : nums[j] = complement := by
exact Array.getElem_eq_iff.mpr hj_val
refine ⟨by omega, hi, by omega, ?_⟩
rw [hj_get]
simp [complement, x]
case case2 i map hi x complement hget ih =>
unfold twoSumLoop
simp [hi]
rw [hget]
simp
apply ih
unfold loop_invariant
refine ⟨?h_lt, ?h_contains, ?h_correct, ?h_no_sol⟩
· omega
· intros i' hi'
let ⟨h₁, h₂, h₃, h₄⟩ := h_inv
by_cases h_lt : i' < i
· let ⟨x', hx'⟩ := h₂ i' h_lt
let ⟨hx'_val, hx'_map⟩ := hx'
exists x'
constructor
· exact hx'_val
· rw [HashMap.contains_insert, hx'_map]
simp
· have hi_eq : i' = i := by
apply Nat.eq_of_lt_succ_of_not_lt hi' h_lt
rw [hi_eq]
exists x
simp
exact (Array.getElem?_eq_some_getElem_iff nums i hi).mpr trivial
· let ⟨h₁, h₂, h₃, h₄⟩ := h_inv
intros x' i' hget'
rw [HashMap.getElem?_insert] at hget'
split at hget'
· have hi_eq : i' = i := by
injection hget' with hi_eq'
rw [hi_eq']
rw [hi_eq]
constructor
· omega
· rename_i h_eq_bool
simp at h_eq_bool
rw [← h_eq_bool]
exact (Array.getElem?_eq_some_getElem_iff nums i hi).mpr trivial
· let ⟨old_lt, old_val⟩ := h₃ x' i' hget'
constructor
· omega
· exact old_val
· intros i' hi' j' hj' h_is_sol
let ⟨_, h₂, _, h₄⟩ := h_inv
if h_both_lt : i' < i ∧ j' < i then
exact h₄ i' h_both_lt.1 j' h_both_lt.2 h_is_sol
else
have : i' = i ∨ j' = i := by omega
rcases h_is_sol with ⟨_, _, h_ne, h_sum⟩
cases this with
| inl h_i_eq_i =>
subst h_i_eq_i
have hj_lt_i : j' < i' := by omega
rcases h₂ j' hj_lt_i with ⟨val_j, h_val_j, h_in_map⟩
have h_complement : nums[j'] = complement := by
simp [complement, x]
rw [← h_sum]
exact Eq.symm ((fun {b a c} => Int.sub_eq_iff_eq_add'.mpr) rfl)
rw [← h_complement] at hget
have h_val_j' : nums[j'] = val_j := by
exact Array.getElem_eq_iff.mpr h_val_j
rw [h_val_j'] at hget
have hh : map.contains val_j = false := by
rw [HashMap.contains_eq_isSome_getElem?]
rw [hget]
simp
rw [hh] at h_in_map
contradiction
| inr h_j_eq_i =>
subst h_j_eq_i
have hi_lt_j : i' < j' := by
omega
let ⟨val_i, h_val_i, h_in_map⟩ := h₂ i' hi_lt_j
have h_val_is_comp : val_i = complement := by
rw [Array.getElem?_eq_getElem] at h_val_i
injection h_val_i with h_val_i'
rw [← h_val_i']
unfold complement
unfold x
rw [← h_sum]
simp
rfl
rw [h_val_is_comp] at h_in_map
rw [HashMap.contains_eq_isSome_getElem?] at h_in_map
rw [hget] at h_in_map
simp at h_in_map
case case3 i map h_not_lt =>
let ⟨_, _, _, hno_sol⟩ := h_inv
exfalso
let ⟨i0, j0, hsol⟩ := h_pre
let ⟨hi0, hj0, hne, hsum⟩ := hsol
have hi0_lt_i : i0 < i := by omega
have hj0_lt_i : j0 < i := by omega
exact hno_sol i0 hi0_lt_i j0 hj0_lt_i hsol
/-- Finally, the statement that `twoSum` is correct. -/
theorem twoSum_is_correct : twoSum_correct twoSum := by
unfold twoSum_correct
intros nums target h_pre
unfold twoSum
apply loop_invariant_recursion
· exact h_pre
· apply loop_invariant_initialization
exact h_pre
Status: Incorrect
Feedback:
Compilation error for /root/CodeProofTheArena/temp/tmp8e9o_8mg/proof.lean: /root/CodeProofTheArena/temp/tmp8e9o_8mg/proof.lean:5:65: error: unexpected token 'open'; expected ':=', 'where' or '|' /root/CodeProofTheArena/temp/tmp8e9o_8mg/proof.lean:24:4: error: 'twoSum' has already been declared /root/CodeProofTheArena/temp/tmp8e9o_8mg/proof.lean:49:49: error: unexpected token '/--'; expected ':=', 'where' or '|' /root/CodeProofTheArena/temp/tmp8e9o_8mg/proof.lean:108:14: error: unknown constant 'Array.getElem_eq_iff.mpr' /root/CodeProofTheArena/temp/tmp8e9o_8mg/proof.lean:136:15: error: unknown constant 'Array.getElem?_eq_some_getElem_iff' /root/CodeProofTheArena/temp/tmp8e9o_8mg/proof.lean:150:17: error: unknown constant 'Array.getElem?_eq_some_getElem_iff' /root/CodeProofTheArena/temp/tmp8e9o_8mg/proof.lean:170:43: error: unknown constant 'Int.sub_eq_iff_eq_add'.mpr' /root/CodeProofTheArena/temp/tmp8e9o_8mg/proof.lean:173:18: error: unknown constant 'Array.getElem_eq_iff.mpr' /root/CodeProofTheArena/temp/tmp8e9o_8mg/proof.lean:209:8: error: 'twoSum_is_correct' has already been declared