Max in agda

max.agda

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

open import Vec

data Max⟨_,_⟩≡_ : ℕ → ℕ → ℕ → Set where
  maxl : ∀{n} → Max⟨ n    , zero ⟩≡ n
  maxr : ∀{n} → Max⟨ zero , n    ⟩≡ n
  suc  : ∀{n m k} → Max⟨ n , m ⟩≡ k → Max⟨ suc n , suc m ⟩≡ suc k

max⟨_,_⟩ : (n m : ℕ) → Σ ℕ Max⟨ n , m ⟩≡_
max⟨ zero  , m     ⟩ = m , maxr
max⟨ n     , zero  ⟩ = n , maxl
max⟨ suc n , suc m ⟩ = suc (fst max⟨ n , m ⟩) , suc (snd max⟨ n , m ⟩)

data Max[_]≡_ : ∀{n} → Vec ℕ (suc n) → ℕ → Set where
  [_] : ∀{x} → Max[ x ∷ [] ]≡ x
  _∷_ : ∀{x n mxs m} {xs : Vec ℕ (suc n)}
         → Max⟨ x , mxs ⟩≡ m → Max[ xs ]≡ mxs → Max[ x ∷ xs ]≡ m

max[_] : ∀{n} → (xs : Vec ℕ (suc n)) → Σ ℕ Max[ xs ]≡_
max[ x ∷ [] ] = x , [_]
max[_] {suc n} (x ∷ xs) with max[ xs ]
...   | mxs , Max[xs]≡mxs with max⟨ x , mxs ⟩
...                       | m , Max⟨x,mxs⟩≡m = m , (Max⟨x,mxs⟩≡m ∷ Max[xs]≡mxs)