Define to-and-from functions from finite maps to tuples and prove one inverse direction

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

Lattice/FiniteValueMap.agda

@@ -0,0 +1,57 @@
+-- Because iterated products currently require both A and B to be of the same
+-- universe, and the FiniteMap is written in a universe-polymorphic way,
+-- specialize the FiniteMap module with Set-typed types only.
+
+open import Lattice
+open import Equivalence
+open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
+open import Relation.Binary.Definitions using (Decidable)
+open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
+open import Function.Definitions using (Inverseˡ; Inverseʳ)
+
+module Lattice.FiniteValueMap (A : Set) (B : Set)
+    (_≈₂_ : B → B → Set)
+    (_⊔₂_ : B → B → B) (_⊓₂_ : B → B → B)
+    (≈-dec-A : Decidable (_≡_ {_} {A}))
+    (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
+
+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 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.IterProd _≈₂_ _≈ᵘ_ _⊔₂_ _⊔ᵘ_ _⊓₂_ _⊓ᵘ_ lB isLatticeᵘ as IP using (IterProd)
+
+    from : ∀ {ks : List A} → FiniteMap ks → IterProd (length ks)
+    from {[]} (([] , _) , _) = tt
+    from {k ∷ ks'} (((k' , v) ∷ kvs' , push _ uks') , refl) = (v , from ((kvs' , uks'), refl))
+
+    to : ∀ {ks : List A} → Unique ks → IterProd (length ks) → FiniteMap ks
+    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)
+
+
+    private
+        _≈ᵐ_ : ∀ {ks : List A} → FiniteMap ks → FiniteMap ks → Set
+        _≈ᵐ_ {ks} = _≈_ ks
+
+        _≈ⁱᵖ_ : ∀ {ks : List A} → IterProd (length ks) → IterProd (length ks) → Set
+        _≈ⁱᵖ_ {ks} = IP._≈_ (length ks)
+
+    from-to-inverseˡ : ∀ {ks : List A} (uks : Unique ks) →
+                      Inverseˡ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {ks}) (from {ks}) (to {ks} uks) -- from (to x) = x
+    from-to-inverseˡ {[]} _ _ = IsEquivalence.≈-refl (IP.≈-equiv 0)
+    from-to-inverseˡ {k ∷ ks'} (push k≢ks' uks') (v , rest)
+        with ((kvs' , ukvs') , refl) ← to uks' rest in p rewrite sym p =
+            (IsLattice.≈-refl lB , from-to-inverseˡ {ks'} uks' rest)
+            -- the rewrite here is needed because the IH is in terms of `to uks' rest`,
+            -- 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`.

Lattice/IterProd.agda

@@ -1,5 +1,9 @@
 open import Lattice
 
+-- Due to universe levels, it becomes relatively annoying to handle the case
+-- where the levels of A and B are not the same. For the time being, constrain
+-- them to be the same.
+
 module Lattice.IterProd {a} {A B : Set a}
     (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a)
     (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)

Lattice/Prod.agda

@@ -1,11 +1,12 @@
 open import Lattice
 
-module Lattice.Prod {a} {A B : Set a}
-    (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a)
+module Lattice.Prod {a b} {A : Set a} {B : Set b}
+    (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set b)
     (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)
     (_⊓₁_ : A → A → A) (_⊓₂_ : B → B → B)
     (lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
 
+open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
 open import Data.Nat using (ℕ; _≤_; _+_; suc)
 open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
 open import Data.Empty using (⊥-elim)
@@ -35,7 +36,7 @@ open IsLattice lB using () renaming
     ; ≺-cong to ≺₂-cong
     )
 
-_≈_ : A × B → A × B → Set a
+_≈_ : A × B → A × B → Set (a ⊔ℓ b)
 (a₁ , b₁) ≈ (a₂ , b₂) = (a₁ ≈₁ a₂) × (b₁ ≈₂ b₂)
 
 ≈-equiv : IsEquivalence (A × B) _≈_