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

Prove that 'to' preserves equality

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-02-25 18:43:54 -08:00
parent 53a08b8f79
commit 3ad7db738a
1 changed files with 20 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
Lattice/FiniteValueMap.agda
View File

@ -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₂))