------------------------------------------------------------------------
-- The Agda standard library
--
-- Universal lifting of predicates over Vectors
------------------------------------------------------------------------

{-# OPTIONS --cubical-compatible --safe #-}

module Data.Vec.Functional.Relation.Unary.All where

open import Data.Fin.Properties using (all?)
open import Data.Product.Base using (_,_)
open import Data.Vec.Functional as VF hiding (map)
open import Level using (Level)
open import Relation.Unary

private
  variable
    a p q  : Level
    A : Set a

------------------------------------------------------------------------
-- Definition

All : Pred A    {n}  Vector A n  Set 
All P xs =  i  P (xs i)

------------------------------------------------------------------------
-- Operations

module _ {P : Pred A p} {Q : Pred A q} where

  map : P  Q   {n}  All P {n = n}  All Q
  map p⊆q ps i = p⊆q (ps i)

------------------------------------------------------------------------
-- Properties of predicates preserved by All

module _ {P : Pred A p} where

  all : Decidable P   {n}  Decidable (All P {n = n})
  all p? xs = all? λ i  p? (xs i)

  universal : Universal P   {n}  Universal (All P {n = n})
  universal uni xs i = uni (xs i)

  satisfiable : Satisfiable P   {n}  Satisfiable (All P {n = n})
  satisfiable (x , px) =  _  x) ,  _  px)