Make auxillary definitions private

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

Isomorphism.agda

@@ -31,25 +31,26 @@ module TransportFiniteHeight
     open import Chain _≈₁_ ≈₁-equiv _≺₁_ ≺₁-cong using () renaming (Chain to Chain₁; done to done₁; step to step₁)
     open import Chain _≈₂_ ≈₂-equiv _≺₂_ ≺₂-cong using () renaming (Chain to Chain₂; done to done₂; step to step₂)
 
-    f-Injective : Injective _≈₁_ _≈₂_ f
-    f-Injective {x} {y} fx≈fy = ≈₁-trans (≈₁-sym (inverseʳ x)) (≈₁-trans (g-preserves-≈₂ fx≈fy) (inverseʳ y))
+    private
+        f-Injective : Injective _≈₁_ _≈₂_ f
+        f-Injective {x} {y} fx≈fy = ≈₁-trans (≈₁-sym (inverseʳ x)) (≈₁-trans (g-preserves-≈₂ fx≈fy) (inverseʳ y))
 
-    g-Injective : Injective _≈₂_ _≈₁_ g
-    g-Injective {x} {y} gx≈gy = ≈₂-trans (≈₂-sym (inverseˡ x)) (≈₂-trans (f-preserves-≈₁ gx≈gy) (inverseˡ y))
+        g-Injective : Injective _≈₂_ _≈₁_ g
+        g-Injective {x} {y} gx≈gy = ≈₂-trans (≈₂-sym (inverseˡ x)) (≈₂-trans (f-preserves-≈₁ gx≈gy) (inverseˡ y))
 
-    f-preserves-̷≈ : f Preserves (λ x y → ¬ x ≈₁ y) ⟶  (λ x y → ¬ x ≈₂ y)
-    f-preserves-̷≈ x̷≈y = λ fx≈fy → x̷≈y (f-Injective fx≈fy)
+        f-preserves-̷≈ : f Preserves (λ x y → ¬ x ≈₁ y) ⟶  (λ x y → ¬ x ≈₂ y)
+        f-preserves-̷≈ x̷≈y = λ fx≈fy → x̷≈y (f-Injective fx≈fy)
 
-    g-preserves-̷≈ : g Preserves (λ x y → ¬ x ≈₂ y) ⟶  (λ x y → ¬ x ≈₁ y)
-    g-preserves-̷≈ x̷≈y = λ gx≈gy → x̷≈y (g-Injective gx≈gy)
+        g-preserves-̷≈ : g Preserves (λ x y → ¬ x ≈₂ y) ⟶  (λ x y → ¬ x ≈₁ y)
+        g-preserves-̷≈ x̷≈y = λ gx≈gy → x̷≈y (g-Injective gx≈gy)
 
-    portChain₁ : ∀ {a₁ a₂ : A} {h : ℕ} → Chain₁ a₁ a₂ h → Chain₂ (f a₁) (f a₂) h
-    portChain₁ (done₁ a₁≈a₂) = done₂ (f-preserves-≈₁ a₁≈a₂)
-    portChain₁ (step₁ {a₁} {a₂} (a₁≼a₂ , a₁̷≈a₂) a₂≈a₂' c) = step₂ (≈₂-trans (≈₂-sym (f-⊔-distr a₁ a₂)) (f-preserves-≈₁ a₁≼a₂) , f-preserves-̷≈ a₁̷≈a₂) (f-preserves-≈₁ a₂≈a₂') (portChain₁ c)
+        portChain₁ : ∀ {a₁ a₂ : A} {h : ℕ} → Chain₁ a₁ a₂ h → Chain₂ (f a₁) (f a₂) h
+        portChain₁ (done₁ a₁≈a₂) = done₂ (f-preserves-≈₁ a₁≈a₂)
+        portChain₁ (step₁ {a₁} {a₂} (a₁≼a₂ , a₁̷≈a₂) a₂≈a₂' c) = step₂ (≈₂-trans (≈₂-sym (f-⊔-distr a₁ a₂)) (f-preserves-≈₁ a₁≼a₂) , f-preserves-̷≈ a₁̷≈a₂) (f-preserves-≈₁ a₂≈a₂') (portChain₁ c)
 
-    portChain₂ : ∀ {b₁ b₂ : B} {h : ℕ} → Chain₂ b₁ b₂ h → Chain₁ (g b₁) (g b₂) h
-    portChain₂ (done₂ a₂≈a₁) = done₁ (g-preserves-≈₂ a₂≈a₁)
-    portChain₂ (step₂ {b₁} {b₂} (b₁≼b₂ , b₁̷≈b₂) b₂≈b₂' c) = step₁ (≈₁-trans (≈₁-sym (g-⊔-distr b₁ b₂)) (g-preserves-≈₂ b₁≼b₂) , g-preserves-̷≈ b₁̷≈b₂) (g-preserves-≈₂ b₂≈b₂') (portChain₂ c)
+        portChain₂ : ∀ {b₁ b₂ : B} {h : ℕ} → Chain₂ b₁ b₂ h → Chain₁ (g b₁) (g b₂) h
+        portChain₂ (done₂ a₂≈a₁) = done₁ (g-preserves-≈₂ a₂≈a₁)
+        portChain₂ (step₂ {b₁} {b₂} (b₁≼b₂ , b₁̷≈b₂) b₂≈b₂' c) = step₁ (≈₁-trans (≈₁-sym (g-⊔-distr b₁ b₂)) (g-preserves-≈₂ b₁≼b₂) , g-preserves-̷≈ b₁̷≈b₂) (g-preserves-≈₂ b₂≈b₂') (portChain₂ c)
 
     isFiniteHeightLattice : IsFiniteHeightLattice B height _≈₂_ _⊔₂_ _⊓₂_
     isFiniteHeightLattice =

Lattice/FiniteValueMap.agda

@@ -19,7 +19,11 @@ open import Data.List using (List; length; []; _∷_)
 open import Utils using (Unique; push; empty)
 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.FiniteMap A B _≈₂_ _⊔₂_ _⊓₂_ ≈-dec-A lB public
 
 module IterProdIsomorphism where
@@ -35,7 +39,15 @@ module IterProdIsomorphism where
     to {[]} _ ⊤ = (([] , empty) , refl)
     to {k ∷ ks'} (push k≢ks' uks') (v , rest)
         with to uks' rest
-    ...   | ((kvs' , ukvs') , refl) = (((k , v) ∷ kvs' , push k≢ks' ukvs') , refl)
+    ...   | ((kvs' , ukvs') , kvs'≡ks') =
+            let
+                -- This would be easier if we pattern matched on the equiality proof
+                -- to get refl, but that makes it harder to reason about 'to' when
+                -- the arguments are not known to be refl.
+                k≢kvs' = subst (λ ks → All (λ k' → ¬ k ≡ k') ks) (sym kvs'≡ks') k≢ks'
+                kvs≡ks = cong (k ∷_) kvs'≡ks'
+            in
+                (((k , v) ∷ kvs' , push k≢kvs' ukvs') , kvs≡ks)
 
 
     private
@@ -55,3 +67,27 @@ module IterProdIsomorphism where
             -- but we end up with the 'unpacked' form (kvs', ...). So, put it back
             -- in the 'packed' form after we've performed enough inspection
             -- to know we take the cons branch of `to`.
+
+    -- The map has its own uniqueness proof, but the call to 'to' needs a standalone
+    -- uniqueness proof too. Work with both proofs as needed to thread things through.
+    from-to-inverseʳ : ∀ {ks : List A} (uks : Unique ks) →
+                       Inverseʳ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {ks}) (from {ks}) (to {ks} uks) -- to (from x) = x
+    from-to-inverseʳ {[]} _ (([] , empty) , kvs≡ks) rewrite kvs≡ks = ((λ k v ()) , (λ k v ()))
+    from-to-inverseʳ {k ∷ ks'} uks@(push k≢ks'₁ uks'₁) fm₁@(m₁@((k , v) ∷ kvs'₁ , push k≢ks'₂ uks'₂) , refl)
+        with to uks'₁ (from ((kvs'₁ , uks'₂) , refl)) | from-to-inverseʳ {ks'} uks'₁ ((kvs'₁ , uks'₂) , refl)
+    ...   | ((kvs'₂ , ukvs'₂) , _) | (kvs'₂⊆kvs'₁ , kvs'₁⊆kvs'₂) = (m₂⊆m₁ , m₁⊆m₂)
+                where
+                    kvs₁ = (k , v) ∷ kvs'₁
+                    kvs₂ = (k , v) ∷ kvs'₂
+
+                    m₁⊆m₂ : subset-impl kvs₁ kvs₂
+                    m₁⊆m₂ k' v' (here refl) = (v' , (IsLattice.≈-refl lB , here refl))
+                    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'₂))
+
+                    m₂⊆m₁ : subset-impl kvs₂ kvs₁
+                    m₂⊆m₁ k' v' (here refl) = (v' , (IsLattice.≈-refl lB , here refl))
+                    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'₁))

Lattice/Map.agda

@@ -479,7 +479,7 @@ _∈k_ k m = MemProp._∈_ k (keys m)
 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
 
-open ImplRelation renaming (subset to subset-impl)
+open ImplRelation using () renaming (subset to subset-impl) public
 
 _⊆_ : Map → Map → Set (a ⊔ℓ b)
 _⊆_ (kvs₁ , _) (kvs₂ , _) = subset-impl kvs₁ kvs₂