-----Description-----
This task requires writing a Lean 4 method that finds the indices of two numbers in an array that add up to a target value. Given an array of integers and a target integer, the function should return the indices of the two numbers such that they add up to the target.

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

-----Input-----
The input consists of:
nums: An array of integers.
target: An integer representing the target sum.

-----Output-----
The output is an array of two integers:
Returns the indices of the two numbers in the array that add up to the target. The indices should be sorted.


Difficulty: advanced

Lean 4 solution:
-- !benchmark @start import type=solution

-- !benchmark @end import

-- !benchmark @start solution_aux

-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux
@[reducible]
def twoSum_precond (nums : Array Int) (target : Int) : Prop :=
  -- !benchmark @start precond
  -- The array must have at least 2 elements
  nums.size ≥ 2 ∧

  -- There exists exactly one pair of indices whose values sum to the target
  (List.range nums.size).any (fun i =>
    (List.range i).any (fun j => nums[i]! + nums[j]! = target)) ∧

  -- No other pair sums to the target (ensuring uniqueness of solution)
  ((List.range nums.size).flatMap (fun i =>
    (List.range i).filter (fun j => nums[i]! + nums[j]! = target))).length = 1
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def twoSum (nums : Array Int) (target : Int) (h_precond : twoSum_precond (nums) (target)) : Array Nat :=
  -- !benchmark @start code
  let rec findIndices (i : Nat) (j : Nat) (fuel : Nat) : Array Nat :=
    match fuel with
    | 0 => #[] -- Fuel exhausted, return empty array
    | fuel+1 =>
      if i >= nums.size then
        #[] -- No solution found
      else if j >= nums.size then
        findIndices (i + 1) (i + 2) fuel -- Move to next i and reset j
      else
        if nums[i]! + nums[j]! == target then
          #[i, j] -- Found solution
        else
          findIndices i (j + 1) fuel -- Try next j

  findIndices 0 1 (nums.size * nums.size)
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def twoSum_postcond (nums : Array Int) (target : Int) (result: Array Nat) (h_precond : twoSum_precond (nums) (target)) : Prop :=
  -- !benchmark @start postcond
  -- Result contains exactly 2 indices
  result.size = 2 ∧

  -- The indices are valid (within bounds of the nums array)
  result[0]! < nums.size ∧ result[1]! < nums.size ∧

  -- The indices are in ascending order (sorted)
  result[0]! < result[1]! ∧

  -- The values at these indices sum to the target
  nums[result[0]!]! + nums[result[1]!]! = target
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem twoSum_spec_satisfied (nums: Array Int) (target: Int) (h_precond : twoSum_precond (nums) (target)) :
    twoSum_postcond (nums) (target) (twoSum (nums) (target) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof




Tests:
input: nums: #[2, 7, 11, 15]
target: 9
nums: #[3, 2, 4]
target: 6
nums: #[3, 3]
target: 6
nums: #[1, 2, 3, 4, 5]
target: 9
nums: #[0, 4, 3, 0]
target: 0
expected: #[0, 1]
#[1, 2]
#[0, 1]
#[3, 4]
#[0, 3]
unexpected: #[1, 0]
#[2, 3]
#[0, 3]
#[0, 1]
#[0, 2]
#[0, 3]
#[1, 0]
#[2, 2]
#[0, 4]
#[1, 3]
#[2, 2]
#[1, 2]
#[2, 1]

Inputs rejected by the precondition:
nums: #[0]
target: 2