Compare commits
No commits in common. "332b7616cf08989d24f8bf470d46bf6564f0e0d6" and "48983c55b1fb4e371596feafdcd208f8824222ca" have entirely different histories.
332b7616cf
...
48983c55b1
30
Lattice.agda
30
Lattice.agda
|
|
@ -85,20 +85,6 @@ record IsSemilattice {a} (A : Set a)
|
|||
≼-refl : ∀ (a : A) → a ≼ a
|
||||
≼-refl a = ⊔-idemp a
|
||||
|
||||
≼-trans : ∀ {a₁ a₂ a₃ : A} → a₁ ≼ a₂ → a₂ ≼ a₃ → a₁ ≼ a₃
|
||||
≼-trans {a₁} {a₂} {a₃} a₁≼a₂ a₂≼a₃ =
|
||||
begin
|
||||
a₁ ⊔ a₃
|
||||
∼⟨ ≈-⊔-cong ≈-refl (≈-sym a₂≼a₃) ⟩
|
||||
a₁ ⊔ (a₂ ⊔ a₃)
|
||||
∼⟨ ≈-sym (⊔-assoc _ _ _) ⟩
|
||||
(a₁ ⊔ a₂) ⊔ a₃
|
||||
∼⟨ ≈-⊔-cong a₁≼a₂ ≈-refl ⟩
|
||||
a₂ ⊔ a₃
|
||||
∼⟨ a₂≼a₃ ⟩
|
||||
a₃
|
||||
∎
|
||||
|
||||
≼-cong : ∀ {a₁ a₂ a₃ a₄ : A} → a₁ ≈ a₂ → a₃ ≈ a₄ → a₁ ≼ a₃ → a₂ ≼ a₄
|
||||
≼-cong {a₁} {a₂} {a₃} {a₄} a₁≈a₂ a₃≈a₄ a₁⊔a₃≈a₃ =
|
||||
begin
|
||||
|
|
@ -132,24 +118,11 @@ module _ {a b} {A : Set a} {B : Set b}
|
|||
(lA : IsSemilattice A _≈₁_ _⊔₁_) (lB : IsSemilattice B _≈₂_ _⊔₂_) where
|
||||
|
||||
open IsSemilattice lA using () renaming (_≼_ to _≼₁_)
|
||||
open IsSemilattice lB using () renaming (_≼_ to _≼₂_; ⊔-idemp to ⊔₂-idemp; ≼-trans to ≼₂-trans)
|
||||
open IsSemilattice lB using () renaming (_≼_ to _≼₂_; ⊔-idemp to ⊔₂-idemp)
|
||||
|
||||
const-Mono : ∀ (x : B) → Monotonic _≼₁_ _≼₂_ (λ _ → x)
|
||||
const-Mono x _ = ⊔₂-idemp x
|
||||
|
||||
open import Data.List as List using (List; foldr; _∷_)
|
||||
open import Utils using (Pairwise; _∷_)
|
||||
|
||||
foldr-Mono : ∀ (l₁ l₂ : List A) (f : A → B → B) (b₁ b₂ : B) →
|
||||
Pairwise _≼₁_ l₁ l₂ → b₁ ≼₂ b₂ →
|
||||
(∀ b → Monotonic _≼₁_ _≼₂_ (λ a → f a b)) →
|
||||
(∀ a → Monotonic _≼₂_ _≼₂_ (f a)) →
|
||||
foldr f b₁ l₁ ≼₂ foldr f b₂ l₂
|
||||
foldr-Mono List.[] List.[] f b₁ b₂ _ b₁≼b₂ _ _ = b₁≼b₂
|
||||
foldr-Mono (x ∷ xs) (y ∷ ys) f b₁ b₂ (x≼y ∷ xs≼ys) b₁≼b₂ f-Mono₁ f-Mono₂ =
|
||||
≼₂-trans (f-Mono₁ (foldr f b₁ xs) x≼y)
|
||||
(f-Mono₂ y (foldr-Mono xs ys f b₁ b₂ xs≼ys b₁≼b₂ f-Mono₁ f-Mono₂))
|
||||
|
||||
record IsLattice {a} (A : Set a)
|
||||
(_≈_ : A → A → Set a)
|
||||
(_⊔_ : A → A → A)
|
||||
|
|
@ -173,7 +146,6 @@ record IsLattice {a} (A : Set a)
|
|||
; _≼_ to _≽_
|
||||
; _≺_ to _≻_
|
||||
; ≼-refl to ≽-refl
|
||||
; ≼-trans to ≽-trans
|
||||
)
|
||||
|
||||
FixedHeight : ∀ (h : ℕ) → Set a
|
||||
|
|
|
|||
|
|
@ -36,7 +36,6 @@ open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB
|
|||
; _∈_
|
||||
; Map-functional
|
||||
; Expr-Provenance
|
||||
; Expr-Provenance-≡
|
||||
; _∩_; _∪_; `_
|
||||
; in₁; in₂; bothᵘ; single
|
||||
; ⊔-combines
|
||||
|
|
@ -185,7 +184,7 @@ module IterProdIsomorphism where
|
|||
narrow₂ {fm₁} {fm₂ = (_ ∷ fm'₂ , push k≢ks _) , kvs≡ks@refl} kvs₁⊆kvs₂ k' v' k',v'∈fm'₁
|
||||
with kvs₁⊆kvs₂ k' v' k',v'∈fm'₁
|
||||
... | (v'' , (v'≈v'' , here refl)) rewrite sym (proj₂ fm₁) =
|
||||
⊥-elim (All¬-¬Any k≢ks (forget k',v'∈fm'₁))
|
||||
⊥-elim (All¬-¬Any k≢ks (forget {m = proj₁ fm₁} k',v'∈fm'₁))
|
||||
... | (v'' , (v'≈v'' , there k',v'∈fm'₂)) =
|
||||
(v'' , (v'≈v'' , k',v'∈fm'₂))
|
||||
|
||||
|
|
@ -196,7 +195,7 @@ module IterProdIsomorphism where
|
|||
k,v∈pop⇒k,v∈ : ∀ {k : A} {ks : List A} {k' : A} {v : B} (fm : FiniteMap (k ∷ ks)) →
|
||||
(k' , v) ∈ᵐ pop fm → (¬ k ≡ k' × ((k' , v) ∈ᵐ fm))
|
||||
k,v∈pop⇒k,v∈ {k} {ks} {k'} {v} (m@((k , _) ∷ fm' , push k≢ks uks') , refl) k',v∈fm =
|
||||
( (λ { refl → All¬-¬Any k≢ks (forget k',v∈fm) })
|
||||
( (λ { refl → All¬-¬Any k≢ks (forget {m = (fm' , uks')} k',v∈fm) })
|
||||
, there k',v∈fm
|
||||
)
|
||||
|
||||
|
|
@ -213,16 +212,17 @@ module IterProdIsomorphism where
|
|||
Provenance-union : ∀ {ks : List A} (fm₁ fm₂ : FiniteMap ks) {k : A} {v : B} →
|
||||
(k , v) ∈ᵐ (fm₁ ⊔ᵐ fm₂) → FromBothMaps k v fm₁ fm₂
|
||||
Provenance-union fm₁@(m₁ , ks₁≡ks) fm₂@(m₂ , ks₂≡ks) {k} {v} k,v∈fm₁fm₂
|
||||
with Expr-Provenance-≡ ((` m₁) ∪ (` m₂)) k,v∈fm₁fm₂
|
||||
... | in₁ (single k,v∈m₁) k∉km₂
|
||||
with k∈km₁ ← (forget k,v∈m₁)
|
||||
with Expr-Provenance k ((` m₁) ∪ (` m₂)) (forget {m = proj₁ (fm₁ ⊔ᵐ fm₂)} k,v∈fm₁fm₂)
|
||||
... | (_ , (in₁ (single k,v∈m₁) k∉km₂ , _))
|
||||
with k∈km₁ ← (forget {m = m₁} k,v∈m₁)
|
||||
rewrite trans ks₁≡ks (sym ks₂≡ks) =
|
||||
⊥-elim (k∉km₂ k∈km₁)
|
||||
... | in₂ k∉km₁ (single k,v∈m₂)
|
||||
with k∈km₂ ← (forget k,v∈m₂)
|
||||
... | (_ , (in₂ k∉km₁ (single k,v∈m₂) , _))
|
||||
with k∈km₂ ← (forget {m = m₂} k,v∈m₂)
|
||||
rewrite trans ks₁≡ks (sym ks₂≡ks) =
|
||||
⊥-elim (k∉km₁ k∈km₂)
|
||||
... | bothᵘ {v₁} {v₂} (single k,v₁∈m₁) (single k,v₂∈m₂) =
|
||||
... | (v₁⊔v₂ , (bothᵘ {v₁} {v₂} (single k,v₁∈m₁) (single k,v₂∈m₂) , k,v₁⊔v₂∈m₁m₂))
|
||||
rewrite Map-functional {m = proj₁ (fm₁ ⊔ᵐ fm₂)} k,v∈fm₁fm₂ k,v₁⊔v₂∈m₁m₂ =
|
||||
((v₁ , v₂) , (refl , (k,v₁∈m₁ , k,v₂∈m₂)))
|
||||
|
||||
pop-⊔-distr : ∀ {k : A} {ks : List A} (fm₁ fm₂ : FiniteMap (k ∷ ks)) →
|
||||
|
|
@ -324,9 +324,11 @@ module IterProdIsomorphism where
|
|||
| from-first-value (fm₁ ⊔ᵐ fm₂)
|
||||
| from-first-value fm₁ | from-first-value fm₂
|
||||
... | (v , k,v∈fm₁fm₂) | (v₁ , k,v₁∈fm₁) | (v₂ , k,v₂∈fm₂) | refl | refl | refl
|
||||
with Expr-Provenance k ((` m₁) ∪ (` m₂)) (forget k,v∈fm₁fm₂)
|
||||
... | (_ , (in₁ _ k∉km₂ , _)) = ⊥-elim (k∉km₂ (forget k,v₂∈fm₂))
|
||||
... | (_ , (in₂ k∉km₁ _ , _)) = ⊥-elim (k∉km₁ (forget k,v₁∈fm₁))
|
||||
with Expr-Provenance k ((` m₁) ∪ (` m₂)) (forget {m = proj₁ (fm₁ ⊔ᵐ fm₂)} k,v∈fm₁fm₂)
|
||||
... | (_ , (in₁ _ k∉km₂ , _)) = ⊥-elim (k∉km₂ (forget {m = m₂}
|
||||
k,v₂∈fm₂))
|
||||
... | (_ , (in₂ k∉km₁ _ , _)) = ⊥-elim (k∉km₁ (forget {m = m₁}
|
||||
k,v₁∈fm₁))
|
||||
... | (v₁⊔v₂ , (bothᵘ {v₁'} {v₂'} (single k,v₁'∈m₁) (single k,v₂'∈m₂) , k,v₁⊔v₂∈m₁m₂))
|
||||
rewrite Map-functional {m = m₁} k,v₁∈fm₁ k,v₁'∈m₁
|
||||
rewrite Map-functional {m = m₂} k,v₂∈fm₂ k,v₂'∈m₂
|
||||
|
|
@ -385,10 +387,10 @@ module IterProdIsomorphism where
|
|||
(v , (IsLattice.≈-refl lB , here refl))
|
||||
... | here refl | there k',v₂∈fm₂' =
|
||||
⊥-elim (All¬-¬Any k≢ks' (subst (k' ∈ˡ_) (proj₂ fm₂')
|
||||
(forget k',v₂∈fm₂')))
|
||||
(forget {m = proj₁ fm₂'} k',v₂∈fm₂')))
|
||||
... | there k',v₁∈fm₁' | here refl =
|
||||
⊥-elim (All¬-¬Any k≢ks' (subst (k' ∈ˡ_) (proj₂ fm₁')
|
||||
(forget k',v₁∈fm₁')))
|
||||
(forget {m = proj₁ fm₁'} k',v₁∈fm₁')))
|
||||
... | there k',v₁∈fm₁' | there k',v₂∈fm₂' =
|
||||
let
|
||||
k',v₁v₂∈fm₁'fm₂' =
|
||||
|
|
|
|||
174
Lattice/Map.agda
174
Lattice/Map.agda
|
|
@ -488,9 +488,7 @@ _∈k_ k m = MemProp._∈_ k (keys m)
|
|||
locate : ∀ {k : A} {m : Map} → k ∈k m → Σ B (λ v → (k , v) ∈ m)
|
||||
locate k∈km = locate-impl k∈km
|
||||
|
||||
-- defined this way because ∈ for maps uses projection, so the full map can't be guessed.
|
||||
-- On the other hand, list can be guessed.
|
||||
forget : ∀ {k : A} {v : B} {l : List (A × B)} → (k , v) ∈ˡ l → k ∈ˡ (ImplKeys.keys l)
|
||||
forget : ∀ {k : A} {v : B} {m : Map} → (k , v) ∈ m → k ∈k m
|
||||
forget = ∈-cong proj₁
|
||||
|
||||
Map-functional : ∀ {k : A} {v v' : B} {m : Map} → (k , v) ∈ m → (k , v') ∈ m → v ≡ v'
|
||||
|
|
@ -594,9 +592,9 @@ 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₂)
|
||||
|
||||
Expr-Provenance-≡ : ∀ {k : A} {v : B} (e : Expr) → (k , v) ∈ ⟦ e ⟧ → Provenance k v e
|
||||
Expr-Provenance-≡ {k} {v} e k,v∈e
|
||||
with (v' , (p , k,v'∈e)) ← Expr-Provenance k e (forget k,v∈e)
|
||||
Expr-Provenance-≡ : ∀ (k : A) (v : B) (e : Expr) → (k , v) ∈ ⟦ e ⟧ → Provenance k v e
|
||||
Expr-Provenance-≡ k v e k,v∈e
|
||||
with (v' , (p , k,v'∈e)) ← Expr-Provenance k e (forget {m = ⟦ e ⟧} k,v∈e)
|
||||
rewrite Map-functional {m = ⟦ e ⟧} k,v∈e k,v'∈e = p
|
||||
|
||||
module _ (≈₂-dec : IsDecidable _≈₂_) where
|
||||
|
|
@ -611,7 +609,7 @@ module _ (≈₂-dec : IsDecidable _≈₂_) where
|
|||
let (v , k,v∈m₁) = locate-impl k∈km₁
|
||||
in no (λ m₁⊆m₂ →
|
||||
let (v' , (_ , k,v'∈m₂)) = m₁⊆m₂ k v k,v∈m₁
|
||||
in k∉km₂ (forget 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₁
|
||||
|
|
@ -667,16 +665,19 @@ private module I⊓ = ImplInsert _⊓₂_
|
|||
|
||||
⊔-⊆ : ∀ (m₁ m₂ m₃ m₄ : Map) → m₁ ≈ m₂ → m₃ ≈ m₄ → (m₁ ⊔ m₃) ⊆ (m₂ ⊔ m₄)
|
||||
⊔-⊆ m₁ m₂ m₃ m₄ m₁≈m₂ m₃≈m₄ k v k,v∈m₁m₃
|
||||
with Expr-Provenance-≡ ((` m₁) ∪ (` m₃)) k,v∈m₁m₃
|
||||
... | bothᵘ (single {v₁} v₁∈m₁) (single {v₃} v₃∈m₃) =
|
||||
with Expr-Provenance k ((` m₁) ∪ (` m₃)) (∈-cong proj₁ k,v∈m₁m₃)
|
||||
... | (_ , (bothᵘ (single {v₁} v₁∈m₁) (single {v₃} v₃∈m₃) , v₁v₃∈m₁m₃))
|
||||
rewrite Map-functional {m = m₁ ⊔ m₃} k,v∈m₁m₃ v₁v₃∈m₁m₃ =
|
||||
let (v₂ , (v₁≈v₂ , k,v₂∈m₂)) = proj₁ m₁≈m₂ k v₁ v₁∈m₁
|
||||
(v₄ , (v₃≈v₄ , k,v₄∈m₄)) = proj₁ m₃≈m₄ k v₃ v₃∈m₃
|
||||
in (v₂ ⊔₂ v₄ , (≈₂-⊔₂-cong v₁≈v₂ v₃≈v₄ , I⊔.union-combines (proj₂ m₂) (proj₂ m₄) k,v₂∈m₂ k,v₄∈m₄))
|
||||
... | in₁ (single {v₁} v₁∈m₁) k∉km₃ =
|
||||
... | (_ , (in₁ (single {v₁} v₁∈m₁) k∉km₃ , v₁∈m₁m₃))
|
||||
rewrite Map-functional {m = m₁ ⊔ m₃} k,v∈m₁m₃ v₁∈m₁m₃ =
|
||||
let (v₂ , (v₁≈v₂ , k,v₂∈m₂)) = proj₁ m₁≈m₂ k v₁ v₁∈m₁
|
||||
k∉km₄ = ≈-∉-cong {m₃} {m₄} m₃≈m₄ k∉km₃
|
||||
in (v₂ , (v₁≈v₂ , I⊔.union-preserves-∈₁ (proj₂ m₂) k,v₂∈m₂ k∉km₄))
|
||||
... | in₂ k∉km₁ (single {v₃} v₃∈m₃) =
|
||||
... | (_ , (in₂ k∉km₁ (single {v₃} v₃∈m₃) , v₃∈m₁m₃))
|
||||
rewrite Map-functional {m = m₁ ⊔ m₃} k,v∈m₁m₃ v₃∈m₁m₃ =
|
||||
let (v₄ , (v₃≈v₄ , k,v₄∈m₄)) = proj₁ m₃≈m₄ k v₃ v₃∈m₃
|
||||
k∉km₂ = ≈-∉-cong {m₁} {m₂} m₁≈m₂ k∉km₁
|
||||
in (v₄ , (v₃≈v₄ , I⊔.union-preserves-∈₂ k∉km₂ k,v₄∈m₄))
|
||||
|
|
@ -689,8 +690,9 @@ private module I⊓ = ImplInsert _⊓₂_
|
|||
where
|
||||
⊓-⊆ : ∀ (m₁ m₂ m₃ m₄ : Map) → m₁ ≈ m₂ → m₃ ≈ m₄ → (m₁ ⊓ m₃) ⊆ (m₂ ⊓ m₄)
|
||||
⊓-⊆ m₁ m₂ m₃ m₄ m₁≈m₂ m₃≈m₄ k v k,v∈m₁m₃
|
||||
with Expr-Provenance-≡ ((` m₁) ∩ (` m₃)) k,v∈m₁m₃
|
||||
... | bothⁱ (single {v₁} v₁∈m₁) (single {v₃} v₃∈m₃) =
|
||||
with Expr-Provenance k ((` m₁) ∩ (` m₃)) (∈-cong proj₁ k,v∈m₁m₃)
|
||||
... | (_ , (bothⁱ (single {v₁} v₁∈m₁) (single {v₃} v₃∈m₃) , v₁v₃∈m₁m₃))
|
||||
rewrite Map-functional {m = m₁ ⊓ m₃} k,v∈m₁m₃ v₁v₃∈m₁m₃ =
|
||||
let (v₂ , (v₁≈v₂ , k,v₂∈m₂)) = proj₁ m₁≈m₂ k v₁ v₁∈m₁
|
||||
(v₄ , (v₃≈v₄ , k,v₄∈m₄)) = proj₁ m₃≈m₄ k v₃ v₃∈m₃
|
||||
in (v₂ ⊓₂ v₄ , (≈₂-⊓₂-cong v₁≈v₂ v₃≈v₄ , I⊓.intersect-combines (proj₂ m₂) (proj₂ m₄) k,v₂∈m₂ k,v₄∈m₄))
|
||||
|
|
@ -700,12 +702,13 @@ private module I⊓ = ImplInsert _⊓₂_
|
|||
where
|
||||
mm-m-⊆ : (m ⊔ m) ⊆ m
|
||||
mm-m-⊆ k v k,v∈mm
|
||||
with Expr-Provenance-≡ ((` m) ∪ (` m)) k,v∈mm
|
||||
... | bothᵘ (single {v'} v'∈m) (single {v''} v''∈m)
|
||||
rewrite Map-functional {m = m} v'∈m v''∈m =
|
||||
with Expr-Provenance k ((` m) ∪ (` m)) (∈-cong proj₁ k,v∈mm)
|
||||
... | (_ , (bothᵘ (single {v'} v'∈m) (single {v''} v''∈m) , v'v''∈mm))
|
||||
rewrite Map-functional {m = m} v'∈m v''∈m
|
||||
rewrite Map-functional {m = m ⊔ m} k,v∈mm v'v''∈mm =
|
||||
(v'' , (⊔₂-idemp v'' , v''∈m))
|
||||
... | in₁ (single {v'} v'∈m) k∉km = ⊥-elim (k∉km (∈-cong proj₁ v'∈m))
|
||||
... | in₂ k∉km (single {v''} v''∈m) = ⊥-elim (k∉km (∈-cong proj₁ v''∈m))
|
||||
... | (_ , (in₁ (single {v'} v'∈m) k∉km , _)) = ⊥-elim (k∉km (∈-cong proj₁ v'∈m))
|
||||
... | (_ , (in₂ k∉km (single {v''} v''∈m) , _)) = ⊥-elim (k∉km (∈-cong proj₁ v''∈m))
|
||||
|
||||
m-mm-⊆ : m ⊆ (m ⊔ m)
|
||||
m-mm-⊆ k v k,v∈m = (v ⊔₂ v , (≈₂-sym (⊔₂-idemp v) , I⊔.union-combines u u k,v∈m k,v∈m))
|
||||
|
|
@ -715,12 +718,15 @@ private module I⊓ = ImplInsert _⊓₂_
|
|||
where
|
||||
⊔-comm-⊆ : ∀ (m₁ m₂ : Map) → (m₁ ⊔ m₂) ⊆ (m₂ ⊔ m₁)
|
||||
⊔-comm-⊆ m₁@(l₁ , u₁) m₂@(l₂ , u₂) k v k,v∈m₁m₂
|
||||
with Expr-Provenance-≡ ((` m₁) ∪ (` m₂)) k,v∈m₁m₂
|
||||
... | bothᵘ {v₁} {v₂} (single v₁∈m₁) (single v₂∈m₂) =
|
||||
with Expr-Provenance k ((` m₁) ∪ (` m₂)) (∈-cong proj₁ k,v∈m₁m₂)
|
||||
... | (_ , (bothᵘ {v₁} {v₂} (single v₁∈m₁) (single v₂∈m₂) , v₁v₂∈m₁m₂))
|
||||
rewrite Map-functional {m = m₁ ⊔ m₂} k,v∈m₁m₂ v₁v₂∈m₁m₂ =
|
||||
(v₂ ⊔₂ v₁ , (⊔₂-comm v₁ v₂ , I⊔.union-combines u₂ u₁ v₂∈m₂ v₁∈m₁))
|
||||
... | in₁ {v₁} (single v₁∈m₁) k∉km₂ =
|
||||
... | (_ , (in₁ {v₁} (single v₁∈m₁) k∉km₂ , v₁∈m₁m₂))
|
||||
rewrite Map-functional {m = m₁ ⊔ m₂} k,v∈m₁m₂ v₁∈m₁m₂ =
|
||||
(v₁ , (≈₂-refl , I⊔.union-preserves-∈₂ k∉km₂ v₁∈m₁))
|
||||
... | in₂ {v₂} k∉km₁ (single v₂∈m₂) =
|
||||
... | (_ , (in₂ {v₂} k∉km₁ (single v₂∈m₂) , v₂∈m₁m₂))
|
||||
rewrite Map-functional {m = m₁ ⊔ m₂} k,v∈m₁m₂ v₂∈m₁m₂ =
|
||||
(v₂ , (≈₂-refl , I⊔.union-preserves-∈₁ u₂ v₂∈m₂ k∉km₁))
|
||||
|
||||
⊔-assoc : ∀ (m₁ m₂ m₃ : Map) → ((m₁ ⊔ m₂) ⊔ m₃) ≈ (m₁ ⊔ (m₂ ⊔ m₃))
|
||||
|
|
@ -728,40 +734,54 @@ private module I⊓ = ImplInsert _⊓₂_
|
|||
where
|
||||
⊔-assoc₁ : ((m₁ ⊔ m₂) ⊔ m₃) ⊆ (m₁ ⊔ (m₂ ⊔ m₃))
|
||||
⊔-assoc₁ k v k,v∈m₁₂m₃
|
||||
with Expr-Provenance-≡ (((` m₁) ∪ (` m₂)) ∪ (` m₃)) k,v∈m₁₂m₃
|
||||
... | in₂ k∉ke₁₂ (single {v₃} v₃∈e₃) =
|
||||
with Expr-Provenance k (((` m₁) ∪ (` m₂)) ∪ (` m₃)) (∈-cong proj₁ k,v∈m₁₂m₃)
|
||||
... | (_ , (in₂ k∉ke₁₂ (single {v₃} v₃∈e₃) , v₃∈m₁₂m₃))
|
||||
rewrite Map-functional {m = (m₁ ⊔ m₂) ⊔ m₃} k,v∈m₁₂m₃ v₃∈m₁₂m₃ =
|
||||
let (k∉ke₁ , k∉ke₂) = I⊔.∉-union-∉-either {l₁ = l₁} {l₂ = l₂} k∉ke₁₂
|
||||
in (v₃ , (≈₂-refl , I⊔.union-preserves-∈₂ k∉ke₁ (I⊔.union-preserves-∈₂ k∉ke₂ v₃∈e₃)))
|
||||
... | in₁ (in₂ k∉ke₁ (single {v₂} v₂∈e₂)) k∉ke₃ =
|
||||
... | (_ , (in₁ (in₂ k∉ke₁ (single {v₂} v₂∈e₂)) k∉ke₃ , v₂∈m₁₂m₃))
|
||||
rewrite Map-functional {m = (m₁ ⊔ m₂) ⊔ m₃} k,v∈m₁₂m₃ v₂∈m₁₂m₃ =
|
||||
(v₂ , (≈₂-refl , I⊔.union-preserves-∈₂ k∉ke₁ (I⊔.union-preserves-∈₁ u₂ v₂∈e₂ k∉ke₃)))
|
||||
... | bothᵘ (in₂ k∉ke₁ (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) =
|
||||
... | (_ , (bothᵘ (in₂ k∉ke₁ (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) , v₂v₃∈m₁₂m₃))
|
||||
rewrite Map-functional {m = (m₁ ⊔ m₂) ⊔ m₃} k,v∈m₁₂m₃ v₂v₃∈m₁₂m₃ =
|
||||
(v₂ ⊔₂ v₃ , (≈₂-refl , I⊔.union-preserves-∈₂ k∉ke₁ (I⊔.union-combines u₂ u₃ v₂∈e₂ v₃∈e₃)))
|
||||
... | in₁ (in₁ (single {v₁} v₁∈e₁) k∉ke₂) k∉ke₃ =
|
||||
... | (_ , (in₁ (in₁ (single {v₁} v₁∈e₁) k∉ke₂) k∉ke₃ , v₁∈m₁₂m₃))
|
||||
rewrite Map-functional {m = (m₁ ⊔ m₂) ⊔ m₃} k,v∈m₁₂m₃ v₁∈m₁₂m₃ =
|
||||
(v₁ , (≈₂-refl , I⊔.union-preserves-∈₁ u₁ v₁∈e₁ (I⊔.union-preserves-∉ k∉ke₂ k∉ke₃)))
|
||||
... | bothᵘ (in₁ (single {v₁} v₁∈e₁) k∉ke₂) (single {v₃} v₃∈e₃) =
|
||||
... | (_ , (bothᵘ (in₁ (single {v₁} v₁∈e₁) k∉ke₂) (single {v₃} v₃∈e₃) , v₁v₃∈m₁₂m₃))
|
||||
rewrite Map-functional {m = (m₁ ⊔ m₂) ⊔ m₃} k,v∈m₁₂m₃ v₁v₃∈m₁₂m₃ =
|
||||
(v₁ ⊔₂ v₃ , (≈₂-refl , I⊔.union-combines u₁ (I⊔.union-preserves-Unique l₂ l₃ u₃) v₁∈e₁ (I⊔.union-preserves-∈₂ k∉ke₂ v₃∈e₃)))
|
||||
... | in₁ (bothᵘ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) k∉ke₃ =
|
||||
... | (_ , (in₁ (bothᵘ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) k∉ke₃), v₁v₂∈m₁₂m₃)
|
||||
rewrite Map-functional {m = (m₁ ⊔ m₂) ⊔ m₃} k,v∈m₁₂m₃ v₁v₂∈m₁₂m₃ =
|
||||
(v₁ ⊔₂ v₂ , (≈₂-refl , I⊔.union-combines u₁ (I⊔.union-preserves-Unique l₂ l₃ u₃) v₁∈e₁ (I⊔.union-preserves-∈₁ u₂ v₂∈e₂ k∉ke₃)))
|
||||
... | bothᵘ (bothᵘ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) =
|
||||
... | (_ , (bothᵘ (bothᵘ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) , v₁v₂v₃∈m₁₂m₃))
|
||||
rewrite Map-functional {m = (m₁ ⊔ m₂) ⊔ m₃} k,v∈m₁₂m₃ v₁v₂v₃∈m₁₂m₃ =
|
||||
(v₁ ⊔₂ (v₂ ⊔₂ v₃) , (⊔₂-assoc v₁ v₂ v₃ , I⊔.union-combines u₁ (I⊔.union-preserves-Unique l₂ l₃ u₃) v₁∈e₁ (I⊔.union-combines u₂ u₃ v₂∈e₂ v₃∈e₃)))
|
||||
|
||||
⊔-assoc₂ : (m₁ ⊔ (m₂ ⊔ m₃)) ⊆ ((m₁ ⊔ m₂) ⊔ m₃)
|
||||
⊔-assoc₂ k v k,v∈m₁m₂₃
|
||||
with Expr-Provenance-≡ ((` m₁) ∪ ((` m₂) ∪ (` m₃))) k,v∈m₁m₂₃
|
||||
... | in₂ k∉ke₁ (in₂ k∉ke₂ (single {v₃} v₃∈e₃)) =
|
||||
with Expr-Provenance k ((` m₁) ∪ ((` m₂) ∪ (` m₃))) (∈-cong proj₁ k,v∈m₁m₂₃)
|
||||
... | (_ , (in₂ k∉ke₁ (in₂ k∉ke₂ (single {v₃} v₃∈e₃)) , v₃∈m₁m₂₃))
|
||||
rewrite Map-functional {m = m₁ ⊔ (m₂ ⊔ m₃)} k,v∈m₁m₂₃ v₃∈m₁m₂₃ =
|
||||
(v₃ , (≈₂-refl , I⊔.union-preserves-∈₂ (I⊔.union-preserves-∉ k∉ke₁ k∉ke₂) v₃∈e₃))
|
||||
... | in₂ k∉ke₁ (in₁ (single {v₂} v₂∈e₂) k∉ke₃) =
|
||||
... | (_ , (in₂ k∉ke₁ (in₁ (single {v₂} v₂∈e₂) k∉ke₃) , v₂∈m₁m₂₃))
|
||||
rewrite Map-functional {m = m₁ ⊔ (m₂ ⊔ m₃)} k,v∈m₁m₂₃ v₂∈m₁m₂₃ =
|
||||
(v₂ , (≈₂-refl , I⊔.union-preserves-∈₁ (I⊔.union-preserves-Unique l₁ l₂ u₂) (I⊔.union-preserves-∈₂ k∉ke₁ v₂∈e₂) k∉ke₃))
|
||||
... | in₂ k∉ke₁ (bothᵘ (single {v₂} v₂∈e₂) (single {v₃} v₃∈e₃)) =
|
||||
... | (_ , (in₂ k∉ke₁ (bothᵘ (single {v₂} v₂∈e₂) (single {v₃} v₃∈e₃)) , v₂v₃∈m₁m₂₃))
|
||||
rewrite Map-functional {m = m₁ ⊔ (m₂ ⊔ m₃)} k,v∈m₁m₂₃ v₂v₃∈m₁m₂₃ =
|
||||
(v₂ ⊔₂ v₃ , (≈₂-refl , I⊔.union-combines (I⊔.union-preserves-Unique l₁ l₂ u₂) u₃ (I⊔.union-preserves-∈₂ k∉ke₁ v₂∈e₂) v₃∈e₃))
|
||||
... | in₁ (single {v₁} v₁∈e₁) k∉ke₂₃ =
|
||||
... | (_ , (in₁ (single {v₁} v₁∈e₁) k∉ke₂₃ , v₁∈m₁m₂₃))
|
||||
rewrite Map-functional {m = m₁ ⊔ (m₂ ⊔ m₃)} k,v∈m₁m₂₃ v₁∈m₁m₂₃ =
|
||||
let (k∉ke₂ , k∉ke₃) = I⊔.∉-union-∉-either {l₁ = l₂} {l₂ = l₃} k∉ke₂₃
|
||||
in (v₁ , (≈₂-refl , I⊔.union-preserves-∈₁ (I⊔.union-preserves-Unique l₁ l₂ u₂) (I⊔.union-preserves-∈₁ u₁ v₁∈e₁ k∉ke₂) k∉ke₃))
|
||||
... | bothᵘ (single {v₁} v₁∈e₁) (in₂ k∉ke₂ (single {v₃} v₃∈e₃)) =
|
||||
... | (_ , (bothᵘ (single {v₁} v₁∈e₁) (in₂ k∉ke₂ (single {v₃} v₃∈e₃)) , v₁v₃∈m₁m₂₃))
|
||||
rewrite Map-functional {m = m₁ ⊔ (m₂ ⊔ m₃)} k,v∈m₁m₂₃ v₁v₃∈m₁m₂₃ =
|
||||
(v₁ ⊔₂ v₃ , (≈₂-refl , I⊔.union-combines (I⊔.union-preserves-Unique l₁ l₂ u₂) u₃ (I⊔.union-preserves-∈₁ u₁ v₁∈e₁ k∉ke₂) v₃∈e₃))
|
||||
... | bothᵘ (single {v₁} v₁∈e₁) (in₁ (single {v₂} v₂∈e₂) k∉ke₃) =
|
||||
... | (_ , (bothᵘ (single {v₁} v₁∈e₁) (in₁ (single {v₂} v₂∈e₂) k∉ke₃) , v₁v₂∈m₁m₂₃))
|
||||
rewrite Map-functional {m = m₁ ⊔ (m₂ ⊔ m₃)} k,v∈m₁m₂₃ v₁v₂∈m₁m₂₃ =
|
||||
(v₁ ⊔₂ v₂ , (≈₂-refl , I⊔.union-preserves-∈₁ (I⊔.union-preserves-Unique l₁ l₂ u₂) (I⊔.union-combines u₁ u₂ v₁∈e₁ v₂∈e₂) k∉ke₃))
|
||||
... | bothᵘ (single {v₁} v₁∈e₁) (bothᵘ (single {v₂} v₂∈e₂) (single {v₃} v₃∈e₃)) =
|
||||
... | (_ , (bothᵘ (single {v₁} v₁∈e₁) (bothᵘ (single {v₂} v₂∈e₂) (single {v₃} v₃∈e₃)) , v₁v₂v₃∈m₁m₂₃))
|
||||
rewrite Map-functional {m = m₁ ⊔ (m₂ ⊔ m₃)} k,v∈m₁m₂₃ v₁v₂v₃∈m₁m₂₃ =
|
||||
((v₁ ⊔₂ v₂) ⊔₂ v₃ , (≈₂-sym (⊔₂-assoc v₁ v₂ v₃) , I⊔.union-combines (I⊔.union-preserves-Unique l₁ l₂ u₂) u₃ (I⊔.union-combines u₁ u₂ v₁∈e₁ v₂∈e₂) v₃∈e₃))
|
||||
|
||||
⊓-idemp : ∀ (m : Map) → (m ⊓ m) ≈ m
|
||||
|
|
@ -769,9 +789,10 @@ private module I⊓ = ImplInsert _⊓₂_
|
|||
where
|
||||
mm-m-⊆ : (m ⊓ m) ⊆ m
|
||||
mm-m-⊆ k v k,v∈mm
|
||||
with Expr-Provenance-≡ ((` m) ∩ (` m)) k,v∈mm
|
||||
... | bothⁱ (single {v'} v'∈m) (single {v''} v''∈m)
|
||||
rewrite Map-functional {m = m} v'∈m v''∈m =
|
||||
with Expr-Provenance k ((` m) ∩ (` m)) (∈-cong proj₁ k,v∈mm)
|
||||
... | (_ , (bothⁱ (single {v'} v'∈m) (single {v''} v''∈m) , v'v''∈mm))
|
||||
rewrite Map-functional {m = m} v'∈m v''∈m
|
||||
rewrite Map-functional {m = m ⊓ m} k,v∈mm v'v''∈mm =
|
||||
(v'' , (⊓₂-idemp v'' , v''∈m))
|
||||
|
||||
m-mm-⊆ : m ⊆ (m ⊓ m)
|
||||
|
|
@ -782,8 +803,9 @@ private module I⊓ = ImplInsert _⊓₂_
|
|||
where
|
||||
⊓-comm-⊆ : ∀ (m₁ m₂ : Map) → (m₁ ⊓ m₂) ⊆ (m₂ ⊓ m₁)
|
||||
⊓-comm-⊆ m₁@(l₁ , u₁) m₂@(l₂ , u₂) k v k,v∈m₁m₂
|
||||
with Expr-Provenance-≡ ((` m₁) ∩ (` m₂)) k,v∈m₁m₂
|
||||
... | bothⁱ {v₁} {v₂} (single v₁∈m₁) (single v₂∈m₂) =
|
||||
with Expr-Provenance k ((` m₁) ∩ (` m₂)) (∈-cong proj₁ k,v∈m₁m₂)
|
||||
... | (_ , (bothⁱ {v₁} {v₂} (single v₁∈m₁) (single v₂∈m₂) , v₁v₂∈m₁m₂))
|
||||
rewrite Map-functional {m = m₁ ⊓ m₂} k,v∈m₁m₂ v₁v₂∈m₁m₂ =
|
||||
(v₂ ⊓₂ v₁ , (⊓₂-comm v₁ v₂ , I⊓.intersect-combines u₂ u₁ v₂∈m₂ v₁∈m₁))
|
||||
|
||||
⊓-assoc : ∀ (m₁ m₂ m₃ : Map) → ((m₁ ⊓ m₂) ⊓ m₃) ≈ (m₁ ⊓ (m₂ ⊓ m₃))
|
||||
|
|
@ -791,14 +813,16 @@ private module I⊓ = ImplInsert _⊓₂_
|
|||
where
|
||||
⊓-assoc₁ : ((m₁ ⊓ m₂) ⊓ m₃) ⊆ (m₁ ⊓ (m₂ ⊓ m₃))
|
||||
⊓-assoc₁ k v k,v∈m₁₂m₃
|
||||
with Expr-Provenance-≡ (((` m₁) ∩ (` m₂)) ∩ (` m₃)) k,v∈m₁₂m₃
|
||||
... | bothⁱ (bothⁱ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) =
|
||||
with Expr-Provenance k (((` m₁) ∩ (` m₂)) ∩ (` m₃)) (∈-cong proj₁ k,v∈m₁₂m₃)
|
||||
... | (_ , (bothⁱ (bothⁱ (single {v₁} v₁∈e₁) (single {v₂} v₂∈e₂)) (single {v₃} v₃∈e₃) , v₁v₂v₃∈m₁₂m₃))
|
||||
rewrite Map-functional {m = (m₁ ⊓ m₂) ⊓ m₃} k,v∈m₁₂m₃ v₁v₂v₃∈m₁₂m₃ =
|
||||
(v₁ ⊓₂ (v₂ ⊓₂ v₃) , (⊓₂-assoc v₁ v₂ v₃ , I⊓.intersect-combines u₁ (I⊓.intersect-preserves-Unique {l₂} {l₃} u₃) v₁∈e₁ (I⊓.intersect-combines u₂ u₃ v₂∈e₂ v₃∈e₃)))
|
||||
|
||||
⊓-assoc₂ : (m₁ ⊓ (m₂ ⊓ m₃)) ⊆ ((m₁ ⊓ m₂) ⊓ m₃)
|
||||
⊓-assoc₂ k v k,v∈m₁m₂₃
|
||||
with Expr-Provenance-≡ ((` m₁) ∩ ((` m₂) ∩ (` m₃))) k,v∈m₁m₂₃
|
||||
... | bothⁱ (single {v₁} v₁∈e₁) (bothⁱ (single {v₂} v₂∈e₂) (single {v₃} v₃∈e₃)) =
|
||||
with Expr-Provenance k ((` m₁) ∩ ((` m₂) ∩ (` m₃))) (∈-cong proj₁ k,v∈m₁m₂₃)
|
||||
... | (_ , (bothⁱ (single {v₁} v₁∈e₁) (bothⁱ (single {v₂} v₂∈e₂) (single {v₃} v₃∈e₃)) , v₁v₂v₃∈m₁m₂₃))
|
||||
rewrite Map-functional {m = m₁ ⊓ (m₂ ⊓ m₃)} k,v∈m₁m₂₃ v₁v₂v₃∈m₁m₂₃ =
|
||||
((v₁ ⊓₂ v₂) ⊓₂ v₃ , (≈₂-sym (⊓₂-assoc v₁ v₂ v₃) , I⊓.intersect-combines (I⊓.intersect-preserves-Unique {l₁} {l₂} u₂) u₃ (I⊓.intersect-combines u₁ u₂ v₁∈e₁ v₂∈e₂) v₃∈e₃))
|
||||
|
||||
absorb-⊓-⊔ : ∀ (m₁ m₂ : Map) → (m₁ ⊓ (m₁ ⊔ m₂)) ≈ m₁
|
||||
|
|
@ -806,18 +830,20 @@ absorb-⊓-⊔ m₁@(l₁ , u₁) m₂@(l₂ , u₂) = (absorb-⊓-⊔¹ , absor
|
|||
where
|
||||
absorb-⊓-⊔¹ : (m₁ ⊓ (m₁ ⊔ m₂)) ⊆ m₁
|
||||
absorb-⊓-⊔¹ k v k,v∈m₁m₁₂
|
||||
with Expr-Provenance-≡ ((` m₁) ∩ ((` m₁) ∪ (` m₂))) k,v∈m₁m₁₂
|
||||
... | bothⁱ (single {v₁} k,v₁∈m₁)
|
||||
(bothᵘ (single {v₁'} k,v₁'∈m₁)
|
||||
(single {v₂} v₂∈m₂))
|
||||
rewrite Map-functional {m = m₁} k,v₁∈m₁ k,v₁'∈m₁ =
|
||||
with Expr-Provenance k ((` m₁) ∩ ((` m₁) ∪ (` m₂))) (∈-cong proj₁ k,v∈m₁m₁₂)
|
||||
... | (_ , (bothⁱ (single {v₁} k,v₁∈m₁)
|
||||
(bothᵘ (single {v₁'} k,v₁'∈m₁)
|
||||
(single {v₂} v₂∈m₂)) , v₁v₁'v₂∈m₁m₁₂))
|
||||
rewrite Map-functional {m = m₁} k,v₁∈m₁ k,v₁'∈m₁
|
||||
rewrite Map-functional {m = m₁ ⊓ (m₁ ⊔ m₂)} k,v∈m₁m₁₂ v₁v₁'v₂∈m₁m₁₂ =
|
||||
(v₁' , (absorb-⊓₂-⊔₂ v₁' v₂ , k,v₁'∈m₁))
|
||||
... | bothⁱ (single {v₁} k,v₁∈m₁)
|
||||
(in₁ (single {v₁'} k,v₁'∈m₁) _)
|
||||
rewrite Map-functional {m = m₁} k,v₁∈m₁ k,v₁'∈m₁ =
|
||||
... | (_ , (bothⁱ (single {v₁} k,v₁∈m₁)
|
||||
(in₁ (single {v₁'} k,v₁'∈m₁) _) , v₁v₁'∈m₁m₁₂))
|
||||
rewrite Map-functional {m = m₁} k,v₁∈m₁ k,v₁'∈m₁
|
||||
rewrite Map-functional {m = m₁ ⊓ (m₁ ⊔ m₂)} k,v∈m₁m₁₂ v₁v₁'∈m₁m₁₂ =
|
||||
(v₁' , (⊓₂-idemp v₁' , k,v₁'∈m₁))
|
||||
... | bothⁱ (single {v₁} k,v₁∈m₁)
|
||||
(in₂ k∉m₁ _ ) = ⊥-elim (k∉m₁ (∈-cong proj₁ k,v₁∈m₁))
|
||||
... | (_ , (bothⁱ (single {v₁} k,v₁∈m₁)
|
||||
(in₂ k∉m₁ _ ) , _)) = ⊥-elim (k∉m₁ (∈-cong proj₁ k,v₁∈m₁))
|
||||
|
||||
absorb-⊓-⊔² : m₁ ⊆ (m₁ ⊓ (m₁ ⊔ m₂))
|
||||
absorb-⊓-⊔² k v k,v∈m₁
|
||||
|
|
@ -832,16 +858,18 @@ absorb-⊔-⊓ m₁@(l₁ , u₁) m₂@(l₂ , u₂) = (absorb-⊔-⊓¹ , absor
|
|||
where
|
||||
absorb-⊔-⊓¹ : (m₁ ⊔ (m₁ ⊓ m₂)) ⊆ m₁
|
||||
absorb-⊔-⊓¹ k v k,v∈m₁m₁₂
|
||||
with Expr-Provenance-≡ ((` m₁) ∪ ((` m₁) ∩ (` m₂))) k,v∈m₁m₁₂
|
||||
... | bothᵘ (single {v₁} k,v₁∈m₁)
|
||||
(bothⁱ (single {v₁'} k,v₁'∈m₁)
|
||||
(single {v₂} k,v₂∈m₂))
|
||||
rewrite Map-functional {m = m₁} k,v₁∈m₁ k,v₁'∈m₁ =
|
||||
with Expr-Provenance k ((` m₁) ∪ ((` m₁) ∩ (` m₂))) (∈-cong proj₁ k,v∈m₁m₁₂)
|
||||
... | (_ , (bothᵘ (single {v₁} k,v₁∈m₁)
|
||||
(bothⁱ (single {v₁'} k,v₁'∈m₁)
|
||||
(single {v₂} k,v₂∈m₂)) , v₁v₁'v₂∈m₁m₁₂))
|
||||
rewrite Map-functional {m = m₁} k,v₁∈m₁ k,v₁'∈m₁
|
||||
rewrite Map-functional {m = m₁ ⊔ (m₁ ⊓ m₂)} k,v∈m₁m₁₂ v₁v₁'v₂∈m₁m₁₂ =
|
||||
(v₁' , (absorb-⊔₂-⊓₂ v₁' v₂ , k,v₁'∈m₁))
|
||||
... | in₁ (single {v₁} k,v₁∈m₁) k∉km₁₂ =
|
||||
... | (_ , (in₁ (single {v₁} k,v₁∈m₁) k∉km₁₂ , k,v₁∈m₁m₁₂))
|
||||
rewrite Map-functional {m = m₁ ⊔ (m₁ ⊓ m₂)} k,v∈m₁m₁₂ k,v₁∈m₁m₁₂ =
|
||||
(v₁ , (≈₂-refl , k,v₁∈m₁))
|
||||
... | in₂ k∉km₁ (bothⁱ (single {v₁'} k,v₁'∈m₁)
|
||||
(single {v₂} k,v₂∈m₂)) =
|
||||
... | (_ , (in₂ k∉km₁ (bothⁱ (single {v₁'} k,v₁'∈m₁)
|
||||
(single {v₂} k,v₂∈m₂)) , _)) =
|
||||
⊥-elim (k∉km₁ (∈-cong proj₁ k,v₁'∈m₁))
|
||||
|
||||
absorb-⊔-⊓² : m₁ ⊆ (m₁ ⊔ (m₁ ⊓ m₂))
|
||||
|
|
@ -981,7 +1009,7 @@ updating-via-k∈ks-forward m {ks} f k∈ks k∈km rewrite transform-keys-≡ (p
|
|||
updating-via-k∈ks-≡ : ∀ (m : Map) {ks : List A} (f : A → B) {k : A} {v : B} →
|
||||
k ∈ˡ ks → (k , v) ∈ (m updating ks via f)→ v ≡ f k
|
||||
updating-via-k∈ks-≡ m {ks} f k∈ks k,v∈um
|
||||
with updating-via-k∈ks m f k∈ks (forget k,v∈um)
|
||||
with updating-via-k∈ks m f k∈ks (forget {m = (m updating ks via f)} k,v∈um)
|
||||
... | k,fk∈um = Map-functional {m = (m updating ks via f)} k,v∈um k,fk∈um
|
||||
|
||||
updating-via-k∉ks-forward : ∀ (m : Map) {ks : List A} (f : A → B) {k : A} {v : B} →
|
||||
|
|
@ -1016,14 +1044,14 @@ module _ {l} {L : Set l}
|
|||
|
||||
f'l₁f'l₂⊆f'l₂ : ((f' l₁) ⊔ (f' l₂)) ⊆ f' l₂
|
||||
f'l₁f'l₂⊆f'l₂ k v k,v∈f'l₁f'l₂
|
||||
with Expr-Provenance-≡ ((` (f' l₁)) ∪ (` (f' l₂))) k,v∈f'l₁f'l₂
|
||||
with Expr-Provenance-≡ k v ((` (f' l₁)) ∪ (` (f' l₂))) k,v∈f'l₁f'l₂
|
||||
... | in₁ (single k,v∈f'l₁) k∉kf'l₂ =
|
||||
let
|
||||
k∈kfl₁ = updating-via-∈k-backward (f l₁) ks (updater l₁) (forget k,v∈f'l₁)
|
||||
k∈kfl₁ = updating-via-∈k-backward (f l₁) ks (updater l₁) (forget {m = f' l₁} k,v∈f'l₁)
|
||||
k∈kfl₁fl₂ = union-preserves-∈k₁ {l₁ = proj₁ (f l₁)} {l₂ = proj₁ (f l₂)} k∈kfl₁
|
||||
(v' , k,v'∈fl₁l₂) = locate {m = (f l₁ ⊔ f l₂)} k∈kfl₁fl₂
|
||||
(v'' , (v'≈v'' , k,v''∈fl₂)) = fl₁fl₂⊆fl₂ k v' k,v'∈fl₁l₂
|
||||
k∈kf'l₂ = updating-via-∈k-forward (f l₂) ks (updater l₂) (forget k,v''∈fl₂)
|
||||
k∈kf'l₂ = updating-via-∈k-forward (f l₂) ks (updater l₂) (forget {m = f l₂} k,v''∈fl₂)
|
||||
in
|
||||
⊥-elim (k∉kf'l₂ k∈kf'l₂)
|
||||
... | in₂ k∉kf'l₁ (single k,v'∈f'l₂) =
|
||||
|
|
@ -1046,10 +1074,10 @@ module _ {l} {L : Set l}
|
|||
|
||||
f'l₂⊆f'l₁f'l₂ : f' l₂ ⊆ ((f' l₁) ⊔ (f' l₂))
|
||||
f'l₂⊆f'l₁f'l₂ k v k,v∈f'l₂
|
||||
with k∈kfl₂ ← updating-via-∈k-backward (f l₂) ks (updater l₂) (forget k,v∈f'l₂)
|
||||
with k∈kfl₂ ← updating-via-∈k-backward (f l₂) ks (updater l₂) (forget {m = f' l₂} k,v∈f'l₂)
|
||||
with (v' , k,v'∈fl₂) ← locate {m = f l₂} k∈kfl₂
|
||||
with (v'' , (v'≈v'' , k,v''∈fl₁fl₂)) ← fl₂⊆fl₁fl₂ k v' k,v'∈fl₂
|
||||
with Expr-Provenance-≡ ((` (f l₁)) ∪ (` (f l₂))) k,v''∈fl₁fl₂
|
||||
with Expr-Provenance-≡ k v'' ((` (f l₁)) ∪ (` (f l₂))) k,v''∈fl₁fl₂
|
||||
... | in₁ (single k,v''∈fl₁) k∉kfl₂ = ⊥-elim (k∉kfl₂ k∈kfl₂)
|
||||
... | in₂ k∉kfl₁ (single k,v''∈fl₂) =
|
||||
let
|
||||
|
|
@ -1060,8 +1088,8 @@ module _ {l} {L : Set l}
|
|||
with k∈-dec k ks
|
||||
... | yes k∈ks with refl ← updating-via-k∈ks-≡ (f l₂) (updater l₂) k∈ks k,v∈f'l₂ =
|
||||
let
|
||||
k,uv₁∈f'l₁ = updating-via-k∈ks-forward (f l₁) (updater l₁) k∈ks (forget k,v₁∈fl₁)
|
||||
k,uv₂∈f'l₂ = updating-via-k∈ks-forward (f l₂) (updater l₂) k∈ks (forget k,v₂∈fl₂)
|
||||
k,uv₁∈f'l₁ = updating-via-k∈ks-forward (f l₁) (updater l₁) k∈ks (forget {m = f l₁} k,v₁∈fl₁)
|
||||
k,uv₂∈f'l₂ = updating-via-k∈ks-forward (f l₂) (updater l₂) k∈ks (forget {m = f l₂} k,v₂∈fl₂)
|
||||
k,uv₁uv₂∈f'l₁f'l₂ = ⊔-combines {m₁ = f' l₁} {m₂ = f' l₂} k,uv₁∈f'l₁ k,uv₂∈f'l₂
|
||||
in
|
||||
(updater l₁ k ⊔₂ updater l₂ k , (IsLattice.≈-sym lB (g-Monotonicʳ k l₁≼l₂) , k,uv₁uv₂∈f'l₁f'l₂))
|
||||
|
|
|
|||
|
|
@ -1,6 +1,5 @@
|
|||
module Utils where
|
||||
|
||||
open import Agda.Primitive using () renaming (_⊔_ to _⊔ℓ_)
|
||||
open import Data.Nat using (ℕ; suc)
|
||||
open import Data.List using (List; []; _∷_; _++_)
|
||||
open import Data.List.Membership.Propositional using (_∈_)
|
||||
|
|
@ -44,9 +43,3 @@ 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)
|
||||
|
||||
data Pairwise {a} {b} {c} {A : Set a} {B : Set b} (P : A → B → Set c) : List A → List B → Set (a ⊔ℓ b ⊔ℓ c) where
|
||||
[] : Pairwise P [] []
|
||||
_∷_ : ∀ {x : A} {y : B} {xs : List A} {ys : List B} →
|
||||
P x y → Pairwise P xs ys →
|
||||
Pairwise P (x ∷ xs) (y ∷ ys)
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user