From c50195942d6d82050efcc44bcdbae0b404898e0f Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Mon, 24 Jul 2023 20:38:34 -0700
Subject: [PATCH] Start moving away from purely list-based maps.

The eventual goal is to make a map be a list and a proof
that all the keys are unique.

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Map.agda | 53 ++++++++++++++++++++++++++++++++++-------------------
 1 file changed, 34 insertions(+), 19 deletions(-)

diff --git a/Map.agda b/Map.agda
index 723306b..ef2ec18 100644
--- a/Map.agda
+++ b/Map.agda
@@ -22,45 +22,60 @@ open import Data.Empty using (⊥)
 Map : Set (a ⊔ b)
 Map = List (A × B)
 
-data Unique : List (A × B) → Set (a ⊔ b) where
-    empty : Unique []
-    push : forall {k : A} {v : B} {xs : List (A × B)}
-        → All (λ (k' , _) → ¬ k ≡ k') xs
-        → Unique xs
-        → Unique ((k , v) ∷ xs)
+keys : List (A × B) → List A
+keys [] = []
+keys ((k , v) ∷ xs) = k ∷ keys xs
 
-_∈_ : (A × B) → Map → Set (a ⊔ b)
+data Unique {c} {C : Set c} : List C → Set c where
+    empty : Unique []
+    push : forall {x : C} {xs : List C}
+        → All (λ x' → ¬ x ≡ x') xs
+        → Unique xs
+        → Unique (x ∷ xs)
+
+_∈_ : (A × B) → List (A × B) → Set (a ⊔ b)
 _∈_ p m = Data.List.Membership.Propositional._∈_ p m
 
-subset : ∀ (_≈_ : B → B → Set b) → Map → Map → Set (a ⊔ b)
+_∈k_ : A → List (A × B) → Set a
+_∈k_ k m = Data.List.Membership.Propositional._∈_ k (keys 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) → Map → Map → Set (a ⊔ b)
+lift : ∀ (_≈_ : B → B → Set b) → List (A × B) → List (A × B) → Set (a ⊔ b)
 lift _≈_ m₁ m₂ = (m₁ ⊆ m₂) × (m₂ ⊆ m₁)
     where
-        _⊆_ : Map → Map → Set (a ⊔ b)
+        _⊆_ : List (A × B) → List (A × B) → Set (a ⊔ b)
         _⊆_ = subset _≈_
 
-foldr : ∀ {c} {C : Set c} → (A → B → C → C) -> C -> Map -> C
+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)
 
-insert : (B → B → B) → A → B → Map → Map
+insert : (B → B → B) → A → B → List (A × B) → List (A × B)
 insert f k v [] = (k , v) ∷ []
 insert f k v (x@(k' , v') ∷ xs) with ≡-dec-A k k'
-...                             | yes _ = (k , f v v') ∷ xs
+...                             | yes _ = (k' , f v v') ∷ xs
 ...                             | no _ = x ∷ insert f k v xs
 
-merge : (B → B → B) → Map → Map → Map
+merge : (B → B → B) → List (A × B) → List (A × B) → List (A × B)
 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'
+absurd : ∀ {a} {A : Set a} →  ⊥ → A
+absurd ()
+
+insert-keys-∈ : ∀ (f : B → B → B) (k : A) (v : B) (l : List (A × B)) → k ∈k l → keys l ≡ keys (insert f k v l)
+insert-keys-∈ f k v ((k' , v') ∷ xs) (here k≡k') with (≡-dec-A k k')
+...                                                | yes _ = refl
+...                                                | no k≢k' = absurd (k≢k' k≡k')
+insert-keys-∈ f k v ((k' , _) ∷ xs) (there k∈kxs) with (≡-dec-A k k')
+...                                                | yes _ = refl
+...                                                | no _ = cong (λ xs' → k' ∷ xs') (insert-keys-∈ f k v xs k∈kxs)
+
+Map-functional : ∀ (k : A) (v v' : B) (xs : List (A × B)) → Unique (keys ((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' xs (push k≢ _) (there k,v'∈xs) = absurd (unique-not-in xs v' (k≢ , k,v'∈xs))
     where
-        absurd : ∀ {a} {A : Set a} →  ⊥ → A
-        absurd ()
-
-        unique-not-in : ∀ (xs : List (A × B)) (v' : B) → ¬ (All (λ (k' , _) → ¬ k ≡ k') xs × (k , v') ∈ xs)
+        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)