Move proof of least element into FiniteHeightLattice

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

Analysis/Forward.agda

@@ -21,7 +21,7 @@ open IsFiniteHeightLattice isFiniteHeightLatticeˡ
     using () renaming (isLattice to isLatticeˡ)
 
 module WithProg (prog : Program) where
-    open import Analysis.Forward.Lattices L prog hiding (≈ᵛ-Decidable) -- to disambiguate instance resolution
+    open import Analysis.Forward.Lattices L prog hiding (≈ᵛ-Decidable; ≈ᵐ-Decidable) -- to disambiguate instance resolution
     open import Analysis.Forward.Evaluation L prog
     open Program prog
 
@@ -66,7 +66,7 @@ module WithProg (prog : Program) where
                            (joinAll-Mono {sv₁} {sv₂} sv₁≼sv₂)
 
         -- The fixed point of the 'analyze' function is our final goal.
-        open import Fixedpoint ≈ᵐ-Decidable isFiniteHeightLatticeᵐ analyze (λ {m₁} {m₂} m₁≼m₂ → analyze-Mono {m₁} {m₂} m₁≼m₂)
+        open import Fixedpoint analyze (λ {m₁} {m₂} m₁≼m₂ → analyze-Mono {m₁} {m₂} m₁≼m₂)
             using ()
             renaming (aᶠ to result; aᶠ≈faᶠ to result≈analyze-result)
             public

Fixedpoint.agda

@@ -5,8 +5,8 @@ module Fixedpoint {a} {A : Set a}
                   {h : ℕ}
                   {_≈_ : A → A → Set a}
                   {_⊔_ : A → A → A} {_⊓_ : A → A → A}
-                  (≈-Decidable : IsDecidable _≈_)
-                  (flA : IsFiniteHeightLattice A h _≈_ _⊔_ _⊓_)
+                  {{ ≈-Decidable : IsDecidable _≈_ }}
+                  {{flA : IsFiniteHeightLattice A h _≈_ _⊔_ _⊓_}}
                   (f : A → A)
                   (Monotonicᶠ : Monotonic (IsFiniteHeightLattice._≼_ flA)
                                           (IsFiniteHeightLattice._≼_ flA) f) where
@@ -28,24 +28,9 @@ private
         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 boundedᴬ (ChainA.step x≺⊥ᴬ ≈-refl longestChainᴬ))
-                    where
-                        ⊥ᴬ⊓a̷≈⊥ᴬ : ¬ (⊥ᴬ ⊓ a) ≈ ⊥ᴬ
-                        ⊥ᴬ⊓a̷≈⊥ᴬ = λ ⊥ᴬ⊓a≈⊥ᴬ → ⊥ᴬ̷≈a⊓⊥ᴬ (≈-trans (≈-sym ⊥ᴬ⊓a≈⊥ᴬ) (⊓-comm _ _))
-
-                        x≺⊥ᴬ : (⊥ᴬ ⊓ a) ≺ ⊥ᴬ
-                        x≺⊥ᴬ = (≈-trans (⊔-comm _ _) (≈-trans (≈-refl {⊥ᴬ ⊔ (⊥ᴬ ⊓ a)}) (absorb-⊔-⊓ ⊥ᴬ a)) , ⊥ᴬ⊓a̷≈⊥ᴬ)
-
     -- using 'g', for gas, here helps make sure the function terminates.
     -- since A forms a fixed-height lattice, we must find a solution after
     -- 'h' steps at most. Gas is set up such that as soon as it runs
@@ -65,7 +50,7 @@ private
                     c' rewrite +-comm 1 hᶜ = ChainA.concat c (ChainA.step a₂≺fa₂ ≈-refl (ChainA.done (≈-refl {f a₂})))
 
     fix : Σ A (λ a → a ≈ f a)
-    fix = doStep (suc h) 0 ⊥ᴬ ⊥ᴬ (ChainA.done ≈-refl) (+-comm (suc h) 0) (⊥ᴬ≼ (f ⊥ᴬ))
+    fix = doStep (suc h) 0 ⊥ᴬ ⊥ᴬ (ChainA.done ≈-refl) (+-comm (suc h) 0) (⊥≼ (f ⊥ᴬ))
 
 aᶠ : A
 aᶠ = proj₁ fix
@@ -85,4 +70,4 @@ private
     ...   | no  _ = stepPreservesLess g' _ _ _ b b≈fb (≼-cong ≈-refl (≈-sym b≈fb) (Monotonicᶠ a₂≼b)) _ _ _
 
 aᶠ≼ : ∀ (a : A) → a ≈ f a → aᶠ ≼ a
-aᶠ≼ a a≈fa = stepPreservesLess (suc h) 0 ⊥ᴬ ⊥ᴬ a a≈fa (⊥ᴬ≼ a) (ChainA.done ≈-refl) (+-comm (suc h) 0) (⊥ᴬ≼ (f ⊥ᴬ))
+aᶠ≼ a a≈fa = stepPreservesLess (suc h) 0 ⊥ᴬ ⊥ᴬ a a≈fa (⊥≼ a) (ChainA.done ≈-refl) (+-comm (suc h) 0) (⊥≼ (f ⊥ᴬ))

Isomorphism.agda

@@ -68,6 +68,7 @@ module TransportFiniteHeight
         renaming (⊥ to ⊥₁; ⊤ to ⊤₁; bounded to bounded₁; longestChain to c)
 
     instance
+        fixedHeight : IsLattice.FixedHeight lB height
         fixedHeight = record
             { ⊥ = f ⊥₁
             ; ⊤ = f ⊤₁

Lattice.agda

@@ -4,7 +4,8 @@ open import Equivalence
 import Chain
 
 open import Relation.Binary.Core using (_Preserves_⟶_ )
-open import Relation.Nullary using (Dec; ¬_)
+open import Relation.Nullary using (Dec; ¬_; yes; no)
+open import Data.Empty using (⊥-elim)
 open import Data.Nat as Nat using (ℕ)
 open import Data.Product using (_×_; Σ; _,_)
 open import Data.Sum using (_⊎_; inj₁; inj₂)
@@ -236,6 +237,28 @@ record IsFiniteHeightLattice {a} (A : Set a)
     field
         {{fixedHeight}} : FixedHeight h
 
+    -- If the equality is decidable, we can prove that the top and bottom
+    -- elements of the chain are least and greatest elements of the lattice
+    module _ {{≈-Decidable : IsDecidable _≈_}} where
+        open IsDecidable ≈-Decidable using () renaming (R-dec to ≈-dec)
+
+        module MyChain = Chain _≈_ ≈-equiv _≺_ ≺-cong
+        open MyChain.Height fixedHeight using (⊥; ⊤) public
+        open MyChain.Height fixedHeight using (bounded; longestChain)
+
+        ⊥≼ : ∀ (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 (MyChain.Bounded-suc-n bounded (MyChain.step x≺⊥ ≈-refl longestChain))
+                        where
+                            ⊥⊓a̷≈⊥ : ¬ (⊥ ⊓ a) ≈ ⊥
+                            ⊥⊓a̷≈⊥ = λ ⊥⊓a≈⊥ → ⊥ᴬ̷≈a⊓⊥ (≈-trans (≈-sym ⊥⊓a≈⊥) (⊓-comm _ _))
+
+                            x≺⊥ : (⊥ ⊓ a) ≺ ⊥
+                            x≺⊥ = (≈-trans (⊔-comm _ _) (≈-trans (≈-refl {⊥ ⊔ (⊥ ⊓ a)}) (absorb-⊔-⊓ ⊥ a)) , ⊥⊓a̷≈⊥)
+
 module ChainMapping {a b} {A : Set a} {B : Set b}
     {_≈₁_ : A → A → Set a} {_≈₂_ : B → B → Set b}
     {_⊔₁_ : A → A → A} {_⊔₂_ : B → B → B}

Lattice/ExtendBelow.agda

@@ -0,0 +1,169 @@
+open import Lattice
+
+module Lattice.ExtendBelow {a} (A : Set a)
+    {_≈₁_ : A → A → Set a} {_⊔₁_ : A → A → A} {_⊓₁_ : A → A → A}
+    {{lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_}} where
+
+open import Equivalence
+open import Showable using (Showable; show)
+open import Relation.Binary.Definitions using (Decidable)
+open import Relation.Binary.PropositionalEquality using (refl)
+open import Relation.Nullary using (Dec; ¬_; yes; no)
+
+open IsLattice lA using ()
+    renaming ( ≈-equiv to ≈₁-equiv
+             ; ≈-⊔-cong to ≈₁-⊔₁-cong
+             ; ⊔-assoc to ⊔₁-assoc; ⊔-comm to ⊔₁-comm; ⊔-idemp to ⊔₁-idemp
+             ; ≈-⊓-cong to ≈₁-⊓₁-cong
+             ; ⊓-assoc to ⊓₁-assoc; ⊓-comm to ⊓₁-comm; ⊓-idemp to ⊓₁-idemp
+             ; absorb-⊔-⊓ to absorb-⊔₁-⊓₁; absorb-⊓-⊔ to absorb-⊓₁-⊔₁
+             )
+
+open IsEquivalence ≈₁-equiv using ()
+    renaming (≈-refl to ≈₁-refl; ≈-sym to ≈₁-sym; ≈-trans to ≈₁-trans)
+
+data ExtendBelow : Set a where
+    [_] : A → ExtendBelow
+    ⊥ : ExtendBelow
+
+instance
+    showable : {{ showableA : Showable A }} → Showable ExtendBelow
+    showable = record
+        { show = (λ
+            { ⊥ → "⊥"
+            ; [ a ] → show a
+            })
+        }
+
+data _≈_ : ExtendBelow → ExtendBelow → Set a where
+    ≈-⊥-⊥ : ⊥ ≈ ⊥
+    ≈-lift : ∀ {x y : A} → x ≈₁ y → [ x ] ≈ [ y ]
+
+≈-refl : ∀ {ab : ExtendBelow} → ab ≈ ab
+≈-refl {⊥} = ≈-⊥-⊥
+≈-refl {[ x ]} = ≈-lift ≈₁-refl
+
+≈-sym : ∀ {ab₁ ab₂ : ExtendBelow} → ab₁ ≈ ab₂ → ab₂ ≈ ab₁
+≈-sym ≈-⊥-⊥ = ≈-⊥-⊥
+≈-sym (≈-lift x≈₁y) = ≈-lift (≈₁-sym x≈₁y)
+
+≈-trans : ∀ {ab₁ ab₂ ab₃ : ExtendBelow} → ab₁ ≈ ab₂ → ab₂ ≈ ab₃ → ab₁ ≈ ab₃
+≈-trans ≈-⊥-⊥ ≈-⊥-⊥ = ≈-⊥-⊥
+≈-trans (≈-lift a₁≈a₂) (≈-lift a₂≈a₃) = ≈-lift (≈₁-trans a₁≈a₂ a₂≈a₃)
+
+instance
+    ≈-equiv : IsEquivalence ExtendBelow _≈_
+    ≈-equiv = record
+        { ≈-refl = ≈-refl
+        ; ≈-sym = ≈-sym
+        ; ≈-trans = ≈-trans
+        }
+
+_⊔_ : ExtendBelow → ExtendBelow → ExtendBelow
+_⊔_ ⊥ x = x
+_⊔_ [ a₁ ] ⊥ = [ a₁ ]
+_⊔_ [ a₁ ] [ a₂ ] = [ a₁ ⊔₁ a₂ ]
+
+_⊓_ : ExtendBelow → ExtendBelow → ExtendBelow
+_⊓_ ⊥ x = ⊥
+_⊓_ [ _ ] ⊥ = ⊥
+_⊓_ [ a₁ ] [ a₂ ] = [ a₁ ⊓₁ a₂ ]
+
+≈-⊔-cong : ∀ {x₁ x₂ x₃ x₄} → x₁ ≈ x₂ → x₃ ≈ x₄ →
+           (x₁ ⊔ x₃) ≈ (x₂ ⊔ x₄)
+≈-⊔-cong .{⊥} .{⊥} {x₃} {x₄} ≈-⊥-⊥ [a₃]≈[a₄] = [a₃]≈[a₄]
+≈-⊔-cong {x₁ = [ a₁ ]} {x₂ = [ a₂ ]} .{⊥} .{⊥} [a₁]≈[a₂] ≈-⊥-⊥ = [a₁]≈[a₂]
+≈-⊔-cong {x₁ = [ a₁ ]} {x₂ = [ a₂ ]} {x₃ = [ a₃ ]} {x₄ = [ a₄ ]} (≈-lift a₁≈a₂) (≈-lift a₃≈a₄) = ≈-lift (≈₁-⊔₁-cong a₁≈a₂ a₃≈a₄)
+
+⊔-assoc : ∀ (x₁ x₂ x₃ : ExtendBelow) →  ((x₁ ⊔ x₂) ⊔ x₃) ≈ (x₁ ⊔ (x₂ ⊔ x₃))
+⊔-assoc ⊥ x₁ x₂ = ≈-refl
+⊔-assoc [ a₁ ] ⊥ x₂ = ≈-refl
+⊔-assoc [ a₁ ] [ a₂ ] ⊥ = ≈-refl
+⊔-assoc [ a₁ ] [ a₂ ] [ a₃ ] = ≈-lift (⊔₁-assoc a₁ a₂ a₃)
+
+⊔-comm : ∀ (x₁ x₂ : ExtendBelow) →  (x₁ ⊔ x₂) ≈ (x₂ ⊔ x₁)
+⊔-comm ⊥ ⊥ = ≈-refl
+⊔-comm ⊥ [ a₂ ] = ≈-refl
+⊔-comm [ a₁ ] ⊥ = ≈-refl
+⊔-comm [ a₁ ] [ a₂ ] = ≈-lift (⊔₁-comm a₁ a₂)
+
+⊔-idemp : ∀ (x : ExtendBelow) →  (x ⊔ x) ≈ x
+⊔-idemp ⊥ = ≈-refl
+⊔-idemp [ a ] = ≈-lift (⊔₁-idemp a)
+
+≈-⊓-cong : ∀ {x₁ x₂ x₃ x₄} → x₁ ≈ x₂ → x₃ ≈ x₄ →
+           (x₁ ⊓ x₃) ≈ (x₂ ⊓ x₄)
+≈-⊓-cong .{⊥} .{⊥} {x₃} {x₄} ≈-⊥-⊥ [a₃]≈[a₄] = ≈-⊥-⊥
+≈-⊓-cong {x₁ = [ a₁ ]} {x₂ = [ a₂ ]} .{⊥} .{⊥} [a₁]≈[a₂] ≈-⊥-⊥ = ≈-⊥-⊥
+≈-⊓-cong {x₁ = [ a₁ ]} {x₂ = [ a₂ ]} {x₃ = [ a₃ ]} {x₄ = [ a₄ ]} (≈-lift a₁≈a₂) (≈-lift a₃≈a₄) = ≈-lift (≈₁-⊓₁-cong a₁≈a₂ a₃≈a₄)
+
+⊓-assoc : ∀ (x₁ x₂ x₃ : ExtendBelow) →  ((x₁ ⊓ x₂) ⊓ x₃) ≈ (x₁ ⊓ (x₂ ⊓ x₃))
+⊓-assoc ⊥ x₁ x₂ = ≈-refl
+⊓-assoc [ a₁ ] ⊥ x₂ = ≈-refl
+⊓-assoc [ a₁ ] [ a₂ ] ⊥ = ≈-refl
+⊓-assoc [ a₁ ] [ a₂ ] [ a₃ ] = ≈-lift (⊓₁-assoc a₁ a₂ a₃)
+
+⊓-comm : ∀ (x₁ x₂ : ExtendBelow) →  (x₁ ⊓ x₂) ≈ (x₂ ⊓ x₁)
+⊓-comm ⊥ ⊥ = ≈-refl
+⊓-comm ⊥ [ a₂ ] = ≈-refl
+⊓-comm [ a₁ ] ⊥ = ≈-refl
+⊓-comm [ a₁ ] [ a₂ ] = ≈-lift (⊓₁-comm a₁ a₂)
+
+⊓-idemp : ∀ (x : ExtendBelow) →  (x ⊓ x) ≈ x
+⊓-idemp ⊥ = ≈-refl
+⊓-idemp [ a ] = ≈-lift (⊓₁-idemp a)
+
+absorb-⊔-⊓ : (x₁ x₂ : ExtendBelow) → (x₁ ⊔ (x₁ ⊓ x₂)) ≈ x₁
+absorb-⊔-⊓ ⊥ ⊥ = ≈-refl
+absorb-⊔-⊓ ⊥ [ a₂ ] = ≈-refl
+absorb-⊔-⊓ [ a₁ ] ⊥ = ≈-refl
+absorb-⊔-⊓ [ a₁ ] [ a₂ ] = ≈-lift (absorb-⊔₁-⊓₁ a₁ a₂)
+
+absorb-⊓-⊔ : (x₁ x₂ : ExtendBelow) → (x₁ ⊓ (x₁ ⊔ x₂)) ≈ x₁
+absorb-⊓-⊔ ⊥ ⊥ = ≈-refl
+absorb-⊓-⊔ ⊥ [ a₂ ] = ≈-refl
+absorb-⊓-⊔ [ a₁ ] ⊥ = ⊓-idemp [ a₁ ]
+absorb-⊓-⊔ [ a₁ ] [ a₂ ] = ≈-lift (absorb-⊓₁-⊔₁ a₁ a₂)
+
+instance
+    isJoinSemilattice : IsSemilattice ExtendBelow _≈_ _⊔_
+    isJoinSemilattice = record
+        { ≈-equiv = ≈-equiv
+        ; ≈-⊔-cong = ≈-⊔-cong
+        ; ⊔-assoc = ⊔-assoc
+        ; ⊔-comm = ⊔-comm
+        ; ⊔-idemp = ⊔-idemp
+        }
+
+    isMeetSemilattice : IsSemilattice ExtendBelow _≈_ _⊓_
+    isMeetSemilattice = record
+        { ≈-equiv = ≈-equiv
+        ; ≈-⊔-cong = ≈-⊓-cong
+        ; ⊔-assoc = ⊓-assoc
+        ; ⊔-comm = ⊓-comm
+        ; ⊔-idemp = ⊓-idemp
+        }
+
+    isLattice : IsLattice ExtendBelow _≈_ _⊔_ _⊓_
+    isLattice = record
+        { joinSemilattice = isJoinSemilattice
+        ; meetSemilattice = isMeetSemilattice
+        ; absorb-⊔-⊓ = absorb-⊔-⊓
+        ; absorb-⊓-⊔ = absorb-⊓-⊔
+        }
+
+module _ {{≈₁-Decidable : IsDecidable _≈₁_}} where
+    open IsDecidable ≈₁-Decidable using () renaming (R-dec to ≈₁-dec)
+
+    ≈-dec : Decidable _≈_
+    ≈-dec ⊥ ⊥ = yes ≈-⊥-⊥
+    ≈-dec [ a₁ ] [ a₂ ]
+        with ≈₁-dec a₁ a₂
+    ...   | yes a₁≈a₂ = yes (≈-lift a₁≈a₂)
+    ...   | no a₁̷≈a₂ = no (λ { (≈-lift a₁≈a₂) → a₁̷≈a₂ a₁≈a₂ })
+    ≈-dec ⊥ [ _ ] = no (λ ())
+    ≈-dec [ _ ] ⊥ = no (λ ())
+
+    instance
+        ≈-Decidable : IsDecidable _≈_
+        ≈-Decidable = record { R-dec = ≈-dec }