From 3ad7db738ade000b846e08951ee4a765942c829d Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 25 Feb 2024 18:43:54 -0800 Subject: [PATCH] Prove that 'to' preserves equality Signed-off-by: Danila Fedorin --- Lattice/FiniteValueMap.agda | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/Lattice/FiniteValueMap.agda b/Lattice/FiniteValueMap.agda index d187626..9dd290f 100644 --- a/Lattice/FiniteValueMap.agda +++ b/Lattice/FiniteValueMap.agda @@ -136,3 +136,23 @@ module IterProdIsomorphism where 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₂)) + + to-preserves-≈ : ∀ {ks : List A} (uks : Unique ks) (ip₁ ip₂ : IterProd (length ks)) → _≈ⁱᵖ_ {ks} ip₁ ip₂ → to uks ip₁ ≈ᵐ to uks ip₂ + to-preserves-≈ {[]} empty tt tt _ = ((λ k v ()), (λ k v ())) + to-preserves-≈ {k ∷ ks'} uks@(push k≢ks' uks') ip₁@(v₁ , rest₁) ip₂@(v₂ , rest₂) (v₁≈v₂ , rest₁≈rest₂) = (fm₁⊆fm₂ , fm₂⊆fm₁) + where + fm₁⊆fm₂ : to uks ip₁ ⊆ᵐ to uks ip₂ + fm₁⊆fm₂ k v k,v∈kvs₁ + with ((kvs'₁ , ukvs'₁) , kvs'₁≡ks') ← to uks' rest₁ in p₁ + with ((kvs'₂ , ukvs'₂) , kvs'₂≡ks') ← to uks' rest₂ in p₂ + with k,v∈kvs₁ + ... | here refl = (v₂ , (v₁≈v₂ , here refl)) + ... | there k,v∈kvs'₁ with refl ← p₁ with refl ← p₂ = let (v' , (v≈v' , k,v'∈kvs₁)) = proj₁ (to-preserves-≈ uks' rest₁ rest₂ rest₁≈rest₂) k v k,v∈kvs'₁ in (v' , (v≈v' , there k,v'∈kvs₁)) + + fm₂⊆fm₁ : to uks ip₂ ⊆ᵐ to uks ip₁ + fm₂⊆fm₁ k v k,v∈kvs₂ + with ((kvs'₁ , ukvs'₁) , kvs'₁≡ks') ← to uks' rest₁ in p₁ + with ((kvs'₂ , ukvs'₂) , kvs'₂≡ks') ← to uks' rest₂ in p₂ + with k,v∈kvs₂ + ... | here refl = (v₁ , (IsLattice.≈-sym lB v₁≈v₂ , here refl)) + ... | there k,v∈kvs'₂ with refl ← p₁ with refl ← p₂ = let (v' , (v≈v' , k,v'∈kvs₂)) = proj₂ (to-preserves-≈ uks' rest₁ rest₂ rest₁≈rest₂) k v k,v∈kvs'₂ in (v' , (v≈v' , there k,v'∈kvs₂))