twoSum

The real classical challenge at https://leetcode.com/problems/two-sum/ !

Given an array of integers nums and an integer target,
return indices of the two numbers such that they add up to target.

You may assume that each input would have exactly one solution,
and you may not use the same element twice.

You can return the answer in any order.

Function Signature

def twoSum (nums : Array Int) (target : Int) : Option (Nat × Nat)

Theorem Signature

/-- 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

View All Submissions

Please log in or register to submit a solution for this challenge.