agda-spa/Utils.agda

module Utils where

open import Agda.Primitive using () renaming (_⊔_ to _⊔ℓ_)
open import Data.Product as Prod using ()
open import Data.Nat using (ℕ; suc)
open import Data.List using (List; cartesianProduct; []; _∷_; _++_; foldr) renaming (map to mapˡ)
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Membership.Propositional.Properties as ListMemProp using ()
open import Data.List.Relation.Unary.All using (All; []; _∷_; map)
open import Data.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-export these with nicer names from map
open import Function.Definitions using (Injective)
open import Relation.Binary.PropositionalEquality using (_≡_; sym; refl)
open import Relation.Nullary using (¬_)

data Unique {c} {C : Set c} : List C → Set c where
    empty : Unique []
    push : ∀ {x : C} {xs : List C}
        → All (λ x' → ¬ x ≡ x') xs
        → Unique xs
        → Unique (x ∷ xs)

Unique-append : ∀ {c} {C : Set c} {x : C} {xs : List C} →
                ¬ x ∈ xs → Unique xs →  Unique (xs ++ (x ∷ []))
Unique-append {c} {C} {x} {[]} _ _ = push [] empty
Unique-append {c} {C} {x} {x' ∷ xs'} x∉xs (push x'≢ uxs') =
    push (help x'≢) (Unique-append (λ x∈xs' → x∉xs (there x∈xs')) uxs')
    where
        x'≢x : ¬ x' ≡ x
        x'≢x x'≡x = x∉xs (here (sym x'≡x))

        help : {l : List C} → All (λ x'' → ¬ x' ≡ x'') l → All (λ x'' → ¬ x' ≡ x'') (l ++ (x ∷ []))
        help {[]} _ = x'≢x ∷ []
        help {e ∷ es} (x'≢e ∷ x'≢es) = x'≢e ∷ help x'≢es

All-≢-map : ∀ {c d} {C : Set c} {D : Set d} (x : C) {xs : List C} (f : C → D) →
            Injective (_≡_ {_} {C}) (_≡_ {_} {D}) f →
            All (λ x' → ¬ x ≡ x') xs → All (λ y' → ¬ (f x) ≡ y') (mapˡ f xs)
All-≢-map x f f-Injecitve [] = []
All-≢-map x {x' ∷ xs'} f f-Injecitve (x≢x' ∷ x≢xs') = (λ fx≡fx' → x≢x' (f-Injecitve fx≡fx')) ∷ All-≢-map x f f-Injecitve x≢xs'

Unique-map : ∀ {c d} {C : Set c} {D : Set d} {l : List C} (f : C → D) →
             Injective (_≡_ {_} {C}) (_≡_ {_} {D}) f →
             Unique l → Unique (mapˡ f l)
Unique-map {l = []} _ _ _ = empty
Unique-map {l = x ∷ xs} f f-Injecitve (push x≢xs uxs) = push (All-≢-map x f f-Injecitve x≢xs) (Unique-map f f-Injecitve uxs)

All¬-¬Any : ∀ {p c} {C : Set c} {P : C → Set p} {l : List C} → All (λ x → ¬ P x) l → ¬ Any P l
All¬-¬Any {l = x ∷ xs} (¬Px ∷ _) (here Px) = ¬Px Px
All¬-¬Any {l = x ∷ xs} (_ ∷ ¬Pxs) (there Pxs) = All¬-¬Any ¬Pxs Pxs

All-single : ∀ {p c} {C : Set c} {P : C → Set p} {c : C} {l : List C} → All P l → c ∈ l → P c
All-single {c = c} {l = x ∷ xs} (p ∷ ps) (here refl) = p
All-single {c = c} {l = x ∷ xs} (p ∷ ps) (there c∈xs) = All-single ps c∈xs

All-x∈xs : ∀ {a} {A : Set a} (xs : List A) → All (λ x → x ∈ xs) xs
All-x∈xs [] = []
All-x∈xs (x ∷ xs') = here refl ∷ map there (All-x∈xs xs')

x∈xs⇒fx∈fxs : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) {x : A} {xs : List A} →
              x ∈ xs → (f x) ∈ mapˡ f xs
x∈xs⇒fx∈fxs f (here refl) = here refl
x∈xs⇒fx∈fxs f (there x∈xs') = there (x∈xs⇒fx∈fxs f x∈xs')

iterate : ∀ {a} {A : Set a} (n : ℕ) → (f : A → A) → A → A
iterate 0 _ a = a
iterate (suc n) f a = f (iterate n f a)

data Pairwise {a} {b} {c} {A : Set a} {B : Set b} (P : A → B → Set c) : List A → List B → Set (a ⊔ℓ b ⊔ℓ c)  where
    [] : Pairwise P [] []
    _∷_ : ∀ {x : A} {y : B} {xs : List A} {ys : List B} →
          P x y → Pairwise P xs ys →
          Pairwise P (x ∷ xs) (y ∷ ys)

∈-cartesianProduct : ∀ {a b} {A : Set a} {B : Set b}
                     {x : A} {xs : List A} {y : B} {ys : List B} →
                     x ∈ xs → y ∈ ys → (x Prod., y) ∈ cartesianProduct xs ys
∈-cartesianProduct {x = x} (here refl) y∈ys = ListMemProp.∈-++⁺ˡ (x∈xs⇒fx∈fxs (x Prod.,_) y∈ys)
∈-cartesianProduct {x = x} {xs = x' ∷ _} {ys = ys} (there x∈rest) y∈ys = ListMemProp.∈-++⁺ʳ (mapˡ (x' Prod.,_) ys) (∈-cartesianProduct x∈rest y∈ys)

concat-∈ : ∀ {a} {A : Set a} {x : A} {l : List A} {ls : List (List A)} →
           x ∈ l → l ∈ ls → x ∈ foldr _++_ [] ls
concat-∈ x∈l (here refl) = ListMemProp.∈-++⁺ˡ x∈l
concat-∈ {ls = l' ∷ ls'} x∈l (there l∈ls') = ListMemProp.∈-++⁺ʳ l' (concat-∈ x∈l l∈ls')

_⇒_ : ∀ {a p₁ p₂} {A : Set a} (P : A → Set p₁) (Q : A → Set p₂) →
      Set (a ⊔ℓ p₁ ⊔ℓ p₂)
_⇒_ P Q = ∀ a → P a → Q a