Add more properties of uniqueness

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-03-09 13:54:01 -08:00
parent 332b7616cf
commit 1ccc6f08e5

View File

@ -2,10 +2,11 @@ module Utils where
open import Agda.Primitive using () renaming (_⊔_ to _⊔_) open import Agda.Primitive using () renaming (_⊔_ to _⊔_)
open import Data.Nat using (; suc) open import Data.Nat using (; suc)
open import Data.List using (List; []; _∷_; _++_) open import Data.List using (List; []; _∷_; _++_) renaming (map to mapˡ)
open import Data.List.Membership.Propositional using (_∈_) open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Relation.Unary.All using (All; []; _∷_; map) 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 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.Binary.PropositionalEquality using (_≡_; sym; refl)
open import Relation.Nullary using (¬_) open import Relation.Nullary using (¬_)
@ -29,6 +30,18 @@ Unique-append {c} {C} {x} {x' ∷ xs'} x∉xs (push x'≢ uxs') =
help {[]} _ = x'≢x [] help {[]} _ = x'≢x []
help {e es} (x'≢e x'≢es) = x'≢e help x'≢es 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 : {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} (¬Px _) (here Px) = ¬Px Px
All¬-¬Any {l = x xs} (_ ¬Pxs) (there Pxs) = All¬-¬Any ¬Pxs Pxs All¬-¬Any {l = x xs} (_ ¬Pxs) (there Pxs) = All¬-¬Any ¬Pxs Pxs