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

Finish proof of from distributivity

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-02-26 00:00:18 -08:00
parent b083561629
commit 8715d6d89c
2 changed files with 41 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

40
Lattice/FiniteValueMap.agda
View File

@ -25,7 +25,7 @@ open import Data.List.Relation.Unary.All using (All)
open import Data.List.Relation.Unary.Any using (Any; here; there)
open import Relation.Nullary using (¬_)
open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≈-dec-A lB using (subset-impl; locate; forget; _∈_; Map-functional; Expr-Provenance; _∩_; _∪_; `_; in₁; in₂; bothᵘ; single)
open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≈-dec-A lB using (subset-impl; locate; forget; _∈_; Map-functional; Expr-Provenance; _∩_; _∪_; `_; in₁; in₂; bothᵘ; single; ⊔-combines)
open import Lattice.FiniteMap A B _≈₂_ _⊔₂_ _⊓₂_ ≈-dec-A lB public
module IterProdIsomorphism where
@ -69,6 +69,9 @@ module IterProdIsomorphism where
_⊔ⁱᵖ_ : ∀ {ks : List A} → IterProd (length ks) → IterProd (length ks) → IterProd (length ks)
_⊔ⁱᵖ_ {ks} = IP._⊔_ (length ks)
_∈ᵐ_ : ∀ {ks : List A} → A × B → FiniteMap ks → Set
_∈ᵐ_ {ks} k,v fm = k,v ∈ proj₁ fm
from-to-inverseˡ : ∀ {ks : List A} (uks : Unique ks) →
Inverseˡ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {ks}) (from {ks}) (to {ks} uks) -- from (to x) = x
from-to-inverseˡ {[]} _ _ = IsEquivalence.≈-refl (IP.≈-equiv 0)
@ -133,8 +136,41 @@ module IterProdIsomorphism where
narrow : ∀ {fm₁ fm₂ : FiniteMap (k ∷ ks)} → fm₁ ⊆ᵐ fm₂ → pop fm₁ ⊆ᵐ pop fm₂
narrow {fm₁} {fm₂} x = narrow₂ {pop fm₁} (narrow₁ {fm₂ = fm₂} x)
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 , _) ∷ kvs' , push k≢ks uks') , refl) k',v∈fm =
((λ { refl → All¬-¬Any k≢ks (forget {m = (kvs' , uks')} k',v∈fm) }), there k',v∈fm)
k,v∈⇒k,v∈pop : ∀ {k : A} {ks : List A} {k' : A} {v : B} (fm : FiniteMap (k ∷ ks)) → ¬ k ≡ k' → (k' , v) ∈ᵐ fm → (k' , v) ∈ᵐ pop fm
k,v∈⇒k,v∈pop {k} {ks} {k'} {v} (m@((k , _) ∷ kvs' , push k≢ks uks') , refl) k≢k' (here refl) = ⊥-elim (k≢k' refl)
k,v∈⇒k,v∈pop {k} {ks} {k'} {v} (m@((k , _) ∷ kvs' , push k≢ks uks') , refl) k≢k' (there k,v'∈kvs') = k,v'∈kvs'
Provenance-union : ∀ {ks : List A} (fm₁ fm₂ : FiniteMap ks) (k : A) (v : B) → (k , v) ∈ᵐ (fm₁ ⊔ᵐ fm₂) → Σ (B × B) (λ (v₁ , v₂) → ((v ≡ v₁ ⊔₂ v₂) × ((k , v₁) ∈ᵐ fm₁ × (k , v₂) ∈ᵐ fm₂)))
Provenance-union fm₁@(m₁ , ks₁≡ks) fm₂@(m₂ , ks₂≡ks) k v k,v∈fm₁fm₂
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 {m = m₂} k,v∈m₂) rewrite trans ks₁≡ks (sym ks₂≡ks) = ⊥-elim (k∉km₁ k∈km₂)
... | (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)) → pop (fm₁ ⊔ᵐ fm₂) ≈ᵐ (pop fm₁ ⊔ᵐ pop fm₂)
pop-⊔-distr = {!!} -- pop (fm₁ ⊔ fm₂) ⊆ pop fm₁ ⊔ pop fm₂ etc.
pop-⊔-distr {k} {ks} fm₁@(m₁ , _) fm₂@(m₂ , _) = (pfm₁fm₂⊆pfm₁pfm₂ , pfm₁pfm₂⊆pfm₁fm₂)
where
-- pfm₁fm₂⊆pfm₁pfm₂ = {!!}
pfm₁fm₂⊆pfm₁pfm₂ : pop (fm₁ ⊔ᵐ fm₂) ⊆ᵐ (pop fm₁ ⊔ᵐ pop fm₂)
pfm₁fm₂⊆pfm₁pfm₂ k' v' k',v'∈pfm₁fm₂
with (k≢k' , k',v'∈fm₁fm₂) ← k,v∈pop⇒k,v∈ (fm₁ ⊔ᵐ fm₂) k',v'∈pfm₁fm₂
with ((v₁ , v₂) , (refl , (k,v₁∈fm₁ , k,v₂∈fm₂))) ← Provenance-union fm₁ fm₂ k' v' k',v'∈fm₁fm₂
with k',v₁∈pfm₁ ← k,v∈⇒k,v∈pop fm₁ k≢k' k,v₁∈fm₁
with k',v₂∈pfm₂ ← k,v∈⇒k,v∈pop fm₂ k≢k' k,v₂∈fm₂
= (v₁ ⊔₂ v₂ , (IsLattice.≈-refl lB , ⊔-combines {m₁ = proj₁ (pop fm₁)} {m₂ = proj₁ (pop fm₂)} k',v₁∈pfm₁ k',v₂∈pfm₂))
pfm₁pfm₂⊆pfm₁fm₂ : (pop fm₁ ⊔ᵐ pop fm₂) ⊆ᵐ pop (fm₁ ⊔ᵐ fm₂)
pfm₁pfm₂⊆pfm₁fm₂ k' v' k',v'∈pfm₁pfm₂
with ((v₁ , v₂) , (refl , (k,v₁∈pfm₁ , k,v₂∈pfm₂))) ← Provenance-union (pop fm₁) (pop fm₂) k' v' k',v'∈pfm₁pfm₂
with (k≢k' , k',v₁∈fm₁) ← k,v∈pop⇒k,v∈ fm₁ k,v₁∈pfm₁
with (_ , k',v₂∈fm₂) ← k,v∈pop⇒k,v∈ fm₂ k,v₂∈pfm₂
= (v₁ ⊔₂ v₂ , (IsLattice.≈-refl lB , k,v∈⇒k,v∈pop (fm₁ ⊔ᵐ fm₂) k≢k' (⊔-combines {m₁ = m₁} {m₂ = m₂} k',v₁∈fm₁ k',v₂∈fm₂)))
from-rest : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) → proj₂ (from fm) ≡ from (pop fm)
from-rest (((_ ∷ kvs') , push _ ukvs') , refl) = refl

3
Lattice/Map.agda
View File

@ -534,6 +534,9 @@ open ImplInsert _⊔₂_ using
; union-preserves-∉
)
⊔-combines : ∀ {k : A} {v₁ v₂ : B} {m₁ m₂ : Map} → (k , v₁) ∈ m₁ → (k , v₂) ∈ m₂ → (k , v₁ ⊔₂ v₂) ∈ (m₁ ⊔ m₂)
⊔-combines {k} {v₁} {v₂} {kvs₁ , u₁} {kvs₂ , u₂} k,v₁∈m₁ k,v₂∈m₂ = union-combines u₁ u₂ k,v₁∈m₁ k,v₂∈m₂
open ImplInsert _⊓₂_ using
( restrict-needs-both
; updates