Some awful ugly testing of a bound function, as an idea of how to get fresh variables in tome

bound.agda

open import Agda.Builtin.Nat renaming (Nat to ℕ) hiding (_<_)
open import Agda.Builtin.Sigma

open import Decidable
open import List

prec : ∀ n m → suc n ≡ suc m → n ≡ m
prec n .n refl = refl

suc≢ : ∀ n → (suc n) ≢ n
suc≢ n ()

suc+≢ : ∀ n m → suc n + m ≢ n
suc+≢ zero m ()
suc+≢ (suc n) m x = suc+≢ n m (prec (suc (n + m)) n x)

suc+≢' : ∀ n m → suc (n + m) ≢ n
suc+≢' zero m ()
suc+≢' (suc n) m eq = suc+≢' n m (prec (suc (n + m)) n eq)

data _≤_ : ℕ → ℕ → Set where
  0≤n    : ∀{n} → zero ≤ n
  sn≤sm : ∀{n m} → n ≤ m → (suc n) ≤ (suc m)

≤refl : ∀ n → n ≤ n
≤refl zero = 0≤n
≤refl (suc n) = sn≤sm (≤refl n)

≤trans : ∀ x y z → x ≤ y → y ≤ z → x ≤ z
≤trans .0 y z 0≤n y≤z = 0≤n
≤trans (suc x) (suc y) (suc z) (sn≤sm x≤y) (sn≤sm y≤z) = sn≤sm (≤trans x y z x≤y y≤z)

_<_ : ℕ → ℕ → Set
n < m = suc n ≤ m

_≤?_ : (n m : ℕ) → Dec (n ≤ m)
zero ≤? zero = yes 0≤n
zero ≤? suc m = yes 0≤n
suc n ≤? zero = no (λ ())
suc n ≤? suc m with n ≤? m
...            | yes n≤m = yes (sn≤sm n≤m)
...            | no ¬n≤m = no φ
                           where φ : _
                                 φ (sn≤sm n≤m) = ¬n≤m n≤m

order : ∀ n m → ¬(n ≤ m) → m ≤ n
order zero m ¬n≤m = ⊥-elim (¬n≤m 0≤n)
order (suc n) zero ¬n≤m = 0≤n
order (suc n) (suc m) ¬n≤m = sn≤sm (order n m (λ z → ¬n≤m (sn≤sm z)))


bound : (xs : List ℕ) → Σ ℕ (λ y → All (λ x → x ≤ y) xs)
bound [] = zero , []
bound (x ∷ xs) with bound xs
bound (x ∷ xs) | bxs , bxspf with x ≤? bxs
bound (x ∷ xs) | bxs , bxspf | yes x≤bxs = bxs , x≤bxs ∷ bxspf
bound (x ∷ xs) | bxs , bxspf | no ¬x≤bxs = x , ≤refl x ∷ alltrans bxs x xs (order x bxs ¬x≤bxs) bxspf
  where
    alltrans : ∀ x y xs → x ≤ y → All (_≤ x) xs → All (_≤ y) xs
    alltrans x y .[] x≤y [] = []
    alltrans x y (z ∷ zs) x≤y (pf ∷ pfs) = ≤trans z x y pf x≤y ∷ alltrans x y zs x≤y pfs

unique : (xs : List ℕ) → Σ ℕ (λ x → All (x ≢_) xs)
unique xs with bound xs
unique xs | bxs , bxspf = suc bxs , alllemma bxs xs bxspf
  where
    suclemma : ∀ x y → y ≤ x → suc x ≢ y
    suclemma zero .0 0≤n ()
    suclemma (suc x) .(suc (suc x)) (sn≤sm y≤x) refl = suclemma x (suc x) y≤x refl
    alllemma : ∀ x xs → All (λ y → y ≤ x) xs → All (λ y → suc x ≢ y) xs
    alllemma x .[] [] = []
    alllemma x (y ∷ ys) (pf ∷ pfs) = suclemma x y pf ∷ alllemma x ys pfs

-- Phew. An example:
nums : List ℕ
nums = 4 ∷ 2 ∷ 6 ∷ 5 ∷ 1 ∷ []

greatest : ℕ
greatest = fst (bound nums)
-- greatest = 6

bigger : ℕ
bigger = fst (unique nums)
-- bigger = 7