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

Implement the more powerful Map-functional theorem

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2023-07-25 18:22:24 -07:00
parent c9ab1152c4
commit 88a712fa98
1 changed files with 11 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
Map.agda
View File

@ -1,4 +1,4 @@
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; cong) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong)
open import Relation.Binary.Definitions using (Decidable) open import Relation.Binary.Definitions using (Decidable)
open import Relation.Binary.Core using (Rel) open import Relation.Binary.Core using (Rel)
open import Relation.Nullary using (Dec; yes; no) open import Relation.Nullary using (Dec; yes; no)
@ -105,13 +105,10 @@ private module ImplInsert (f : B → B → B) where
merge-preserves-unique [] l₂ u₂ = u₂ 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₂) 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' private
-- Map-functional k v v' _ _ (here k,v'≡k,v) = sym (cong proj₂ k,v'≡k,v) unique-not-in : ∀ {k : A} {v : B} {l : List (A × B)} → ¬ (All (λ k' → ¬ k ≡ k') (keys l) × MemProp._∈_ (k , v) l)
-- Map-functional k v v' xs (push k≢ _) (there k,v'∈xs) = absurd (unique-not-in xs v' (k≢ , k,v'∈xs)) unique-not-in {l = (k' , _) ∷ xs} (k≢k' ∷ _ , here k',≡x) = k≢k' (cong proj₁ k',≡x)
-- where unique-not-in {l = _ ∷ xs} (_ ∷ rest , there k,v'∈xs) = unique-not-in (rest , 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)
module _ (f : B → B → B) where module _ (f : B → B → B) where
open ImplInsert f renaming open ImplInsert f renaming
@ -134,3 +131,9 @@ module _ (_≈_ : B → B → Set b) where
lift : Map → Map → Set (a ⊔ b) lift : Map → Map → Set (a ⊔ b)
lift m₁ m₂ = subset m₁ m₂ × subset m₂ m₁ lift m₁ m₂ = subset m₁ m₂ × subset m₂ m₁
Map-functional : ∀ {k : A} {v v' : B} {m : Map} → (k , v) ∈ m → (k , v') ∈ m → v ≡ v'
Map-functional (here k,v≡x) (here k,v'≡x) = cong proj₂ (trans k,v≡x (sym k,v'≡x))
Map-functional {m = (_ , push k≢xs _)} (here k,v≡x) (there k,v'∈xs) rewrite sym k,v≡x = absurd (unique-not-in (k≢xs , k,v'∈xs))
Map-functional {m = (_ , push k≢xs _)} (there k,v∈xs) (here k,v'≡x) rewrite sym k,v'≡x = absurd (unique-not-in (k≢xs , k,v∈xs))
Map-functional {m = (_ ∷ xs , push _ uxs)} (there k,v∈xs) (there k,v'∈xs) = Map-functional {m = (xs , uxs)} k,v∈xs k,v'∈xs