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

Use binary operator for decidable equality consistently

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2025-01-04 19:08:28 -08:00
parent b0488c9cc6
commit d90b544436
2 changed files with 28 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
Lattice/FiniteMap.agda
View File

@ -7,11 +7,11 @@ open import Data.List using (List; _∷_; [])
module Lattice.FiniteMap {A : Set} {B : Set}
{_≈₂_ : B → B → Set}
{_⊔₂_ : B → B → B} {_⊓₂_ : B → B → B}
(≡-dec-A : IsDecidable (_≡_ {_} {A}))
(≡-Decidable-A : IsDecidable {_} {A} _≡_)
(lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
open IsLattice lB using () renaming (_≼_ to _≼₂_)
open import Lattice.Map ≡-dec-A lB as Map
open import Lattice.Map ≡-Decidable-A lB as Map
using
( Map
; ⊔-equal-keys

52
Lattice/Map.agda
View File

@ -22,7 +22,7 @@ open import Utils using (Unique; push; Unique-append; All¬-¬Any; All-x∈xs)
open import Data.String using () renaming (_++_ to _++ˢ_)
open import Showable using (Showable; show)
open IsDecidable ≡-Decidable-A using () renaming (R-dec to ≡-dec-A)
open IsDecidable ≡-Decidable-A using () renaming (R-dec to _≟ᴬ_)
open IsLattice lB using () renaming
( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym; ≈-trans to ≈₂-trans
@ -42,7 +42,7 @@ private module ImplKeys where
∈k-dec : ∀ (k : A) (l : List (A × B)) → Dec (k ∈ˡ (ImplKeys.keys l))
∈k-dec k [] = no (λ ())
∈k-dec k ((k' , v) ∷ xs)
with (≡-dec-A k k')
with (k ≟ᴬ k')
... | yes k≡k' = yes (here k≡k')
... | no k≢k' with (∈k-dec k xs)
... | yes k∈kxs = yes (there k∈kxs)
@ -77,7 +77,7 @@ private module _ where
k∈-dec : ∀ (k : A) (l : List A) → Dec (k ∈ l)
k∈-dec k [] = no (λ ())
k∈-dec k (x ∷ xs)
with (≡-dec-A k x)
with (k ≟ᴬ x)
... | yes refl = yes (here refl)
... | no k≢x with (k∈-dec k xs)
... | yes k∈xs = yes (there k∈xs)
@ -114,7 +114,7 @@ private module ImplInsert (f : B → B → B) where
insert : A → B → List (A × B) → List (A × B)
insert k v [] = (k , v) ∷ []
insert k v (x@(k' , v') ∷ xs) with ≡-dec-A k k'
insert k v (x@(k' , v') ∷ xs) with k ≟ᴬ k'
... | yes _ = (k' , f v v') ∷ xs
... | no _ = x ∷ insert k v xs
@ -124,11 +124,11 @@ private module ImplInsert (f : B → B → B) where
insert-keys-∈ : ∀ {k : A} {v : B} {l : List (A × B)} →
k ∈k l → keys l ≡ keys (insert k v l)
insert-keys-∈ {k} {v} {(k' , v') ∷ xs} (here k≡k')
with (≡-dec-A k k')
with (k ≟ᴬ k')
... | yes _ = refl
... | no k≢k' = ⊥-elim (k≢k' k≡k')
insert-keys-∈ {k} {v} {(k' , _) ∷ xs} (there k∈kxs)
with (≡-dec-A k k')
with (k ≟ᴬ k')
... | yes _ = refl
... | no _ = cong (λ xs' → k' ∷ xs') (insert-keys-∈ k∈kxs)
@ -136,7 +136,7 @@ private module ImplInsert (f : B → B → B) where
¬ (k ∈k l) → (keys l ++ (k ∷ [])) ≡ keys (insert k v l)
insert-keys-∉ {k} {v} {[]} _ = refl
insert-keys-∉ {k} {v} {(k' , v') ∷ xs} k∉kl
with (≡-dec-A k k')
with (k ≟ᴬ k')
... | yes k≡k' = ⊥-elim (k∉kl (here k≡k'))
... | no _ = cong (λ xs' → k' ∷ xs')
(insert-keys-∉ (λ k∈kxs → k∉kl (there k∈kxs)))
@ -172,7 +172,7 @@ private module ImplInsert (f : B → B → B) where
¬ k ∈k l → (k , v) ∈ insert k v l
insert-fresh {l = []} k∉kl = here refl
insert-fresh {k} {l = (k' , v') ∷ xs} k∉kl
with ≡-dec-A k k'
with k ≟ᴬ k'
... | yes k≡k' = ⊥-elim (k∉kl (here k≡k'))
... | no _ = there (insert-fresh (λ k∈kxs → k∉kl (there k∈kxs)))
@ -181,9 +181,9 @@ private module ImplInsert (f : B → B → B) where
insert-preserves-∉k {l = []} k≢k' k∉kl (here k≡k') = k≢k' k≡k'
insert-preserves-∉k {l = []} k≢k' k∉kl (there ())
insert-preserves-∉k {k} {k'} {v'} {(k'' , v'') ∷ xs} k≢k' k∉kl k∈kil
with ≡-dec-A k k''
with k ≟ᴬ k''
... | yes k≡k'' = k∉kl (here k≡k'')
... | no k≢k'' with ≡-dec-A k' k'' | k∈kil
... | no k≢k'' with k' ≟ᴬ k'' | k∈kil
... | yes k'≡k'' | here k≡k'' = k≢k'' k≡k''
... | yes k'≡k'' | there k∈kxs = k∉kl (there k∈kxs)
... | no k'≢k'' | here k≡k'' = k∉kl (here k≡k'')
@ -194,18 +194,18 @@ private module ImplInsert (f : B → B → B) where
¬ k ∈k l₁ → ¬ k ∈k l₂ → ¬ k ∈k union l₁ l₂
union-preserves-∉ {l₁ = []} _ k∉kl₂ = k∉kl₂
union-preserves-∉ {k} {(k' , v') ∷ xs₁} k∉kl₁ k∉kl₂
with ≡-dec-A k k'
with k ≟ᴬ k'
... | yes k≡k' = ⊥-elim (k∉kl₁ (here k≡k'))
... | no k≢k' = insert-preserves-∉k k≢k' (union-preserves-∉ (λ k∈kxs₁ → k∉kl₁ (there k∈kxs₁)) k∉kl₂)
insert-preserves-∈k : ∀ {k k' : A} {v' : B} {l : List (A × B)} →
k ∈k l → k ∈k insert k' v' l
insert-preserves-∈k {k} {k'} {v'} {(k'' , v'') ∷ xs} (here k≡k'')
with (≡-dec-A k' k'')
with k' ≟ᴬ k''
... | yes _ = here k≡k''
... | no _ = here k≡k''
insert-preserves-∈k {k} {k'} {v'} {(k'' , v'') ∷ xs} (there k∈kxs)
with (≡-dec-A k' k'')
with k' ≟ᴬ k''
... | yes _ = there k∈kxs
... | no _ = there (insert-preserves-∈k k∈kxs)
@ -237,11 +237,11 @@ private module ImplInsert (f : B → B → B) where
insert-preserves-∈ : ∀ {k k' : A} {v v' : B} {l : List (A × B)} →
¬ k ≡ k' → (k , v) ∈ l → (k , v) ∈ insert k' v' l
insert-preserves-∈ {k} {k'} {l = x ∷ xs} k≢k' (here k,v=x)
rewrite sym k,v=x with ≡-dec-A k' k
rewrite sym k,v=x with k' ≟ᴬ k
... | yes k'≡k = ⊥-elim (k≢k' (sym k'≡k))
... | no _ = here refl
insert-preserves-∈ {k} {k'} {l = (k'' , _) ∷ xs} k≢k' (there k,v∈xs)
with ≡-dec-A k' k''
with k' ≟ᴬ k''
... | yes _ = there k,v∈xs
... | no _ = there (insert-preserves-∈ k≢k' k,v∈xs)
@ -260,7 +260,7 @@ private module ImplInsert (f : B → B → B) where
k,v∈mxs₁l = union-preserves-∈₁ uxs₁ k,v∈xs₁ k∉kl₂
k≢k' : ¬ k ≡ k'
k≢k' with ≡-dec-A k k'
k≢k' with k ≟ᴬ k'
... | yes k≡k' rewrite k≡k' = ⊥-elim (All¬-¬Any k'≢xs₁ (∈-cong proj₁ k,v∈xs₁))
... | no k≢k' = k≢k'
union-preserves-∈₁ {l₁ = (k' , v') ∷ xs₁} (push k'≢xs₁ uxs₁) (here k,v≡k',v') k∉kl₂
@ -271,11 +271,11 @@ private module ImplInsert (f : B → B → B) where
Unique (keys l) → (k , v') ∈ l → (k , f v v') ∈ (insert k v l)
insert-combines {l = (k' , v'') ∷ xs} _ (here k,v'≡k',v'')
rewrite cong proj₁ k,v'≡k',v'' rewrite cong proj₂ k,v'≡k',v''
with ≡-dec-A k' k'
with k' ≟ᴬ k'
... | yes _ = here refl
... | no k≢k' = ⊥-elim (k≢k' refl)
insert-combines {k} {l = (k' , v'') ∷ xs} (push k'≢xs uxs) (there k,v'∈xs)
with ≡-dec-A k k'
with k ≟ᴬ k'
... | yes k≡k' rewrite k≡k' = ⊥-elim (All¬-¬Any k'≢xs (∈-cong proj₁ k,v'∈xs))
... | no k≢k' = there (insert-combines uxs k,v'∈xs)
@ -289,13 +289,13 @@ private module ImplInsert (f : B → B → B) where
insert-preserves-∈ k≢k' (union-combines uxs₁ ul₂ k,v₁∈xs₁ k,v₂∈l₂)
where
k≢k' : ¬ k ≡ k'
k≢k' with ≡-dec-A k k'
k≢k' with k ≟ᴬ k'
... | yes k≡k' rewrite k≡k' = ⊥-elim (All¬-¬Any k'≢xs₁ (∈-cong proj₁ k,v₁∈xs₁))
... | no k≢k' = k≢k'
update : A → B → List (A × B) → List (A × B)
update k v [] = []
update k v ((k' , v') ∷ xs) with ≡-dec-A k k'
update k v ((k' , v') ∷ xs) with k ≟ᴬ k'
... | yes _ = (k' , f v v') ∷ xs
... | no _ = (k' , v') ∷ update k v xs
@ -315,7 +315,7 @@ private module ImplInsert (f : B → B → B) where
keys l ≡ keys (update k v l)
update-keys {l = []} = refl
update-keys {k} {v} {l = (k' , v') ∷ xs}
with ≡-dec-A k k'
with k ≟ᴬ k'
... | yes _ = refl
... | no _ rewrite update-keys {k} {v} {xs} = refl
@ -432,11 +432,11 @@ private module ImplInsert (f : B → B → B) where
¬ k ≡ k' → (k , v) ∈ l → (k , v) ∈ update k' v' l
update-preserves-∈ {k} {k'} {v} {v'} {(k'' , v'') ∷ xs} k≢k' (here k,v≡k'',v'')
rewrite cong proj₁ k,v≡k'',v'' rewrite cong proj₂ k,v≡k'',v''
with ≡-dec-A k' k''
with k' ≟ᴬ k''
... | yes k'≡k'' = ⊥-elim (k≢k' (sym k'≡k''))
... | no _ = here refl
update-preserves-∈ {k} {k'} {v} {v'} {(k'' , v'') ∷ xs} k≢k' (there k,v∈xs)
with ≡-dec-A k' k''
with k' ≟ᴬ k''
... | yes _ = there k,v∈xs
... | no _ = there (update-preserves-∈ k≢k' k,v∈xs)
@ -450,11 +450,11 @@ private module ImplInsert (f : B → B → B) where
Unique (keys l) → (k , v) ∈ l → (k , f v' v) ∈ update k v' l
update-combines {k} {v} {v'} {(k' , v'') ∷ xs} _ (here k,v=k',v'')
rewrite cong proj₁ k,v=k',v'' rewrite cong proj₂ k,v=k',v''
with ≡-dec-A k' k'
with k' ≟ᴬ k'
... | yes _ = here refl
... | no k'≢k' = ⊥-elim (k'≢k' refl)
update-combines {k} {v} {v'} {(k' , v'') ∷ xs} (push k'≢xs uxs) (there k,v∈xs)
with ≡-dec-A k k'
with k ≟ᴬ k'
... | yes k≡k' rewrite k≡k' = ⊥-elim (All¬-¬Any k'≢xs (∈-cong proj₁ k,v∈xs))
... | no _ = there (update-combines uxs k,v∈xs)
@ -468,7 +468,7 @@ private module ImplInsert (f : B → B → B) where
update-preserves-∈ k≢k' (updates-combine uxs₁ u₂ k,v₁∈xs k,v₂∈l₂)
where
k≢k' : ¬ k ≡ k'
k≢k' with ≡-dec-A k k'
k≢k' with k ≟ᴬ k'
... | yes k≡k' rewrite k≡k' = ⊥-elim (All¬-¬Any k'≢xs (∈-cong proj₁ k,v₁∈xs))
... | no k≢k' = k≢k'