From 1ccc6f08e5553261de26c07e643ba89ed84d8dbc Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 9 Mar 2024 13:54:01 -0800 Subject: [PATCH] Add more properties of uniqueness Signed-off-by: Danila Fedorin --- Utils.agda | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/Utils.agda b/Utils.agda index 3432533..6c58ba4 100644 --- a/Utils.agda +++ b/Utils.agda @@ -2,10 +2,11 @@ module Utils where open import Agda.Primitive using () renaming (_⊔_ to _⊔ℓ_) 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.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 (¬_) @@ -29,6 +30,18 @@ Unique-append {c} {C} {x} {x' ∷ xs'} x∉xs (push x'≢ uxs') = 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