Re-write the IterProd proofs to couple lattice and finite height lattice

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

Lattice/IterProd.agda

@@ -23,94 +23,97 @@ IterProd k = iterate k (λ t → A × t) B
 
 -- To make iteration more convenient, package the definitions in Lattice
 -- records, perform the recursion, and unpackage.
+--
 
-module _ where
+-- If we prove isLattice and isFiniteHeightLattice by induction separately,
-    lattice : ∀ {k : ℕ} → Lattice (IterProd k)
+-- we lose the connection between the operations (which should be the same)
-    lattice {0} = record
+-- that are built up by the two iterations. So, do everything in one iteration.
+-- This requires some odd code.
+
+private
+    record RequiredForFixedHeight : Set (lsuc a) where
+         field
+            ≈₁-dec : IsDecidable _≈₁_
+            ≈₂-dec : IsDecidable _≈₂_
+            h₁ h₂ : ℕ
+            fhA : FixedHeight₁ h₁
+            fhB : FixedHeight₂ h₂
+
+    record IsFiniteHeightAndDecEq {A : Set a} {_≈_ : A → A → Set a} {_⊔_ : A → A → A} {_⊓_ : A → A → A} (isLattice : IsLattice A _≈_ _⊔_ _⊓_) : Set (lsuc a) where
+        field
+            height : ℕ
+            fixedHeight : IsLattice.FixedHeight isLattice height
+            ≈-dec : IsDecidable _≈_
+
+    record Everything (A : Set a) : Set (lsuc a) where
+        field
+            _≈_ : A → A → Set a
+            _⊔_ : A → A → A
+            _⊓_ : A → A → A
+
+            isLattice : IsLattice A _≈_ _⊔_ _⊓_
+            isFiniteHeightIfSupported : RequiredForFixedHeight → IsFiniteHeightAndDecEq isLattice
+
+    everything : ∀ (k : ℕ) → Everything (IterProd k)
+    everything 0 = record
         { _≈_ = _≈₂_
         ; _⊔_ = _⊔₂_
         ; _⊓_ = _⊓₂_
         ; isLattice = lB
+        ; isFiniteHeightIfSupported = λ req → record
+            { height = RequiredForFixedHeight.h₂ req
+            ; fixedHeight = RequiredForFixedHeight.fhB req
+            ; ≈-dec = RequiredForFixedHeight.≈₂-dec req
+            }
         }
-    lattice {suc k'} = record
+    everything (suc k') = record
-        { _≈_ = _≈_
+        { _≈_ = P._≈_
-        ; _⊔_ = _⊔_
+        ; _⊔_ = P._⊔_
-        ; _⊓_ = _⊓_
+        ; _⊓_ = P._⊓_
-        ; isLattice = isLattice
+        ; isLattice = P.isLattice
+        ; isFiniteHeightIfSupported = λ req →
+            let
+                fhlRest = Everything.isFiniteHeightIfSupported everythingRest req
+            in
+                record
+                    { height = (RequiredForFixedHeight.h₁ req) + IsFiniteHeightAndDecEq.height fhlRest
+                    ; fixedHeight =
+                        P.fixedHeight
+                        (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightAndDecEq.≈-dec fhlRest)
+                        (RequiredForFixedHeight.h₁ req) (IsFiniteHeightAndDecEq.height fhlRest)
+                        (RequiredForFixedHeight.fhA req) (IsFiniteHeightAndDecEq.fixedHeight fhlRest)
+                    ; ≈-dec = P.≈-dec (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightAndDecEq.≈-dec fhlRest)
+                    }
         }
         where
-            Right : Lattice (IterProd k')
+            everythingRest = everything k'
-            Right = lattice {k'}
 
-            open import Lattice.Prod
+            import Lattice.Prod
-                _≈₁_ (Lattice._≈_ Right)
+                _≈₁_ (Everything._≈_ everythingRest)
-                _⊔₁_ (Lattice._⊔_ Right)
+                _⊔₁_ (Everything._⊔_ everythingRest)
-                _⊓₁_ (Lattice._⊓_ Right)
+                _⊓₁_ (Everything._⊓_ everythingRest)
-                lA  (Lattice.isLattice Right)
+                lA  (Everything.isLattice everythingRest) as P
 
 module _ (k : ℕ) where
-    open Lattice.Lattice (lattice {k}) public
+    open Everything (everything k) using (_≈_; _⊔_; _⊓_; isLattice) public
+    open Lattice.IsLattice isLattice public
 
-module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
+    module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
-         (h₁ h₂ : ℕ)
+             (h₁ h₂ : ℕ)
-         (fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where
+             (fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where
-
-    private module _ where
-        record FiniteHeightAndDecEq (A : Set a) : Set (lsuc a) where
-            field
-                height : ℕ
-                _≈_ : A → A → Set a
-                _⊔_ : A → A → A
-                _⊓_ : A → A → A
-
-                isFiniteHeightLattice : IsFiniteHeightLattice A height _≈_ _⊔_ _⊓_
-                ≈-dec : IsDecidable _≈_
-
-            open IsFiniteHeightLattice isFiniteHeightLattice public
-
-        finiteHeightAndDec : ∀ {k : ℕ} → FiniteHeightAndDecEq (IterProd k)
-        finiteHeightAndDec {0} = record
-            { height = h₂
-            ; _≈_ = _≈₂_
-            ; _⊔_ = _⊔₂_
-            ; _⊓_ = _⊓₂_
-            ; isFiniteHeightLattice = record
-                { isLattice = lB
-                ; fixedHeight = fhB
-                }
-            ; ≈-dec = ≈₂-dec
-            }
-        finiteHeightAndDec {suc k'} = record
-            { height = h₁ + FiniteHeightAndDecEq.height Right
-            ; _≈_ = P._≈_
-            ; _⊔_ = P._⊔_
-            ; _⊓_ = P._⊓_
-            ; isFiniteHeightLattice = isFiniteHeightLattice
-                ≈₁-dec (FiniteHeightAndDecEq.≈-dec Right)
-                h₁ (FiniteHeightAndDecEq.height Right)
-                fhA (IsFiniteHeightLattice.fixedHeight (FiniteHeightAndDecEq.isFiniteHeightLattice Right))
-            ; ≈-dec = ≈-dec ≈₁-dec (FiniteHeightAndDecEq.≈-dec Right)
-            }
-            where
-                Right = finiteHeightAndDec {k'}
-
-                open import Lattice.Prod
-                    _≈₁_ (FiniteHeightAndDecEq._≈_ Right)
-                    _⊔₁_ (FiniteHeightAndDecEq._⊔_ Right)
-                    _⊓₁_ (FiniteHeightAndDecEq._⊓_ Right)
-                    lA  (FiniteHeightAndDecEq.isLattice Right) as P
-
-    module _ (k : ℕ) where
-        open FiniteHeightAndDecEq (finiteHeightAndDec {k}) using (isFiniteHeightLattice) public
 
         private
-            FHD = finiteHeightAndDec {k}
+            required : RequiredForFixedHeight
+            required = record
+                { ≈₁-dec = ≈₁-dec
+                ; ≈₂-dec = ≈₂-dec
+                ; h₁ = h₁
+                ; h₂ = h₂
+                ; fhA = fhA
+                ; fhB = fhB
+                }
 
-        finiteHeightLattice : FiniteHeightLattice (IterProd k)
+        isFiniteHeightLattice = record
-        finiteHeightLattice = record
+            { isLattice = isLattice
-            { height = FiniteHeightAndDecEq.height FHD
+            ; fixedHeight = IsFiniteHeightAndDecEq.fixedHeight (Everything.isFiniteHeightIfSupported (everything k) required)
-            ; _≈_ = FiniteHeightAndDecEq._≈_ FHD
-            ; _⊔_ = FiniteHeightAndDecEq._⊔_ FHD
-            ; _⊓_ = FiniteHeightAndDecEq._⊓_ FHD
-            ; isFiniteHeightLattice = isFiniteHeightLattice
             }

Lattice/Prod.agda

@@ -171,18 +171,21 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
                                      , ≤-stepsˡ 1 (subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂))
                                      ))
 
+    fixedHeight : IsLattice.FixedHeight isLattice (h₁ + h₂)
+    fixedHeight =
+      ( ( ((amin , bmin) , (amax , bmax))
+        , concat
+            (ChainMapping₁.Chain-map (λ a → (a , bmin)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) (proj₂ (proj₁ fhA)))
+            (ChainMapping₂.Chain-map (λ b → (amax , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) (proj₂ (proj₁ fhB)))
+        )
+      , λ a₁b₁a₂b₂ → let ((n₁ , n₂) , ((a₁a₂ , b₁b₂) , n≤n₁+n₂)) = unzip a₁b₁a₂b₂
+                     in ≤-trans n≤n₁+n₂ (+-mono-≤ (proj₂ fhA a₁a₂) (proj₂ fhB b₁b₂))
+      )
+
     isFiniteHeightLattice : IsFiniteHeightLattice (A × B) (h₁ + h₂) _≈_ _⊔_ _⊓_
     isFiniteHeightLattice = record
         { isLattice = isLattice
-        ; fixedHeight =
+        ; fixedHeight = fixedHeight
-            ( ( ((amin , bmin) , (amax , bmax))
-              , concat
-                  (ChainMapping₁.Chain-map (λ a → (a , bmin)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) (proj₂ (proj₁ fhA)))
-                  (ChainMapping₂.Chain-map (λ b → (amax , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) (proj₂ (proj₁ fhB)))
-              )
-            , λ a₁b₁a₂b₂ → let ((n₁ , n₂) , ((a₁a₂ , b₁b₂) , n≤n₁+n₂)) = unzip a₁b₁a₂b₂
-                           in ≤-trans n≤n₁+n₂ (+-mono-≤ (proj₂ fhA a₁a₂) (proj₂ fhB b₁b₂))
-            )
         }
 
     finiteHeightLattice : FiniteHeightLattice (A × B)

Lattice/Unit.agda

@@ -107,10 +107,13 @@ private
     isLongest {tt} {tt} (step (tt⊔tt≈tt , tt̷≈tt) _ _) = ⊥-elim (tt̷≈tt refl)
     isLongest (done _) = z≤n
 
+fixedHeight : IsLattice.FixedHeight isLattice 0
+fixedHeight = (((tt , tt) , longestChain) , isLongest)
+
 isFiniteHeightLattice : IsFiniteHeightLattice ⊤ 0 _≈_ _⊔_ _⊓_
 isFiniteHeightLattice = record
     { isLattice = isLattice
-    ; fixedHeight = (((tt , tt) , longestChain) , isLongest)
+    ; fixedHeight = fixedHeight
     }
 
 finiteHeightLattice : FiniteHeightLattice ⊤