DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Define unique as a data type to match stdlib All and Any

Browse Source
This commit is contained in:
Danila Fedorin
2023-07-23 21:34:24 -07:00
parent d9c18fe483
commit f2e72b54ce
1 changed files with 7 additions and 6 deletions
Download Patch File Download Diff File Expand all files Collapse all files

13
Map.agda
View File

@@ -22,11 +22,12 @@ open import Data.Empty using (⊥)
Map : Set (a ⊔ b) Map : Set (a ⊔ b)
Map = List (A × B) Map = List (A × B)
record ⊤' : Set (a ⊔ b) where data Unique : List (A × B) → Set (a ⊔ b) where
empty : Unique []
Unique : List (A × B) → Set (a ⊔ b) push : forall {k : A} {v : B} {xs : List (A × B)}
Unique [] = ⊤' → All (λ (k' , _) → ¬ k ≡ k') xs
Unique ((k , _) ∷ xs) = All (λ (k' , _) → ¬ k ≡ k') xs × Unique xs → Unique xs
→ Unique ((k , v) ∷ xs)
_∈_ : (A × B) → Map → Set (a ⊔ b) _∈_ : (A × B) → Map → Set (a ⊔ b)
_∈_ p m = Data.List.Membership.Propositional._∈_ p m _∈_ p m = Data.List.Membership.Propositional._∈_ p m
@@ -55,7 +56,7 @@ merge f m₁ m₂ = foldr (insert f) m₂ m₁
Map-functional : ∀ (k : A) (v v' : B) (xs : List (A × B)) → Unique ((k , v) ∷ xs) → Data.List.Membership.Propositional._∈_ (k , v') ((k , v) ∷ xs) → v ≡ v' Map-functional : ∀ (k : A) (v v' : B) (xs : List (A × B)) → Unique ((k , v) ∷ xs) → Data.List.Membership.Propositional._∈_ (k , v') ((k , v) ∷ xs) → v ≡ v'
Map-functional k v v' _ _ (here k,v'≡k,v) = sym (cong proj₂ k,v'≡k,v) Map-functional k v v' _ _ (here k,v'≡k,v) = sym (cong proj₂ k,v'≡k,v)
Map-functional k v v' xs (k≢ , _) (there k,v'∈xs) = absurd (unique-not-in xs v' (k≢ , k,v'∈xs)) Map-functional k v v' xs (push k≢ _) (there k,v'∈xs) = absurd (unique-not-in xs v' (k≢ , k,v'∈xs))
where where
absurd : ∀ {a} {A : Set a} → ⊥ → A absurd : ∀ {a} {A : Set a} → ⊥ → A
absurd () absurd ()