Prove one absorption law
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
990a785463
commit
dc405b989f
61
Map.agda
61
Map.agda
@ -2,7 +2,7 @@ open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym;
|
||||
open import Relation.Binary.Definitions using (Decidable)
|
||||
open import Relation.Binary.Core using (Rel)
|
||||
open import Relation.Nullary using (Dec; yes; no; Reflects; ofʸ; ofⁿ)
|
||||
open import Agda.Primitive using (Level; _⊔_)
|
||||
open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
|
||||
|
||||
module Map {a b : Level} (A : Set a) (B : Set b)
|
||||
(≡-dec-A : Decidable (_≡_ {a} {A}))
|
||||
@ -94,7 +94,7 @@ private module _ where
|
||||
private module ImplRelation (_≈_ : B → B → Set b) where
|
||||
open MemProp using (_∈_)
|
||||
|
||||
subset : List (A × B) → List (A × B) → Set (a ⊔ b)
|
||||
subset : List (A × B) → List (A × B) → Set (a ⊔ℓ b)
|
||||
subset m₁ m₂ = ∀ (k : A) (v : B) → (k , v) ∈ m₁ →
|
||||
Σ B (λ v' → v ≈ v' × ((k , v') ∈ m₂))
|
||||
|
||||
@ -440,10 +440,10 @@ private module ImplInsert (f : B → B → B) where
|
||||
restrict-preserves-∈₂ (∈-cong proj₁ k,v₁∈l₁) (updates-combine u₁ u₂ k,v₁∈l₁ k,v₂∈l₂)
|
||||
|
||||
|
||||
Map : Set (a ⊔ b)
|
||||
Map : Set (a ⊔ℓ b)
|
||||
Map = Σ (List (A × B)) (λ l → Unique (keys l))
|
||||
|
||||
_∈_ : (A × B) → Map → Set (a ⊔ b)
|
||||
_∈_ : (A × B) → Map → Set (a ⊔ℓ b)
|
||||
_∈_ p (kvs , _) = MemProp._∈_ p kvs
|
||||
|
||||
_∈k_ : A → Map → Set a
|
||||
@ -452,7 +452,7 @@ _∈k_ k (kvs , _) = MemProp._∈_ k (keys kvs)
|
||||
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
|
||||
|
||||
data Expr : Set (a ⊔ b) where
|
||||
data Expr : Set (a ⊔ℓ b) where
|
||||
`_ : Map → Expr
|
||||
_∪_ : Expr → Expr → Expr
|
||||
_∩_ : Expr → Expr → Expr
|
||||
@ -491,7 +491,7 @@ module _ (fUnion : B → B → B) (fIntersect : B → B → B) where
|
||||
⟦ e₁ ∪ e₂ ⟧ = union fUnion ⟦ e₁ ⟧ ⟦ e₂ ⟧
|
||||
⟦ e₁ ∩ e₂ ⟧ = intersect fIntersect ⟦ e₁ ⟧ ⟦ e₂ ⟧
|
||||
|
||||
data Provenance (k : A) : B → Expr → Set (a ⊔ b) where
|
||||
data Provenance (k : A) : B → Expr → Set (a ⊔ℓ b) where
|
||||
single : ∀ {v : B} {m : Map} → (k , v) ∈ m → Provenance k v (` m)
|
||||
in₁ : ∀ {v : B} {e₁ e₂ : Expr} → Provenance k v e₁ → ¬ k ∈k ⟦ e₂ ⟧ → Provenance k v (e₁ ∪ e₂)
|
||||
in₂ : ∀ {v : B} {e₁ e₂ : Expr} → ¬ k ∈k ⟦ e₁ ⟧ → Provenance k v e₂ → Provenance k v (e₁ ∪ e₂)
|
||||
@ -527,16 +527,16 @@ module _ (fUnion : B → B → B) (fIntersect : B → B → B) where
|
||||
module _ (_≈_ : B → B → Set b) where
|
||||
open ImplRelation _≈_ renaming (subset to subset-impl)
|
||||
|
||||
subset : Map → Map → Set (a ⊔ b)
|
||||
subset : Map → Map → Set (a ⊔ℓ b)
|
||||
subset (kvs₁ , _) (kvs₂ , _) = subset-impl kvs₁ kvs₂
|
||||
|
||||
lift : Map → Map → Set (a ⊔ b)
|
||||
lift : Map → Map → Set (a ⊔ℓ b)
|
||||
lift m₁ m₂ = subset m₁ m₂ × subset m₂ m₁
|
||||
|
||||
module _ (≈-refl : ∀ {b : B} → b ≈ b)
|
||||
(≈-sym : ∀ {b₁ b₂ : B} → b₁ ≈ b₂ → b₂ ≈ b₁)
|
||||
(f : B → B → B) where
|
||||
module I = ImplInsert f
|
||||
private module I = ImplInsert f
|
||||
|
||||
-- The Provenance type requires both union and intersection functions,
|
||||
-- but here we're working with one operation only. Just use the union function
|
||||
@ -676,3 +676,46 @@ module _ (_≈_ : B → B → Set b) where
|
||||
... | (_ , (bothⁱ (single {v₁} v₁∈e₁) (bothⁱ (single {v₂} v₂∈e₂) (single {v₃} v₃∈e₃)) , v₁v₂v₃∈m₁m₂₃))
|
||||
rewrite Map-functional {m = intersect f m₁ (intersect f m₂ m₃)} k,v∈m₁m₂₃ v₁v₂v₃∈m₁m₂₃ =
|
||||
(f (f v₁ v₂) v₃ , (≈-sym (f-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₃))
|
||||
|
||||
module _ (≈-refl : ∀ {b : B} → b ≈ b)
|
||||
(≈-sym : ∀ {b₁ b₂ : B} → b₁ ≈ b₂ → b₂ ≈ b₁)
|
||||
(_⊔₂_ : B → B → B) (_⊓₂_ : B → B → B)
|
||||
(⊔₂-idemp : ∀ (b : B) → (b ⊔₂ b) ≈ b)
|
||||
(⊓₂-idemp : ∀ (b : B) → (b ⊓₂ b) ≈ b)
|
||||
(⊔₂-⊓₂-absorb : ∀ {b₁ b₂ : B} → (b₁ ⊔₂ (b₁ ⊓₂ b₂)) ≈ b₁)
|
||||
(⊓₂-⊔₂-absorb : ∀ {b₁ b₂ : B} → (b₁ ⊓₂ (b₁ ⊔₂ b₂)) ≈ b₁)
|
||||
where
|
||||
private module I⊔ = ImplInsert _⊔₂_
|
||||
private module I⊓ = ImplInsert _⊓₂_
|
||||
|
||||
private
|
||||
_⊔_ = union _⊔₂_
|
||||
_⊓_ = intersect _⊓₂_
|
||||
|
||||
intersect-union-absorb : ∀ (m₁ m₂ : Map) → lift (m₁ ⊓ (m₁ ⊔ m₂)) m₁
|
||||
intersect-union-absorb m₁@(l₁ , u₁) m₂@(l₂ , u₂) = (intersect-union-absorb₁ , intersect-union-absorb₂)
|
||||
where
|
||||
intersect-union-absorb₁ : subset (m₁ ⊓ (m₁ ⊔ m₂)) m₁
|
||||
intersect-union-absorb₁ k v k,v∈m₁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 , 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₁ _ ) , _)) = absurd (k∉m₁ (∈-cong proj₁ k,v₁∈m₁))
|
||||
|
||||
intersect-union-absorb₂ : subset m₁ (m₁ ⊓ (m₁ ⊔ m₂))
|
||||
intersect-union-absorb₂ k v k,v∈m₁
|
||||
with ∈k-dec k l₂
|
||||
... | yes k∈km₂ =
|
||||
let (v₂ , k,v₂∈m₂) = locate k∈km₂
|
||||
in (v ⊓₂ (v ⊔₂ v₂) , (≈-sym ⊓₂-⊔₂-absorb , I⊓.intersect-combines u₁ (I⊔.union-preserves-Unique l₁ l₂ u₂) k,v∈m₁ (I⊔.union-combines u₁ u₂ k,v∈m₁ k,v₂∈m₂)))
|
||||
... | no k∉km₂ = (v ⊓₂ v , (≈-sym (⊓₂-idemp v) , I⊓.intersect-combines u₁ (I⊔.union-preserves-Unique l₁ l₂ u₂) k,v∈m₁ (I⊔.union-preserves-∈₁ u₁ k,v∈m₁ k∉km₂)))
|
||||
|
||||
Loading…
Reference in New Issue
Block a user