-----Description-----  
The task is to determine whether there exists at least one pair of different floating-point numbers in a list such that the absolute difference between them is less than a given threshold. The focus is solely on deciding if such a pair is present in the list.

-----Input-----  
The input consists of:  
• numbers: A list of floating-point numbers.  
• threshold: A floating-point number representing the maximum allowed difference between two numbers for them to be considered "close."  

-----Output-----  
The output is a boolean value:  
• true – if there exists at least one pair of distinct elements in the list such that the absolute difference between them is less than the threshold.  
• false – if for every possible pair of elements, the absolute difference is greater than or equal to the threshold.

-----Note-----
It is assumed that:
- The list of numbers contains only valid (non-NaN, non-infinite) floating-point values.
- The threshold is a non-negative, valid floating-point number.
Difficulty: basic

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

-- !benchmark @end import

-- !benchmark @start solution_aux
def absDiff (a b : Float) : Float :=
  if a - b < 0.0 then b - a else a - b
-- !benchmark @end solution_aux

-- !benchmark @start precond_aux

-- !benchmark @end precond_aux
@[reducible, simp]
def has_close_elements_precond (numbers : List Float) (threshold : Float) : Prop :=
  -- !benchmark @start precond
  threshold ≥ 0.0 ∧
  ¬threshold.isNaN ∧
  numbers.all (fun x => ¬x.isNaN ∧ ¬x.isInf)  -- no NaN or Inf values
  -- !benchmark @end precond


-- !benchmark @start code_aux
-- !benchmark @end code_aux


def has_close_elements (numbers : List Float) (threshold : Float) (h_precond : has_close_elements_precond (numbers) (threshold)) : Bool :=
  -- !benchmark @start code
  let len := numbers.length
  let rec outer (idx : Nat) : Bool :=
    if idx < len then
      let rec inner (idx2 : Nat) : Bool :=
        if idx2 < idx then
          let a := numbers.getD idx2 0.0
          let b := numbers.getD idx 0.0
          let d := absDiff a b
          if d < threshold then true else inner (idx2 + 1)
        else
          false
      if inner 0 then true else outer (idx + 1)
    else
      false
  outer 0
  -- !benchmark @end code


-- !benchmark @start postcond_aux

-- !benchmark @end postcond_aux


@[reducible, simp]
def has_close_elements_postcond (numbers : List Float) (threshold : Float) (result: Bool) (h_precond : has_close_elements_precond (numbers) (threshold)) :=
  -- !benchmark @start postcond
  ¬ result ↔ (List.Pairwise (fun a b => absDiff a b ≥ threshold) numbers)
  -- !benchmark @end postcond


-- !benchmark @start proof_aux

-- !benchmark @end proof_aux


theorem has_close_elements_spec_satisfied (numbers: List Float) (threshold: Float) (h_precond : has_close_elements_precond (numbers) (threshold)) :
    has_close_elements_postcond (numbers) (threshold) (has_close_elements (numbers) (threshold) h_precond) h_precond := by
  -- !benchmark @start proof
  sorry
  -- !benchmark @end proof


Tests:
input: numbers: [1.0, 2.0, 3.0]
threshold: 1.5
numbers: [10.0, 12.0, 15.0]
threshold: 1.5
numbers: [5.0, 5.0]
threshold: 0.1
threshold: 2
numbers: [0.0, 0.5, 1.1, 2.2]
threshold: 0.6
expected: True
False
True
False
True

Inputs rejected by the precondition:
numbers: [1.0, 2.0, 3.0]
threshold: -1
numbers: [Float.nan, 1.0]
threshold: 1
numbers: [1.0, Float.nan, 2.0]
threshold: 0.5
numbers: [Float.inf, 1.0]
threshold: 1