Add congruence for Map union and intersect

This commit is contained in:
Danila Fedorin 2023-09-03 16:57:56 -07:00
parent 29fb828ee2
commit eee814ae3c

View File

@ -586,16 +586,66 @@ module _ (_≈_ : B → B → Set b) where
... | _ | no m₂̷⊆m₁ = no (λ (_ , m₂⊆m₁) m₂̷⊆m₁ m₂⊆m₁) ... | _ | no m₂̷⊆m₁ = no (λ (_ , m₂⊆m₁) m₂̷⊆m₁ m₂⊆m₁)
... | no m₁̷⊆m₂ | _ = no (λ (m₁⊆m₂ , _) m₁̷⊆m₂ m₁⊆m₂) ... | no m₁̷⊆m₂ | _ = no (λ (m₁⊆m₂ , _) m₁̷⊆m₂ m₁⊆m₂)
-- The Provenance type requires both union and intersection functions,
-- but sometimes here we're working with one operation only. Just use the
-- union/intersection function for both -- it doesn't matter, since we don't
-- use the dual operations in these proofs.
module _ (f : B B B)
(≈-f-cong : {b₁ b₂ b₃ b₄} b₁ b₂ b₃ b₄ f b₁ b₃ f b₂ b₄) where
private module I = ImplInsert f
union-cong : {m₁ m₂ m₃ m₄ : Map} lift m₁ m₂ lift m₃ m₄ lift (union f m₁ m₃) (union f m₂ m₄)
union-cong {m₁} {m₂} {m₃} {m₄} (m₁⊆m₂ , m₂⊆m₁) (m₃⊆m₄ , m₄⊆m₃) =
( union-subset m₁ m₂ m₃ m₄ (m₁⊆m₂ , m₂⊆m₁) (m₃⊆m₄ , m₄⊆m₃)
, union-subset m₂ m₁ m₄ m₃ (m₂⊆m₁ , m₁⊆m₂) (m₄⊆m₃ , m₃⊆m₄)
)
where
≈-∉-cong : {m₁ m₂ : Map} {k : A} lift m₁ m₂ ¬ k ∈k m₁ ¬ k ∈k m₂
≈-∉-cong (m₁⊆m₂ , m₂⊆m₁) k∉km₁ k∈km₂ =
let (v₂ , k,v₂∈m₂) = locate k∈km₂
(_ , (_ , k,v₁∈m₁)) = m₂⊆m₁ _ v₂ k,v₂∈m₂
in k∉km₁ (∈-cong proj₁ k,v₁∈m₁)
union-subset : (m₁ m₂ m₃ m₄ : Map) lift m₁ m₂ lift m₃ m₄ subset (union f m₁ m₃) (union f m₂ m₄)
union-subset m₁ m₂ m₃ m₄ m₁≈m₂ m₃≈m₄ k v k,v∈m₁m₃
with Expr-Provenance f f 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 = union f 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 (f v₂ v₄ , (≈-f-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₃ , v₁∈m₁m₃))
rewrite Map-functional {m = union f 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₃) , v₃∈m₁m₃))
rewrite Map-functional {m = union f 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₄))
intersect-cong : {m₁ m₂ m₃ m₄ : Map} lift m₁ m₂ lift m₃ m₄ lift (intersect f m₁ m₃) (intersect f m₂ m₄)
intersect-cong {m₁} {m₂} {m₃} {m₄} (m₁⊆m₂ , m₂⊆m₁) (m₃⊆m₄ , m₄⊆m₃) =
( intersect-subset m₁ m₂ m₃ m₄ (m₁⊆m₂ , m₂⊆m₁) (m₃⊆m₄ , m₄⊆m₃)
, intersect-subset m₂ m₁ m₄ m₃ (m₂⊆m₁ , m₁⊆m₂) (m₄⊆m₃ , m₃⊆m₄)
)
where
intersect-subset : (m₁ m₂ m₃ m₄ : Map) lift m₁ m₂ lift m₃ m₄ subset (intersect f m₁ m₃) (intersect f m₂ m₄)
intersect-subset m₁ m₂ m₃ m₄ m₁≈m₂ m₃≈m₄ k v k,v∈m₁m₃
with Expr-Provenance f f 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 = intersect f 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 (f v₂ v₄ , (≈-f-cong v₁≈v₂ v₃≈v₄ , I.intersect-combines (proj₂ m₂) (proj₂ m₄) k,v₂∈m₂ k,v₄∈m₄))
module _ (≈-refl : {b : B} b b) module _ (≈-refl : {b : B} b b)
(≈-sym : {b₁ b₂ : B} b₁ b₂ b₂ b₁) (≈-sym : {b₁ b₂ : B} b₁ b₂ b₂ b₁)
(f : B B B) where (f : B B B) where
private 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
-- for both -- it doesn't matter, since we don't use intersection in
-- these proofs.
module _ (f-idemp : (b : B) f b b b) where module _ (f-idemp : (b : B) f b b b) where
union-idemp : (m : Map) lift (union f m m) m union-idemp : (m : Map) lift (union f m m) m
union-idemp m@(l , u) = (mm-m-subset , m-mm-subset) union-idemp m@(l , u) = (mm-m-subset , m-mm-subset)