agda-spa/Utils.agda
Danila Fedorin 3a537f54ba Add a helpful utility function
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-03-01 19:08:11 -08:00

46 lines
2.1 KiB
Agda
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

module Utils where
open import Data.Nat using (; suc)
open import Data.List using (List; []; _∷_; _++_)
open import Data.List.Membership.Propositional 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 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¬-¬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')
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)