-----Description-----
Given an integer array nums, return true if there exists a triple of indices (i, j, k) such that i < j < k and nums[i] < nums[j] < nums[k]. If no such indices exist, return false.

-----Input-----
The input consists of a single list:
nums: A list of integers.

-----Output-----
The output is a boolean:
Returns true if there exists a triplet (i, j, k) where i < j < k and nums[i] < nums[j] < nums[k]; otherwise, returns false.


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


-- !benchmark @start code_aux

-- !benchmark @end code_aux


def increasingTriplet (nums : List Int) (h_precond : increasingTriplet_precond (nums)) : Bool :=
  -- !benchmark @start code
  -- must have at least 3 elements to form a triplet
  let rec lengthCheck : List Int → Nat → Nat
    | [], acc => acc
    | _ :: rest, acc => lengthCheck rest (acc + 1)

  let len := lengthCheck nums 0

  if len < 3 then
    false
  else
    -- scan for increasing triplet
    let rec loop (xs : List Int) (first : Int) (second : Int) : Bool :=
      match xs with
      | [] => false
      | x :: rest =>
        let nextFirst := if x ≤ first then x else first
        let nextSecond := if x > first ∧ x ≤ second then x else second
        if x ≤ first then
          loop rest nextFirst second
        else if x ≤ second then
          loop rest first nextSecond
        else
          true  -- found triplet
    match nums with
    | [] => false
    | _ :: rest1 =>
      match rest1 with
      | [] => false
      | _ :: rest2 =>
        match rest2 with
        | [] => false
        | _ =>
          -- Use Option to handle unbounded Int values instead of magic number
          let initFirst := nums.head?
          let initSecond := nums.head?
          match initFirst, initSecond with
          | some f, some s => loop nums f s
          | _, _ => false
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible]
def increasingTriplet_postcond (nums : List Int) (result: Bool) (h_precond : increasingTriplet_precond (nums)) : Prop :=
  -- !benchmark @start postcond
  let nums' := nums.zipIdx
  (result →
    nums'.any (fun (x, i) =>
      nums'.any (fun (y, j) =>
        nums'.any (fun (z, k) =>
          i < j ∧ j < k ∧ x < y ∧ y < z
        )
      )
    ))
  ∧
  (¬ result → nums'.all (fun (x, i) =>
    nums'.all (fun (y, j) =>
      nums'.all (fun (z, k) =>
        i ≥ j ∨ j ≥ k ∨ x ≥ y ∨ y ≥ z
      )
    )
  ))
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem increasingTriplet_spec_satisfied (nums: List Int) (h_precond : increasingTriplet_precond (nums)) :
    increasingTriplet_postcond (nums) (increasingTriplet (nums) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: nums: [1, 2, 3]
nums: [5, 4, 3, 2, 1]
nums: [2, 1, 5, 0, 4, 6]
nums: [1, 5, 0, 4, 1, 3]
nums: [5, 4, 3]
expected: True
False
True
True
False
False
unexpected: False
True
False
False
True
True

Inputs rejected by the precondition: