From 53a08b8f79d95d60ada0a325170cef570226be23 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 25 Feb 2024 18:08:03 -0800 Subject: [PATCH] Prove that 'first' presrves equality Signed-off-by: Danila Fedorin --- Lattice/FiniteValueMap.agda | 51 ++++++++++++++++++++++++++++++++++--- 1 file changed, 48 insertions(+), 3 deletions(-) diff --git a/Lattice/FiniteValueMap.agda b/Lattice/FiniteValueMap.agda index 5f43e3c..d187626 100644 --- a/Lattice/FiniteValueMap.agda +++ b/Lattice/FiniteValueMap.agda @@ -16,20 +16,23 @@ module Lattice.FiniteValueMap (A : Set) (B : Set) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where open import Data.List using (List; length; []; _∷_) -open import Utils using (Unique; push; empty) +open import Data.Product using (Σ; proj₁; proj₂; _×_) +open import Data.Empty using (⊥-elim) +open import Utils using (Unique; push; empty; All¬-¬Any) open import Data.Product using (_,_) open import Data.List.Properties using (∷-injectiveʳ) 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) +open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≈-dec-A lB using (subset-impl; locate; forget; _∈_; Map-functional) open import Lattice.FiniteMap A B _≈₂_ _⊔₂_ _⊓₂_ ≈-dec-A lB public module IterProdIsomorphism where open import Data.Unit using (⊤; tt) - open import Lattice.Unit using () renaming (_≈_ to _≈ᵘ_; _⊔_ to _⊔ᵘ_; _⊓_ to _⊓ᵘ_; ≈-dec to ≈ᵘ-dec; isLattice to isLatticeᵘ) + open import Lattice.Unit using () renaming (_≈_ to _≈ᵘ_; _⊔_ to _⊔ᵘ_; _⊓_ to _⊓ᵘ_; ≈-dec to ≈ᵘ-dec; isLattice to isLatticeᵘ; ≈-equiv to ≈ᵘ-equiv) open import Lattice.IterProd _≈₂_ _≈ᵘ_ _⊔₂_ _⊔ᵘ_ _⊓₂_ _⊓ᵘ_ lB isLatticeᵘ as IP using (IterProd) + open IsLattice lB using () renaming (≈-trans to ≈₂-trans; ≈-sym to ≈₂-sym) from : ∀ {ks : List A} → FiniteMap ks → IterProd (length ks) from {[]} (([] , _) , _) = tt @@ -54,6 +57,9 @@ module IterProdIsomorphism where _≈ᵐ_ : ∀ {ks : List A} → FiniteMap ks → FiniteMap ks → Set _≈ᵐ_ {ks} = _≈_ ks + _⊆ᵐ_ : ∀ {ks₁ ks₂ : List A} → FiniteMap ks₁ → FiniteMap ks₂ → Set + _⊆ᵐ_ fm₁ fm₂ = subset-impl (proj₁ (proj₁ fm₁)) (proj₁ (proj₁ fm₂)) + _≈ⁱᵖ_ : ∀ {ks : List A} → IterProd (length ks) → IterProd (length ks) → Set _≈ⁱᵖ_ {ks} = IP._≈_ (length ks) @@ -91,3 +97,42 @@ module IterProdIsomorphism where m₂⊆m₁ k' v' (there k',v'∈kvs'₂) = let (v'' , (v'≈v'' , k',v''∈kvs'₁)) = kvs'₂⊆kvs'₁ k' v' k',v'∈kvs'₂ in (v'' , (v'≈v'' , there k',v''∈kvs'₁)) + + private + first-key-in-map : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) → Σ B (λ v → (k , v) ∈ proj₁ fm) + first-key-in-map (((k , v) ∷ _ , _) , refl) = (v , here refl) + + from-first-value : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) → proj₁ (from fm) ≈₂ proj₁ (first-key-in-map fm) + from-first-value {k} {ks} (((k , v) ∷ _ , push _ _) , refl) = IsLattice.≈-refl lB + + pop : ∀ {k : A} {ks : List A} → FiniteMap (k ∷ ks) → FiniteMap ks + pop (((_ ∷ kvs') , push _ ukvs') , refl) = ((kvs' , ukvs') , refl) + + pop-≈ : ∀ {k : A} {ks : List A} (fm₁ fm₂ : FiniteMap (k ∷ ks)) → fm₁ ≈ᵐ fm₂ → pop fm₁ ≈ᵐ pop fm₂ + pop-≈ {k} {ks} fm₁ fm₂ (fm₁⊆fm₂ , fm₂⊆fm₁) = (narrow fm₁⊆fm₂ , narrow fm₂⊆fm₁) + where + narrow₁ : ∀ {fm₁ fm₂ : FiniteMap (k ∷ ks)} → fm₁ ⊆ᵐ fm₂ → pop fm₁ ⊆ᵐ fm₂ + narrow₁ {(_ ∷ _ , push _ _) , refl} kvs₁⊆kvs₂ k' v' k',v'∈kvs'₁ = kvs₁⊆kvs₂ k' v' (there k',v'∈kvs'₁) + + narrow₂ : ∀ {fm₁ : FiniteMap ks} {fm₂ : FiniteMap (k ∷ ks)} → fm₁ ⊆ᵐ fm₂ → fm₁ ⊆ᵐ pop fm₂ + narrow₂ {fm₁} {fm₂ = (_ ∷ kvs'₂ , push k≢ks _) , kvs≡ks@refl} kvs₁⊆kvs₂ k' v' k',v'∈kvs'₁ + with kvs₁⊆kvs₂ k' v' k',v'∈kvs'₁ + ... | (v'' , (v'≈v'' , here refl)) rewrite sym (proj₂ fm₁) = ⊥-elim (All¬-¬Any k≢ks (forget {m = proj₁ fm₁} k',v'∈kvs'₁)) + ... | (v'' , (v'≈v'' , there k',v'∈kvs'₂)) = (v'' , (v'≈v'' , k',v'∈kvs'₂)) + + narrow : ∀ {fm₁ fm₂ : FiniteMap (k ∷ ks)} → fm₁ ⊆ᵐ fm₂ → pop fm₁ ⊆ᵐ pop fm₂ + narrow {fm₁} {fm₂} x = narrow₂ {pop fm₁} (narrow₁ {fm₂ = fm₂} x) + + from-rest : ∀ {k : A} {ks : List A} (fm : FiniteMap (k ∷ ks)) → proj₂ (from fm) ≡ from (pop fm) + from-rest (((_ ∷ kvs') , push _ ukvs') , refl) = refl + + from-preserves-≈ : ∀ {ks : List A} → (fm₁ fm₂ : FiniteMap ks) → fm₁ ≈ᵐ fm₂ → (_≈ⁱᵖ_ {ks}) (from fm₁) (from fm₂) + from-preserves-≈ {[]} (([] , _) , _) (([] , _) , _) _ = IsEquivalence.≈-refl ≈ᵘ-equiv + from-preserves-≈ {k ∷ ks'} fm₁@(m₁ , _) fm₂@(m₂ , _) fm₁≈fm₂@(kvs₁⊆kvs₂ , kvs₂⊆kvs₁) + with first-key-in-map fm₁ | first-key-in-map fm₂ | from-first-value fm₁ | from-first-value fm₂ + ... | (v₁ , k,v₁∈fm₁) | (v₂ , k,v₂∈fm₂) | fv₁≈v₁ | fv₂≈v₂ + with kvs₁⊆kvs₂ _ _ k,v₁∈fm₁ + ... | (v₁' , (v₁≈v₁' , k,v₁'∈fm₂)) + rewrite Map-functional {m = m₂} k,v₂∈fm₂ k,v₁'∈fm₂ + rewrite from-rest fm₁ rewrite from-rest fm₂ + = (≈₂-trans fv₁≈v₁ (≈₂-trans v₁≈v₁' (≈₂-sym fv₂≈v₂)) , from-preserves-≈ (pop fm₁) (pop fm₂) (pop-≈ fm₁ fm₂ fm₁≈fm₂))