-----Description-----
This task requires writing a Lean 4 method that implementing the "Two Sum" problem. Given a list of integers
and a target integer, the function should return the indices of the two numbers that add up to
the target. If no valid pair exists, the function should return none. And the indices returned must
be within the bounds of the list. If multiple pairs exist, return the lexicographically first pair (i, j),
meaning the pair with the smallest i, and among those, the smallest j.

-----Input-----
- nums: A list of integers.
- target: An integer representing the target sum.

-----Output-----
- An option type containing a pair of natural numbers (indices) such that
  nums[i] + nums[j] = target with i < j, if such a pair exists. Otherwise, it returns none.
  The pair returned must be lexicographically first among all valid pairs.


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 : List Int) (target : Int) : Prop :=
  -- !benchmark @start precond
  True
  -- !benchmark @end precond


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def twoSum (nums : List Int) (target : Int) (h_precond : twoSum_precond (nums) (target)) : Option (Nat × Nat) :=
  -- !benchmark @start code
  let rec outer (lst : List Int) (i : Nat)
            : Option (Nat × Nat) :=
        match lst with
        | [] =>
            none
        | x :: xs =>
            let rec inner (lst' : List Int) (j : Nat)
                    : Option Nat :=
                match lst' with
                | [] =>
                    none
                | y :: ys =>
                    if x + y = target then
                        some j
                    else
                        inner ys (j + 1)
            match inner xs (i + 1) with
            | some j =>
                some (i, j)
            | none =>
                outer xs (i + 1)
        outer nums 0
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def twoSum_postcond (nums : List Int) (target : Int) (result: Option (Nat × Nat)) (h_precond : twoSum_precond (nums) (target)) : Prop :=
  -- !benchmark @start postcond
    match result with
    | none => List.Pairwise (· + · ≠ target) nums
    | some (i, j) =>
        i < j ∧
        j < nums.length ∧
        nums[i]! + nums[j]! = target ∧
        -- Lexicographically first: no valid pair (i', j') with i' < i exists
        (nums.take i).zipIdx.all (fun ⟨a, i'⟩ =>
          (nums.drop (i' + 1)).all (fun b => a + b ≠ target)) ∧
        -- For this i, j is the smallest valid partner
        ((nums.drop (i + 1)).take (j - i - 1)).all (fun b => nums[i]! + b ≠ target)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem twoSum_spec_satisfied (nums: List 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]
target: 7
nums: [0, 4, 3, 0]
target: 0
expected: some (0, 1)
some (1, 2)
some (0, 1)
none
some (0, 3)
unexpected: some (1, 2)
none
some (0, 2)
none
some (1, 1)
none
some (0, 2)
some (1, 2)
none

Inputs rejected by the precondition: