Migrate Maps to including a uniqueness proof

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2023-07-24 23:55:09 -07:00
parent c2bc1c5421
commit 4aea9a0358
2 changed files with 43 additions and 26 deletions

View File

@ -101,19 +101,22 @@ module IsEquivalenceInstances where
in (v'' , (≈₂-trans v≈v' v'≈v'' , k,v''∈m₃))
≈-refl : {m : Map} m m
≈-refl {m} = (⊆-refl , ⊆-refl)
≈-refl {m} = (⊆-refl {m}, ⊆-refl {m})
≈-sym : {m₁ m₂ : Map} m₁ m₂ m₂ m₁
≈-sym (m₁⊆m₂ , m₂⊆m₁) = (m₂⊆m₁ , m₁⊆m₂)
≈-trans : {m₁ m₂ m₃ : Map} m₁ m₂ m₂ m₃ m₁ m₃
≈-trans (m₁⊆m₂ , m₂⊆m₁) (m₂⊆m₃ , m₃⊆m₂) = (⊆-trans m₁⊆m₂ m₂⊆m₃ , ⊆-trans m₃⊆m₂ m₂⊆m₁)
≈-trans {m₁} {m₂} {m₃} (m₁⊆m₂ , m₂⊆m₁) (m₂⊆m₃ , m₃⊆m₂) =
( ⊆-trans {m₁} {m₂} {m₃} m₁⊆m₂ m₂⊆m₃
, ⊆-trans {m₃} {m₂} {m₁} m₃⊆m₂ m₂⊆m₁
)
LiftEquivalence : IsEquivalence Map _≈_
LiftEquivalence = record
{ ≈-refl = ≈-refl
; ≈-sym = ≈-sym
; ≈-trans = ≈-trans
{ ≈-refl = λ {m₁} ≈-refl {m₁}
; ≈-sym = λ {m₁} {m₂} ≈-sym {m₁} {m₂}
; ≈-trans = λ {m₁} {m₂} {m₃} ≈-trans {m₁} {m₂} {m₃}
}
module IsSemilatticeInstances where

View File

@ -18,9 +18,6 @@ open import Data.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-ex
open import Data.Product using (_×_; _,_; Σ; proj₁ ; proj₂)
open import Data.Empty using ()
Map : Set (a b)
Map = List (A × B)
keys : List (A × B) List A
keys [] = []
keys ((k , v) xs) = k keys xs
@ -32,6 +29,9 @@ data Unique {c} {C : Set c} : List C → Set c where
Unique xs
Unique (x xs)
Map : Set (a b)
Map = Σ (List (A × B)) (λ l Unique (keys l))
Unique-append : {c} {C : Set c} {x : C} {xs : List C} ¬ MemProp._∈_ 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')
@ -46,15 +46,6 @@ Unique-append {c} {C} {x} {x' ∷ xs'} x∉xs (push x'≢ uxs') = push (help x'
_∈_ : (A × B) List (A × B) Set (a b)
_∈_ p m = MemProp._∈_ p m
subset : (_≈_ : B B Set b) List (A × B) List (A × B) Set (a b)
subset _≈_ m₁ m₂ = (k : A) (v : B) (k , v) m₁ Σ B (λ v' v v' × ((k , v') m₂))
lift : (_≈_ : B B Set b) List (A × B) List (A × B) Set (a b)
lift _≈_ m₁ m₂ = (m₁ m₂) × (m₂ m₁)
where
_⊆_ : List (A × B) List (A × B) Set (a b)
_⊆_ = subset _≈_
foldr : {c} {C : Set c} (A B C C) -> C -> List (A × B) -> C
foldr f b [] = b
foldr f b ((k , v) xs) = f k v (foldr f b xs)
@ -62,7 +53,11 @@ foldr f b ((k , v) ∷ xs) = f k v (foldr f b xs)
absurd : {a} {A : Set a} A
absurd ()
private module Impl (f : B B B) where
private module ImplRelation (_≈_ : B B Set b) where
subset : List (A × B) List (A × B) Set (a b)
subset m₁ m₂ = (k : A) (v : B) (k , v) m₁ Σ B (λ v' v v' × ((k , v') m₂))
private module ImplInsert (f : B B B) where
_∈k_ : A List (A × B) Set a
_∈k_ k m = MemProp._∈_ k (keys m)
@ -110,13 +105,32 @@ private module Impl (f : B → B → B) where
merge-preserves-unique [] l₂ u₂ = u₂
merge-preserves-unique ((k₁ , v₁) xs₁) l₂ u₂ = insert-preserves-unique k₁ v₁ (merge xs₁ l₂) (merge-preserves-unique xs₁ l₂ u₂)
Map-functional : (k : A) (v v' : B) (xs : List (A × B)) Unique (keys ((k , v) xs)) MemProp._∈_ (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' xs (push k≢ _) (there k,v'∈xs) = absurd (unique-not-in xs v' (k≢ , k,v'∈xs))
where
unique-not-in : (xs : List (A × B)) (v' : B) ¬ (All (λ k' ¬ k k') (keys xs) × (k , v') xs)
unique-not-in ((k' , _) xs) v' (k≢k' _ , here k',≡x) = k≢k' (cong proj₁ k',≡x)
unique-not-in (_ xs) v' (_ rest , there k,v'∈xs) = unique-not-in xs v' (rest , k,v'∈xs)
-- Map-functional : ∀ (k : A) (v v' : B) (xs : List (A × B)) → Unique (keys ((k , v) ∷ xs)) → MemProp._∈_ (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' xs (push k≢ _) (there k,v'∈xs) = absurd (unique-not-in xs v' (k≢ , k,v'∈xs))
-- where
-- unique-not-in : ∀ (xs : List (A × B)) (v' : B) → ¬ (All (λ k' → ¬ k ≡ k') (keys xs) × (k , v') ∈ xs)
-- unique-not-in ((k' , _) ∷ xs) v' (k≢k' ∷ _ , here k',≡x) = k≢k' (cong proj₁ k',≡x)
-- unique-not-in (_ ∷ xs) v' (_ ∷ rest , there k,v'∈xs) = unique-not-in xs v' (rest , k,v'∈xs)
module _ (f : B B B) where
open Impl f public using (insert; merge)
open ImplInsert f renaming
( insert to insert-impl
; merge to merge-impl
)
insert : A B Map Map
insert k v (kvs , uks) = (insert-impl k v kvs , insert-preserves-unique k v kvs uks)
merge : Map Map Map
merge (kvs₁ , _) (kvs₂ , uks₂) = (merge-impl kvs₁ kvs₂ , merge-preserves-unique kvs₁ kvs₂ uks₂)
module _ (_≈_ : B B Set b) where
open ImplRelation _≈_ renaming (subset to subset-impl)
subset : Map Map Set (a b)
subset (kvs₁ , _) (kvs₂ , _) = subset-impl kvs₁ kvs₂
lift : Map Map Set (a b)
lift m₁ m₂ = subset m₁ m₂ × subset m₂ m₁