{-# OPTIONS --without-K --safe #-}
module Util.Vec where

open import Data.Vec public
open import Data.Vec.All as All public using (All ; [] ; _∷_)
open import Data.Vec.Any as Any public using (Any ; here ; there)
open import Data.Vec.Membership.Propositional public using (_∈_)

open import Data.Nat as ℕ using (_≤_)
open import Level using (_⊔_)
open import Relation.Binary using (Rel)

open import Util.Prelude

import Data.Nat.Properties as ℕ


max : ∀ {n} → Vec ℕ n → ℕ
max = foldr _ ℕ._⊔_ 


max-weaken : ∀ {n} x (xs : Vec ℕ n) → max xs ≤ max (x ∷ xs)
max-weaken _ _ = ℕ.n≤m⊔n _ _


max-maximal : ∀ {n} (xs : Vec ℕ n) → All (_≤ max xs) xs
max-maximal [] = []
max-maximal (x ∷ xs)
  = ℕ.m≤m⊔n _ _
  ∷ All.map (λ x≤max → ℕ.≤-trans x≤max (max-weaken x xs)) (max-maximal xs)


All→∈→P : ∀ {α β} {A : Set α} {P : A → Set β} {n} {xs : Vec A n}
  → All P xs
  → ∀ {x}
  → x ∈ xs
  → P x
All→∈→P (px ∷ allP) (here refl) = px
All→∈→P (px ∷ allP) (there x∈xs) = All→∈→P allP x∈xs


max-maximal-∈ : ∀ {n x} {xs : Vec ℕ n} → x ∈ xs → x ≤ max xs
max-maximal-∈ = All→∈→P (max-maximal _)


data All₂ {α} {A : Set α} {ρ} (R : Rel A ρ)
  : ∀ {n} → Vec A n → Vec A n → Set (α ⊔ ρ) where
  [] : All₂ R [] []
  _∷_ : ∀ {n x y} {xs ys : Vec A n}
    → R x y
    → All₂ R xs ys
    → All₂ R (x ∷ xs) (y ∷ ys)


All₂-tabulate⁺ : ∀ {α} {A : Set α} {ρ} {R : Rel A ρ} {n} {f g : Fin n → A}
  → (∀ x → R (f x) (g x))
  → All₂ R (tabulate f) (tabulate g)
All₂-tabulate⁺ {n = zero} p = []
All₂-tabulate⁺ {n = suc n} p = p zero ∷ All₂-tabulate⁺ (λ x → p (suc x))


All₂-tabulate⁻ : ∀ {α} {A : Set α} {ρ} {R : Rel A ρ} {n} {f g : Fin n → A}
  → All₂ R (tabulate f) (tabulate g)
  → ∀ x → R (f x) (g x)
All₂-tabulate⁻ [] ()
All₂-tabulate⁻ (fzRgz ∷ all) zero = fzRgz
All₂-tabulate⁻ (fzRgz ∷ all) (suc x) = All₂-tabulate⁻ all x