Compare commits

..

11 Commits

Author SHA1 Message Date
45f2babfa3 Fix typo in FixedHeightLattice definition
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-11 15:37:00 -08:00
16c4d13242 Prove that iterated products are finite height
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-11 15:36:12 -08:00
0ba4b46e16 Add proof of decidable equivalence for products
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-11 15:35:50 -08:00
7e5cc1b316 Add an 'iterated product' lattice for A x A ... x A x B.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-11 14:19:41 -08:00
33b7bc37f0 Add a 'FiniteHeightLattice' bundle
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-11 14:19:41 -08:00
6fe8dc2a02 Add an 'iterate' function to Utils
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-11 14:19:41 -08:00
ec31333e9a Add a 'Finite Map' lattice
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-11 14:19:41 -08:00
ad26d20274 Add facts about equal-key maps
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-11 12:45:43 -08:00
2b27e397b6 Add another utility proof
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-11 12:45:33 -08:00
d718338759 Clean up 'Map' to hide implementation details, extract code
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-10 16:51:43 -08:00
1b8c88b1a2 Expose only a 'public' "keys" function from Map
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-10 16:35:21 -08:00
6 changed files with 342 additions and 68 deletions

View File

@ -145,3 +145,14 @@ record Lattice {a} (A : Set a) : Set (lsuc a) where
isLattice : IsLattice A _≈_ _⊔_ _⊓_
open IsLattice isLattice public
record FiniteHeightLattice {a} (A : Set a) : Set (lsuc a) where
field
height :
_≈_ : A A Set a
_⊔_ : A A A
_⊓_ : A A A
isFiniteHeightLattice : IsFiniteHeightLattice A height _≈_ _⊔_ _⊓_
open IsFiniteHeightLattice isFiniteHeightLattice public

78
Lattice/FiniteMap.agda Normal file
View File

@ -0,0 +1,78 @@
open import Lattice
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
open import Relation.Binary.Definitions using (Decidable)
open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔_)
open import Data.List using (List)
module Lattice.FiniteMap {a b : Level} (A : Set a) (B : Set b)
(_≈₂_ : B B Set b)
(_⊔₂_ : B B B) (_⊓₂_ : B B B)
(≡-dec-A : Decidable (_≡_ {a} {A}))
(lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB as Map
using (Map; ⊔-equal-keys; ⊓-equal-keys)
renaming
( _≈_ to _≈ᵐ_
; _⊔_ to _⊔ᵐ_
; _⊓_ to _⊓ᵐ_
; ≈-equiv to ≈ᵐ-equiv
; ≈-⊔-cong to ≈ᵐ-⊔ᵐ-cong
; ⊔-assoc to ⊔ᵐ-assoc
; ⊔-comm to ⊔ᵐ-comm
; ⊔-idemp to ⊔ᵐ-idemp
; ≈-⊓-cong to ≈ᵐ-⊓ᵐ-cong
; ⊓-assoc to ⊓ᵐ-assoc
; ⊓-comm to ⊓ᵐ-comm
; ⊓-idemp to ⊓ᵐ-idemp
; absorb-⊔-⊓ to absorb-⊔ᵐ-⊓ᵐ
; absorb-⊓-⊔ to absorb-⊓ᵐ-⊔ᵐ
)
open import Data.Product using (_×_; _,_; Σ; proj₁ ; proj₂)
open import Equivalence
module _ (ks : List A) where
FiniteMap : Set (a ⊔ℓ b)
FiniteMap = Σ Map (λ m Map.keys m ks)
_≈_ : FiniteMap FiniteMap Set (a ⊔ℓ b)
_≈_ (m₁ , _) (m₂ , _) = m₁ ≈ᵐ m₂
_⊔_ : FiniteMap FiniteMap FiniteMap
_⊔_ (m₁ , km₁≡ks) (m₂ , km₂≡ks) = (m₁ ⊔ᵐ m₂ , trans (sym (⊔-equal-keys {m₁} {m₂} (trans (km₁≡ks) (sym km₂≡ks)))) km₁≡ks)
_⊓_ : FiniteMap FiniteMap FiniteMap
_⊓_ (m₁ , km₁≡ks) (m₂ , km₂≡ks) = (m₁ ⊓ᵐ m₂ , trans (sym (⊓-equal-keys {m₁} {m₂} (trans (km₁≡ks) (sym km₂≡ks)))) km₁≡ks)
≈-equiv : IsEquivalence FiniteMap _≈_
≈-equiv = record
{ ≈-refl = λ {(m , _)} IsEquivalence.≈-refl ≈ᵐ-equiv {m}
; ≈-sym = λ {(m₁ , _)} {(m₂ , _)} IsEquivalence.≈-sym ≈ᵐ-equiv {m₁} {m₂}
; ≈-trans = λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} IsEquivalence.≈-trans ≈ᵐ-equiv {m₁} {m₂} {m₃}
}
isUnionSemilattice : IsSemilattice FiniteMap _≈_ _⊔_
isUnionSemilattice = record
{ ≈-equiv = ≈-equiv
; ≈-⊔-cong = λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} {(m₄ , _)} m₁≈m₂ m₃≈m₄ ≈ᵐ-⊔ᵐ-cong {m₁} {m₂} {m₃} {m₄} m₁≈m₂ m₃≈m₄
; ⊔-assoc = λ (m₁ , _) (m₂ , _) (m₃ , _) ⊔ᵐ-assoc m₁ m₂ m₃
; ⊔-comm = λ (m₁ , _) (m₂ , _) ⊔ᵐ-comm m₁ m₂
; ⊔-idemp = λ (m , _) ⊔ᵐ-idemp m
}
isIntersectSemilattice : IsSemilattice FiniteMap _≈_ _⊓_
isIntersectSemilattice = record
{ ≈-equiv = ≈-equiv
; ≈-⊔-cong = λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} {(m₄ , _)} m₁≈m₂ m₃≈m₄ ≈ᵐ-⊓ᵐ-cong {m₁} {m₂} {m₃} {m₄} m₁≈m₂ m₃≈m₄
; ⊔-assoc = λ (m₁ , _) (m₂ , _) (m₃ , _) ⊓ᵐ-assoc m₁ m₂ m₃
; ⊔-comm = λ (m₁ , _) (m₂ , _) ⊓ᵐ-comm m₁ m₂
; ⊔-idemp = λ (m , _) ⊓ᵐ-idemp m
}
isLattice : IsLattice FiniteMap _≈_ _⊔_ _⊓_
isLattice = record
{ joinSemilattice = isUnionSemilattice
; meetSemilattice = isIntersectSemilattice
; absorb-⊔-⊓ = λ (m₁ , _) (m₂ , _) absorb-⊔ᵐ-⊓ᵐ m₁ m₂
; absorb-⊓-⊔ = λ (m₁ , _) (m₂ , _) absorb-⊓ᵐ-⊔ᵐ m₁ m₂
}

107
Lattice/IterProd.agda Normal file
View File

@ -0,0 +1,107 @@
open import Lattice
module Lattice.IterProd {a} {A B : Set a}
(_≈₁_ : A A Set a) (_≈₂_ : B B Set a)
(_⊔₁_ : A A A) (_⊔₂_ : B B B)
(_⊓₁_ : A A A) (_⊓₂_ : B B B)
(lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
open import Agda.Primitive using (lsuc)
open import Data.Nat using (; suc; _+_)
open import Data.Product using (_×_)
open import Utils using (iterate)
open IsLattice lA renaming (FixedHeight to FixedHeight₁)
open IsLattice lB renaming (FixedHeight to FixedHeight₂)
IterProd : Set a
IterProd k = iterate k (λ t A × t) B
-- To make iteration more convenient, package the definitions in Lattice
-- records, perform the recursion, and unpackage.
private module _ where
BLattice : Lattice B
BLattice = record
{ _≈_ = _≈₂_
; _⊔_ = _⊔₂_
; _⊓_ = _⊓₂_
; isLattice = lB
}
IterProdLattice : {k : } Lattice (IterProd k)
IterProdLattice {0} = BLattice
IterProdLattice {suc k'} = record
{ _≈_ = _≈_
; _⊔_ = _⊔_
; _⊓_ = _⊓_
; isLattice = isLattice
}
where
Right : Lattice (IterProd k')
Right = IterProdLattice {k'}
open import Lattice.Prod
_≈₁_ (Lattice._≈_ Right)
_⊔₁_ (Lattice._⊔_ Right)
_⊓₁_ (Lattice._⊓_ Right)
lA (Lattice.isLattice Right)
module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
(h₁ h₂ : )
(fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where
private module _ where
record FiniteHeightAndDecEq (A : Set a) : Set (lsuc a) where
field
height :
_≈_ : A A Set a
_⊔_ : A A A
_⊓_ : A A A
isFiniteHeightLattice : IsFiniteHeightLattice A height _≈_ _⊔_ _⊓_
≈-dec : IsDecidable _≈_
open IsFiniteHeightLattice isFiniteHeightLattice public
BFiniteHeightLattice : FiniteHeightAndDecEq B
BFiniteHeightLattice = record
{ height = h₂
; _≈_ = _≈₂_
; _⊔_ = _⊔₂_
; _⊓_ = _⊓₂_
; isFiniteHeightLattice = record
{ isLattice = lB
; fixedHeight = fhB
}
; ≈-dec = ≈₂-dec
}
IterProdFiniteHeightLattice : {k : } FiniteHeightAndDecEq (IterProd k)
IterProdFiniteHeightLattice {0} = BFiniteHeightLattice
IterProdFiniteHeightLattice {suc k'} = record
{ height = h₁ + FiniteHeightAndDecEq.height Right
; _≈_ = _≈_
; _⊔_ = _⊔_
; _⊓_ = _⊓_
; isFiniteHeightLattice = isFiniteHeightLattice
≈₁-dec (FiniteHeightAndDecEq.≈-dec Right)
h₁ (FiniteHeightAndDecEq.height Right)
fhA (IsFiniteHeightLattice.fixedHeight (FiniteHeightAndDecEq.isFiniteHeightLattice Right))
; ≈-dec = ≈-dec ≈₁-dec (FiniteHeightAndDecEq.≈-dec Right)
}
where
Right = IterProdFiniteHeightLattice {k'}
open import Lattice.Prod
_≈₁_ (FiniteHeightAndDecEq._≈_ Right)
_⊔₁_ (FiniteHeightAndDecEq._⊔_ Right)
_⊓₁_ (FiniteHeightAndDecEq._⊓_ Right)
lA (FiniteHeightAndDecEq.isLattice Right)
module _ (k : ) where
open FiniteHeightAndDecEq (IterProdFiniteHeightLattice {k}) using (fixedHeight) public
-- Expose the computed definition in public.
module _ (k : ) where
open Lattice.Lattice (IterProdLattice {k}) public

View File

@ -19,6 +19,7 @@ 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 (⊥; ⊥-elim)
open import Equivalence
open import Utils using (Unique; push; empty; Unique-append; All¬-¬Any; All-x∈xs)
open IsLattice lB using () renaming
( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym; ≈-trans to ≈₂-trans
@ -28,35 +29,13 @@ open IsLattice lB using () renaming
; absorb-⊔-⊓ to absorb-⊔₂-⊓₂; absorb-⊓-⊔ to absorb-⊓₂-⊔₂
)
keys : List (A × B) List A
keys = map proj₁
data Unique {c} {C : Set c} : List C Set c where
empty : Unique []
push : {x : C} {xs : List C}
All (λ x' ¬ x x') xs
Unique xs
Unique (x xs)
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')
where
x'≢x : ¬ x' x
x'≢x x'≡x = x∉xs (here (sym x'≡x))
help : {l : List C} All (λ x'' ¬ x' x'') l All (λ x'' ¬ x' x'') (l ++ (x []))
help {[]} _ = x'≢x []
help {e es} (x'≢e x'≢es) = x'≢e help x'≢es
All¬-¬Any : {p c} {C : Set c} {P : C Set p} {l : List C} All (λ x ¬ P x) l ¬ Any P l
All¬-¬Any {l = x xs} (¬Px _) (here Px) = ¬Px Px
All¬-¬Any {l = x xs} (_ ¬Pxs) (there Pxs) = All¬-¬Any ¬Pxs Pxs
private module ImplKeys where
keys : List (A × B) List A
keys = map proj₁
private module _ where
open MemProp using (_∈_)
open ImplKeys
unique-not-in : {k : A} {v : B} {l : List (A × B)}
¬ (All (λ k' ¬ k k') (keys l) × (k , v) l)
@ -108,6 +87,7 @@ private module ImplRelation where
private module ImplInsert (f : B B B) where
open import Data.List using (map)
open MemProp using (_∈_)
open ImplKeys
private
_∈k_ : A List (A × B) Set a
@ -153,6 +133,20 @@ private module ImplInsert (f : B → B → B) where
... | yes k∈kl rewrite insert-keys-∈ {v = v} k∈kl = u
... | no k∉kl rewrite sym (insert-keys-∉ {v = v} k∉kl) = Unique-append k∉kl u
union-subset-keys : {l₁ l₂ : List (A × B)}
All (λ k k ∈k l₂) (keys l₁)
keys l₂ keys (union l₁ l₂)
union-subset-keys {[]} _ = refl
union-subset-keys {(k , v) l₁'} (k∈kl₂ kl₁'⊆kl₂)
rewrite union-subset-keys kl₁'⊆kl₂ =
insert-keys-∈ k∈kl₂
union-equal-keys : {l₁ l₂ : List (A × B)}
keys l₁ keys l₂ keys l₁ keys (union l₁ l₂)
union-equal-keys {l₁} {l₂} kl₁≡kl₂
with subst (λ l All (λ k k l) (keys l₁)) kl₁≡kl₂ (All-x∈xs (keys l₁))
... | kl₁⊆kl₂ = trans kl₁≡kl₂ (union-subset-keys {l₁} {l₂} kl₁⊆kl₂)
union-preserves-Unique : (l₁ l₂ : List (A × B))
Unique (keys l₂) Unique (keys (union l₁ l₂))
union-preserves-Unique [] l₂ u₂ = u₂
@ -366,6 +360,29 @@ private module ImplInsert (f : B → B → B) where
let (k∈kl₁ , k∈kxs) = restrict-needs-both k∈l₁xs
in (k∈kl₁ , there k∈kxs)
restrict-subset-keys : {l₁ l₂ : List (A × B)}
All (λ k k ∈k l₁) (keys l₂)
keys l₂ keys (restrict l₁ l₂)
restrict-subset-keys {l₁} {[]} _ = refl
restrict-subset-keys {l₁} {(k , v) l₂'} (k∈kl₁ kl₂'⊆kl₁)
with ∈k-dec k l₁
... | no k∉kl₁ = ⊥-elim (k∉kl₁ k∈kl₁)
... | yes _ rewrite restrict-subset-keys {l₁} {l₂'} kl₂'⊆kl₁ = refl
restrict-equal-keys : {l₁ l₂ : List (A × B)}
keys l₁ keys l₂
keys l₁ keys (restrict l₁ l₂)
restrict-equal-keys {l₁} {l₂} kl₁≡kl₂
with subst (λ l All (λ k k l) (keys l₂)) (sym kl₁≡kl₂) (All-x∈xs (keys l₂))
... | kl₂⊆kl₁ = trans kl₁≡kl₂ (restrict-subset-keys {l₁} {l₂} kl₂⊆kl₁)
intersect-equal-keys : {l₁ l₂ : List (A × B)}
keys l₁ keys l₂
keys l₁ keys (intersect l₁ l₂)
intersect-equal-keys {l₁} {l₂} kl₁≡kl₂
rewrite restrict-equal-keys (trans kl₁≡kl₂ (updates-keys {l₁} {l₂}))
rewrite updates-keys {l₁} {l₂} = refl
restrict-preserves-∉₁ : {k : A} {l₁ l₂ : List (A × B)}
¬ k ∈k l₁ ¬ k ∈k restrict l₁ l₂
restrict-preserves-∉₁ {k} {l₁} {l₂} k∉kl₁ k∈kl₁l₂ =
@ -448,13 +465,16 @@ private module ImplInsert (f : B → B → B) where
Map : Set (a ⊔ℓ b)
Map = Σ (List (A × B)) (λ l Unique (keys l))
Map = Σ (List (A × B)) (λ l Unique (ImplKeys.keys l))
keys : Map List A
keys (kvs , _) = ImplKeys.keys kvs
_∈_ : (A × B) Map Set (a ⊔ℓ b)
_∈_ p (kvs , _) = MemProp._∈_ p kvs
_∈k_ : A Map Set a
_∈k_ k (kvs , _) = MemProp._∈_ k (keys kvs)
_∈k_ k m = MemProp._∈_ k (keys m)
Map-functional : {k : A} {v v' : B} {m : Map} (k , v) m (k , v') m v v'
Map-functional {m = (l , ul)} k,v∈m k,v'∈m = ListAB-functional ul k,v∈m k,v'∈m
@ -492,8 +512,8 @@ data Expr : Set (a ⊔ℓ b) where
__ : Expr Expr Expr
_∩_ : Expr Expr Expr
open ImplInsert _⊔₂_ using (union-preserves-Unique) renaming (insert to insert-impl; union to union-impl)
open ImplInsert _⊓₂_ using (intersect-preserves-Unique) renaming (intersect to intersect-impl)
open ImplInsert _⊔₂_ using (union-preserves-Unique; union-equal-keys) renaming (insert to insert-impl; union to union-impl)
open ImplInsert _⊓₂_ using (intersect-preserves-Unique; intersect-equal-keys) renaming (intersect to intersect-impl)
_⊔_ : Map Map Map
_⊔_ (kvs₁ , _) (kvs₂ , uks₂) = (union-impl kvs₁ kvs₂ , union-preserves-Unique kvs₁ kvs₂ uks₂)
@ -553,45 +573,46 @@ Expr-Provenance k (e₁ ∩ e₂) k∈ke₁e₂
... | no k∉ke₁ | yes k∈ke₂ = ⊥-elim (intersect-preserves-∉₁ {l₂ = proj₁ e₂ } k∉ke₁ k∈ke₁e₂)
... | no k∉ke₁ | no k∉ke₂ = ⊥-elim (intersect-preserves-∉₂ {l₁ = proj₁ e₁ } k∉ke₂ k∈ke₁e₂)
data SubsetInfo (m₁ m₂ : Map) : Set (a ⊔ℓ b) where
extra : (k : A) k ∈k m₁ ¬ k ∈k m₂ SubsetInfo m₁ m₂
mismatch : (k : A) (v₁ v₂ : B) (k , v₁) m₁ (k , v₂) m₂ ¬ v₁ ≈₂ v₂ SubsetInfo m₁ m₂
fine : m₁ m₂ SubsetInfo m₁ m₂
SubsetInfo-to-dec : {m₁ m₂ : Map} SubsetInfo m₁ m₂ Dec (m₁ m₂)
SubsetInfo-to-dec (extra k k∈km₁ k∉km₂) =
let (v , k,v∈m₁) = locate k∈km₁
in no (λ m₁⊆m₂
let (v' , (_ , k,v'∈m₂)) = m₁⊆m₂ k v k,v∈m₁
in k∉km₂ (∈-cong proj₁ k,v'∈m₂))
SubsetInfo-to-dec {m₁} {m₂} (mismatch k v₁ v₂ k,v₁∈m₁ k,v₂∈m₂ v₁̷≈v₂) =
no (λ m₁⊆m₂
let (v' , (v₁≈v' , k,v'∈m₂)) = m₁⊆m₂ k v₁ k,v₁∈m₁
in v₁̷≈v₂ (subst (λ v'' v₁ ≈₂ v'') (Map-functional {k} {v'} {v₂} {m₂} k,v'∈m₂ k,v₂∈m₂) v₁≈v')) -- for some reason, can't just use subst...
SubsetInfo-to-dec (fine m₁⊆m₂) = yes m₁⊆m₂
module _ (≈₂-dec : (b₁ b₂ : B) Dec (b₁ ≈₂ b₂)) where
compute-SubsetInfo : m₁ m₂ SubsetInfo m₁ m₂
compute-SubsetInfo ([] , _) m₂ = fine (λ k v ())
compute-SubsetInfo m₁@((k , v) xs₁ , push k≢xs₁ uxs₁) m₂@(l₂ , u₂)
with compute-SubsetInfo (xs₁ , uxs₁) m₂
... | extra k' k'∈kxs₁ k'∉km₂ = extra k' (there k'∈kxs₁) k'∉km₂
... | mismatch k' v₁ v₂ k',v₁∈xs₁ k',v₂∈m₂ v₁̷≈v₂ =
mismatch k' v₁ v₂ (there k',v₁∈xs₁) k',v₂∈m₂ v₁̷≈v₂
... | fine xs₁⊆m₂ with ∈k-dec k l₂
... | no k∉km₂ = extra k (here refl) k∉km₂
... | yes k∈km₂ with locate k∈km₂
... | (v' , k,v'∈m₂) with ≈₂-dec v v'
... | no v̷≈v' = mismatch k v v' (here refl) (k,v'∈m₂) v̷≈v'
... | yes v≈v' = fine m₁⊆m₂
where
m₁⊆m₂ : m₁ m₂
m₁⊆m₂ k' v'' (here k,v≡k',v'')
rewrite cong proj₁ k,v≡k',v''
rewrite cong proj₂ k,v≡k',v'' =
(v' , (v≈v' , k,v'∈m₂))
m₁⊆m₂ k' v'' (there k,v≡k',v'') =
xs₁⊆m₂ k' v'' k,v≡k',v''
private module _ where
data SubsetInfo (m₁ m₂ : Map) : Set (a ⊔ℓ b) where
extra : (k : A) k ∈k m₁ ¬ k ∈k m₂ SubsetInfo m₁ m₂
mismatch : (k : A) (v₁ v₂ : B) (k , v₁) m₁ (k , v₂) m₂ ¬ v₁ ≈₂ v₂ SubsetInfo m₁ m₂
fine : m₁ m₂ SubsetInfo m₁ m₂
SubsetInfo-to-dec : {m₁ m₂ : Map} SubsetInfo m₁ m₂ Dec (m₁ m₂)
SubsetInfo-to-dec (extra k k∈km₁ k∉km₂) =
let (v , k,v∈m₁) = locate k∈km₁
in no (λ m₁⊆m₂
let (v' , (_ , k,v'∈m₂)) = m₁⊆m₂ k v k,v∈m₁
in k∉km₂ (∈-cong proj₁ k,v'∈m₂))
SubsetInfo-to-dec {m₁} {m₂} (mismatch k v₁ v₂ k,v₁∈m₁ k,v₂∈m₂ v₁̷≈v₂) =
no (λ m₁⊆m₂
let (v' , (v₁≈v' , k,v'∈m₂)) = m₁⊆m₂ k v₁ k,v₁∈m₁
in v₁̷≈v₂ (subst (λ v'' v₁ ≈₂ v'') (Map-functional {k} {v'} {v₂} {m₂} k,v'∈m₂ k,v₂∈m₂) v₁≈v')) -- for some reason, can't just use subst...
SubsetInfo-to-dec (fine m₁⊆m₂) = yes m₁⊆m₂
compute-SubsetInfo : m₁ m₂ SubsetInfo m₁ m₂
compute-SubsetInfo ([] , _) m₂ = fine (λ k v ())
compute-SubsetInfo m₁@((k , v) xs₁ , push k≢xs₁ uxs₁) m₂@(l₂ , u₂)
with compute-SubsetInfo (xs₁ , uxs₁) m₂
... | extra k' k'∈kxs₁ k'∉km₂ = extra k' (there k'∈kxs₁) k'∉km₂
... | mismatch k' v₁ v₂ k',v₁∈xs₁ k',v₂∈m₂ v₁̷≈v₂ =
mismatch k' v₁ v₂ (there k',v₁∈xs₁) k',v₂∈m₂ v₁̷≈v₂
... | fine xs₁⊆m₂ with ∈k-dec k l₂
... | no k∉km₂ = extra k (here refl) k∉km₂
... | yes k∈km₂ with locate k∈km₂
... | (v' , k,v'∈m₂) with ≈₂-dec v v'
... | no v̷≈v' = mismatch k v v' (here refl) (k,v'∈m₂) v̷≈v'
... | yes v≈v' = fine m₁⊆m₂
where
m₁⊆m₂ : m₁ m₂
m₁⊆m₂ k' v'' (here k,v≡k',v'')
rewrite cong proj₁ k,v≡k',v''
rewrite cong proj₂ k,v≡k',v'' =
(v' , (v≈v' , k,v'∈m₂))
m₁⊆m₂ k' v'' (there k,v≡k',v'') =
xs₁⊆m₂ k' v'' k,v≡k',v''
⊆-dec : m₁ m₂ Dec (m₁ m₂)
⊆-dec m₁ m₂ = SubsetInfo-to-dec (compute-SubsetInfo m₁ m₂)
@ -860,3 +881,9 @@ isLattice = record
; absorb-⊔-⊓ = absorb-⊔-⊓
; absorb-⊓-⊔ = absorb-⊓-⊔
}
⊔-equal-keys : {m₁ m₂ : Map} keys m₁ keys m₂ keys m₁ keys (m₁ m₂)
⊔-equal-keys km₁≡km₂ = union-equal-keys km₁≡km₂
⊓-equal-keys : {m₁ m₂ : Map} keys m₁ keys m₂ keys m₁ keys (m₁ m₂)
⊓-equal-keys km₁≡km₂ = intersect-equal-keys km₁≡km₂

View File

@ -94,6 +94,16 @@ isLattice = record
)
}
module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) where
≈-dec : IsDecidable _≈_
≈-dec (a₁ , b₁) (a₂ , b₂)
with ≈₁-dec a₁ a₂ | ≈₂-dec b₁ b₂
... | yes a₁≈a₂ | yes b₁≈b₂ = yes (a₁≈a₂ , b₁≈b₂)
... | no a₁̷≈a₂ | _ = no (λ (a₁≈a₂ , _) a₁̷≈a₂ a₁≈a₂)
... | _ | no b₁̷≈b₂ = no (λ (_ , b₁≈b₂) b₁̷≈b₂ b₁≈b₂)
module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
(h₁ h₂ : )
(fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where

41
Utils.agda Normal file
View File

@ -0,0 +1,41 @@
module Utils where
open import Data.Nat using (; suc)
open import Data.List using (List; []; _∷_; _++_)
open import Data.List.Membership.Propositional using (_∈_)
open import Data.List.Relation.Unary.All using (All; []; _∷_; map)
open import Data.List.Relation.Unary.Any using (Any; here; there) -- TODO: re-export these with nicer names from map
open import Relation.Binary.PropositionalEquality using (_≡_; sym; refl)
open import Relation.Nullary using (¬_)
data Unique {c} {C : Set c} : List C Set c where
empty : Unique []
push : {x : C} {xs : List C}
All (λ x' ¬ x x') xs
Unique xs
Unique (x xs)
Unique-append : {c} {C : Set c} {x : C} {xs : List C}
¬ 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')
where
x'≢x : ¬ x' x
x'≢x x'≡x = x∉xs (here (sym x'≡x))
help : {l : List C} All (λ x'' ¬ x' x'') l All (λ x'' ¬ x' x'') (l ++ (x []))
help {[]} _ = x'≢x []
help {e es} (x'≢e x'≢es) = x'≢e help x'≢es
All¬-¬Any : {p c} {C : Set c} {P : C Set p} {l : List C} All (λ x ¬ P x) l ¬ Any P l
All¬-¬Any {l = x xs} (¬Px _) (here Px) = ¬Px Px
All¬-¬Any {l = x xs} (_ ¬Pxs) (there Pxs) = All¬-¬Any ¬Pxs Pxs
All-x∈xs : {a} {A : Set a} (xs : List A) All (λ x x xs) xs
All-x∈xs [] = []
All-x∈xs (x xs') = here refl map there (All-x∈xs xs')
iterate : {a} {A : Set a} (n : ) (f : A A) A A
iterate 0 _ a = a
iterate (suc n) f a = f (iterate n f a)