Use records rather than nested pairs to represent 'fixed height'

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

Analysis/Forward.agda

@@ -19,6 +19,7 @@ open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Data.Unit using (⊤)
 open import Function using (_∘_; flip)
+import Chain
 
 open import Utils using (Pairwise; _⇒_; _∨_)
 import Lattice.FiniteValueMap
@@ -77,7 +78,7 @@ module WithProg (prog : Program) where
     ≈ᵛ-dec = ≈ˡ-dec⇒≈ᵛ-dec ≈ˡ-dec
     joinSemilatticeᵛ = IsFiniteHeightLattice.joinSemilattice isFiniteHeightLatticeᵛ
     fixedHeightᵛ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵛ
-    ⊥ᵛ = proj₁ (proj₁ (proj₁ fixedHeightᵛ))
+    ⊥ᵛ = Chain.Height.⊥ fixedHeightᵛ
 
     -- Finally, the map we care about is (state -> (variables -> value)). Bring that in.
     module StateVariablesFiniteMap = Lattice.FiniteValueMap.WithKeys _≟_ isLatticeᵛ states

Chain.agda

@@ -10,7 +10,7 @@ open import Data.Nat using (ℕ; suc; _+_; _≤_)
 open import Data.Nat.Properties using (+-comm; m+1+n≰m)
 open import Data.Product using (_×_; Σ; _,_)
 open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
-open import Data.Empty using (⊥)
+open import Data.Empty as Empty using ()
 
 open IsEquivalence ≈-equiv
 
@@ -38,11 +38,16 @@ module _  where
     Bounded : ℕ → Set a
     Bounded bound = ∀ {a₁ a₂ : A} {n : ℕ} → Chain a₁ a₂ n → n ≤ bound
 
-    Bounded-suc-n : ∀ {a₁ a₂ : A} {n : ℕ} → Bounded n → Chain a₁ a₂ (suc n) → ⊥
+    Bounded-suc-n : ∀ {a₁ a₂ : A} {n : ℕ} → Bounded n → Chain a₁ a₂ (suc n) → Empty.⊥
     Bounded-suc-n {a₁} {a₂} {n} bounded c = (m+1+n≰m n n+1≤n)
         where
             n+1≤n : n + 1 ≤ n
             n+1≤n rewrite (+-comm n 1) = bounded c
 
-    Height : ℕ → Set a
+    record Height (height : ℕ) : Set a where
-    Height height = (Σ (A × A) (λ (a₁ , a₂) → Chain a₁ a₂ height) × Bounded height)
+        field
+            ⊥ : A
+            ⊤ : A
+
+            longestChain : Chain ⊥ ⊤ height
+            bounded : Bounded height

Fixedpoint.agda

@@ -23,15 +23,21 @@ import Chain
 module ChainA = Chain _≈_ ≈-equiv _≺_ ≺-cong
 
 private
-    ⊥ᴬ : A
+    open ChainA.Height fixedHeight
-    ⊥ᴬ = proj₁ (proj₁ (proj₁ fixedHeight))
+        using ()
+        renaming
+            ( ⊥ to ⊥ᴬ
+            ; longestChain to longestChainᴬ
+            ; bounded to boundedᴬ
+            )
+
 
     ⊥ᴬ≼ : ∀ (a : A) → ⊥ᴬ ≼ a
     ⊥ᴬ≼ a with ≈-dec a ⊥ᴬ
     ...   | yes a≈⊥ᴬ = ≼-cong a≈⊥ᴬ ≈-refl (≼-refl a)
     ...   | no a̷≈⊥ᴬ with ≈-dec ⊥ᴬ (a ⊓ ⊥ᴬ)
     ...         | yes ⊥ᴬ≈a⊓⊥ᴬ = ≈-trans (⊔-comm ⊥ᴬ a) (≈-trans (≈-⊔-cong (≈-refl {a}) ⊥ᴬ≈a⊓⊥ᴬ) (absorb-⊔-⊓ a ⊥ᴬ))
-    ...         | no ⊥ᴬ̷≈a⊓⊥ᴬ = ⊥-elim (ChainA.Bounded-suc-n (proj₂ fixedHeight) (ChainA.step x≺⊥ᴬ ≈-refl (proj₂ (proj₁ fixedHeight))))
+    ...         | no ⊥ᴬ̷≈a⊓⊥ᴬ = ⊥-elim (ChainA.Bounded-suc-n boundedᴬ (ChainA.step x≺⊥ᴬ ≈-refl longestChainᴬ))
                     where
                         ⊥ᴬ⊓a̷≈⊥ᴬ : ¬ (⊥ᴬ ⊓ a) ≈ ⊥ᴬ
                         ⊥ᴬ⊓a̷≈⊥ᴬ = λ ⊥ᴬ⊓a≈⊥ᴬ → ⊥ᴬ̷≈a⊓⊥ᴬ (≈-trans (≈-sym ⊥ᴬ⊓a≈⊥ᴬ) (⊓-comm _ _))
@@ -45,7 +51,7 @@ private
     -- out, we have exceeded h steps, which shouldn't be possible.
 
     doStep : ∀ (g hᶜ : ℕ) (a₁ a₂ : A) (c : ChainA.Chain a₁ a₂ hᶜ) (g+hᶜ≡h : g + hᶜ ≡ suc h) (a₂≼fa₂ : a₂ ≼ f a₂) → Σ A (λ a → a ≈ f a)
-    doStep 0 hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite g+hᶜ≡sh = ⊥-elim (ChainA.Bounded-suc-n (proj₂ fixedHeight) c)
+    doStep 0 hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite g+hᶜ≡sh = ⊥-elim (ChainA.Bounded-suc-n boundedᴬ c)
     doStep (suc g') hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite sym (+-suc g' hᶜ)
         with ≈-dec a₂ (f a₂)
     ...   | yes a₂≈fa₂ = (a₂ , a₂≈fa₂)
@@ -71,7 +77,7 @@ private
                      (c : ChainA.Chain a₁ a₂ hᶜ) (g+hᶜ≡h : g + hᶜ ≡ suc h)
                      (a₂≼fa₂ : a₂ ≼ f a₂) →
                      proj₁ (doStep g hᶜ a₁ a₂ c g+hᶜ≡h a₂≼fa₂) ≼ a
-    stepPreservesLess 0 _ _ _ _ _ _ c g+hᶜ≡sh _ rewrite g+hᶜ≡sh = ⊥-elim (ChainA.Bounded-suc-n (proj₂ fixedHeight) c)
+    stepPreservesLess 0 _ _ _ _ _ _ c g+hᶜ≡sh _ rewrite g+hᶜ≡sh = ⊥-elim (ChainA.Bounded-suc-n boundedᴬ c)
     stepPreservesLess (suc g') hᶜ a₁ a₂ a a≈fa a₂≼a c g+hᶜ≡sh a₂≼fa₂ rewrite sym (+-suc g' hᶜ)
         with ≈-dec a₂ (f a₂)
     ...   | yes _ = a₂≼a

Isomorphism.agda

@@ -38,8 +38,9 @@ module TransportFiniteHeight
     open IsEquivalence ≈₁-equiv using () renaming (≈-sym to ≈₁-sym; ≈-trans to ≈₁-trans)
     open IsEquivalence ≈₂-equiv using () renaming (≈-sym to ≈₂-sym; ≈-trans to ≈₂-trans)
 
-    open import Chain _≈₁_ ≈₁-equiv _≺₁_ ≺₁-cong using () renaming (Chain to Chain₁; done to done₁; step to step₁)
+    import Chain
-    open import Chain _≈₂_ ≈₂-equiv _≺₂_ ≺₂-cong using () renaming (Chain to Chain₂; done to done₂; step to step₂)
+    open Chain _≈₁_ ≈₁-equiv _≺₁_ ≺₁-cong using () renaming (Chain to Chain₁; done to done₁; step to step₁)
+    open Chain _≈₂_ ≈₂-equiv _≺₂_ ≺₂-cong using () renaming (Chain to Chain₂; done to done₂; step to step₂)
 
     private
         f-Injective : Injective _≈₁_ _≈₂_ f
@@ -65,10 +66,17 @@ module TransportFiniteHeight
     isFiniteHeightLattice : IsFiniteHeightLattice B height _≈₂_ _⊔₂_ _⊓₂_
     isFiniteHeightLattice =
         let
-            (((a₁ , a₂) , c) , bounded₁) = IsFiniteHeightLattice.fixedHeight fhlA
+            open Chain.Height (IsFiniteHeightLattice.fixedHeight fhlA)
+                using ()
+                renaming (⊥ to ⊥₁; ⊤ to ⊤₁; bounded to bounded₁; longestChain to c)
         in record
             { isLattice = lB
-            ; fixedHeight = (((f a₁ , f a₂), portChain₁ c) , λ c' → bounded₁ (portChain₂ c'))
+            ; fixedHeight = record
+                { ⊥ = f ⊥₁
+                ; ⊤ = f ⊤₁
+                ; longestChain = portChain₁ c
+                ; bounded = λ c' → bounded₁ (portChain₂ c')
+                }
             }
 
     finiteHeightLattice : FiniteHeightLattice B

Lattice/AboveBelow.agda

@@ -355,7 +355,12 @@ module Plain (x : A) where
         rewrite [x]≺y⇒y≡⊤ _ _ [x]≺y with ≈-⊤-⊤ ← y≈z = ⊥-elim (¬-Chain-⊤ c)
 
     fixedHeight : IsLattice.FixedHeight isLattice 2
-    fixedHeight = (((⊥ , ⊤) , longestChain) , isLongest)
+    fixedHeight = record
+        { ⊥ = ⊥
+        ; ⊤ = ⊤
+        ; longestChain = longestChain
+        ; bounded = isLongest
+        }
 
     isFiniteHeightLattice : IsFiniteHeightLattice AboveBelow 2 _≈_ _⊔_ _⊓_
     isFiniteHeightLattice = record

Lattice/IterProd.agda

@@ -14,6 +14,7 @@ open import Agda.Primitive using (lsuc)
 open import Data.Nat using (ℕ; zero; suc; _+_)
 open import Data.Product using (_×_; _,_; proj₁; proj₂)
 open import Utils using (iterate)
+open import Chain using (Height)
 
 open IsLattice lA renaming (FixedHeight to FixedHeight₁)
 open IsLattice lB renaming (FixedHeight to FixedHeight₂)
@@ -44,10 +45,10 @@ private
             fhB : FixedHeight₂ h₂
 
         ⊥₁ : A
-        ⊥₁ = proj₁ (proj₁ (proj₁ fhA))
+        ⊥₁ = Height.⊥ fhA
 
         ⊥₂ : B
-        ⊥₂ = proj₁ (proj₁ (proj₁ fhB))
+        ⊥₂ = Height.⊥ fhB
 
         ⊥k : ∀ (k : ℕ) → IterProd k
         ⊥k = build ⊥₁ ⊥₂
@@ -58,7 +59,7 @@ private
             fixedHeight : IsLattice.FixedHeight isLattice height
             ≈-dec : IsDecidable _≈_
 
-            ⊥-correct : proj₁ (proj₁ (proj₁ fixedHeight)) ≈ ⊥
+            ⊥-correct : Height.⊥ fixedHeight ≈ ⊥
 
     record Everything (k : ℕ) : Set (lsuc a) where
         T = IterProd k

Lattice/Prod.agda

@@ -143,17 +143,8 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
         ∙,b-Preserves-≈₁ : ∀ (b : B) → (λ a → (a , b)) Preserves _≈₁_ ⟶  _≈_
         ∙,b-Preserves-≈₁ b {a₁} {a₂} a₁≈a₂ = (a₁≈a₂ , ≈₂-refl)
 
-        ⊥₁ : A
+        open ChainA.Height fhA using () renaming (⊥ to ⊥₁; ⊤ to ⊤₁; longestChain to longestChain₁; bounded to bounded₁)
-        ⊥₁ = proj₁ (proj₁ (proj₁ fhA))
+        open ChainB.Height fhB using () renaming (⊥ to ⊥₂; ⊤ to ⊤₂; longestChain to longestChain₂; bounded to bounded₂)
-
-        ⊤₁ : A
-        ⊤₁ = proj₂ (proj₁ (proj₁ fhA))
-
-        ⊥₂ : B
-        ⊥₂ = proj₁ (proj₁ (proj₁ fhB))
-
-        ⊤₂ : B
-        ⊤₂ = proj₂ (proj₁ (proj₁ fhB))
 
         unzip : ∀ {a₁ a₂ : A} {b₁ b₂ : B} {n : ℕ} → Chain (a₁ , b₁) (a₂ , b₂) n → Σ (ℕ × ℕ) (λ (n₁ , n₂) → ((Chain₁ a₁ a₂ n₁ × Chain₂ b₁ b₂ n₂) × (n ≤ n₁ + n₂)))
         unzip (done (a₁≈a₂ , b₁≈b₂)) = ((0 , 0) , ((done₁ a₁≈a₂ , done₂ b₁≈b₂) , ≤-refl))
@@ -172,15 +163,16 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
                                      ))
 
     fixedHeight : IsLattice.FixedHeight isLattice (h₁ + h₂)
-    fixedHeight =
+    fixedHeight = record
-      ( ( ((⊥₁ , ⊥₂) , (⊤₁ , ⊤₂))
+      { ⊥ = (⊥₁ , ⊥₂)
-        , concat
+      ; ⊤ = (⊤₁ , ⊤₂)
-            (ChainMapping₁.Chain-map (λ a → (a , ⊥₂)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) (proj₂ (proj₁ fhA)))
+      ; longestChain = concat
-            (ChainMapping₂.Chain-map (λ b → (⊤₁ , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) (proj₂ (proj₁ fhB)))
+            (ChainMapping₁.Chain-map (λ a → (a , ⊥₂)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) longestChain₁)
-        )
+            (ChainMapping₂.Chain-map (λ b → (⊤₁ , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) longestChain₂)
-      , λ a₁b₁a₂b₂ → let ((n₁ , n₂) , ((a₁a₂ , b₁b₂) , n≤n₁+n₂)) = unzip a₁b₁a₂b₂
+      ; bounded = λ a₁b₁a₂b₂ →
-                     in ≤-trans n≤n₁+n₂ (+-mono-≤ (proj₂ fhA a₁a₂) (proj₂ fhB b₁b₂))
+            let ((n₁ , n₂) , ((a₁a₂ , b₁b₂) , n≤n₁+n₂)) = unzip a₁b₁a₂b₂
-      )
+            in ≤-trans n≤n₁+n₂ (+-mono-≤ (bounded₁ a₁a₂) (bounded₂ b₁b₂))
+      }
 
     isFiniteHeightLattice : IsFiniteHeightLattice (A × B) (h₁ + h₂) _≈_ _⊔_ _⊓_
     isFiniteHeightLattice = record

Lattice/Unit.agda

@@ -108,7 +108,12 @@ private
     isLongest (done _) = z≤n
 
 fixedHeight : IsLattice.FixedHeight isLattice 0
-fixedHeight = (((tt , tt) , longestChain) , isLongest)
+fixedHeight = record
+    { ⊥ = tt
+    ; ⊤ = tt
+    ; longestChain = longestChain
+    ; bounded = isLongest
+    }
 
 isFiniteHeightLattice : IsFiniteHeightLattice ⊤ 0 _≈_ _⊔_ _⊓_
 isFiniteHeightLattice = record