Isomorphism.agda

@@ -60,12 +60,3 @@ module TransportFiniteHeight
             { isLattice = lB
             ; fixedHeight = (((f a₁ , f a₂), portChain₁ c) , λ c' → bounded₁ (portChain₂ c'))
             }
-
-    finiteHeightLattice : FiniteHeightLattice B
-    finiteHeightLattice = record
-        { height = height
-        ; _≈_ = _≈₂_
-        ; _⊔_ = _⊔₂_
-        ; _⊓_ = _⊓₂_
-        ; isFiniteHeightLattice = isFiniteHeightLattice
-        }

Lattice.agda

@@ -14,12 +14,6 @@ open import Function.Definitions using (Injective)
 IsDecidable : ∀ {a} {A : Set a} (R : A → A → Set a) → Set a
 IsDecidable {a} {A} R = ∀ (a₁ a₂ : A) → Dec (R a₁ a₂)
 
-module _ {a b} {A : Set a} {B : Set b}
-    (_≼₁_ : A → A → Set a) (_≼₂_ : B → B → Set b) where
-
-    Monotonic : (A → B) → Set (a ⊔ℓ b)
-    Monotonic f = ∀ {a₁ a₂ : A} → a₁ ≼₁ a₂ → f a₁ ≼₂ f a₂
-
 record IsSemilattice {a} (A : Set a)
     (_≈_ : A → A → Set a)
     (_⊔_ : A → A → A) : Set a where
@@ -42,26 +36,6 @@ record IsSemilattice {a} (A : Set a)
 
     open import Relation.Binary.Reasoning.Base.Single _≈_ ≈-refl ≈-trans
 
-    ⊔-Monotonicˡ : ∀ (a₁ : A) → Monotonic _≼_ _≼_ (λ a₂ → a₁ ⊔ a₂)
-    ⊔-Monotonicˡ a {a₁} {a₂} a₁≼a₂ = ≈-trans (≈-sym lhs) (≈-⊔-cong (≈-refl {a}) a₁≼a₂)
-        where
-            lhs =
-                begin
-                    a ⊔ (a₁ ⊔ a₂)
-                ∼⟨ ≈-⊔-cong (≈-sym (⊔-idemp _)) ≈-refl ⟩
-                    (a ⊔ a) ⊔ (a₁ ⊔ a₂)
-                ∼⟨ ⊔-assoc _ _ _ ⟩
-                    a ⊔ (a ⊔ (a₁ ⊔ a₂))
-                ∼⟨ ≈-⊔-cong ≈-refl (≈-sym (⊔-assoc _ _ _)) ⟩
-                    a ⊔ ((a ⊔ a₁) ⊔ a₂)
-                ∼⟨ ≈-⊔-cong ≈-refl (≈-⊔-cong (⊔-comm _ _) ≈-refl) ⟩
-                    a ⊔ ((a₁ ⊔ a) ⊔ a₂)
-                ∼⟨ ≈-⊔-cong ≈-refl (⊔-assoc _ _ _) ⟩
-                    a ⊔ (a₁ ⊔ (a ⊔ a₂))
-                ∼⟨ ≈-sym (⊔-assoc _ _ _) ⟩
-                    (a ⊔ a₁) ⊔ (a ⊔ a₂)
-                ∎
-
     ≼-refl : ∀ (a : A) → a ≼ a
     ≼-refl a = ⊔-idemp a
 
@@ -123,6 +97,12 @@ record IsFiniteHeightLattice {a} (A : Set a)
     field
         fixedHeight : FixedHeight h
 
+module _ {a b} {A : Set a} {B : Set b}
+    (_≼₁_ : A → A → Set a) (_≼₂_ : B → B → Set b) where
+
+    Monotonic : (A → B) → Set (a ⊔ℓ b)
+    Monotonic f = ∀ {a₁ a₂ : A} → a₁ ≼₁ a₂ → f a₁ ≼₂ f 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/Bundles/FiniteValueMap.agda

@@ -1,26 +0,0 @@
-open import Relation.Binary.PropositionalEquality using (_≡_)
-open import Relation.Binary.Definitions using (Decidable)
-
-module Lattice.Bundles.FiniteValueMap (A B : Set) (≡-dec-A : Decidable (_≡_ {_} {A})) where
-
-open import Lattice
-open import Data.List using (List)
-open import Data.Nat using (ℕ)
-open import Utils using (Unique)
-
-module _ (fhB : FiniteHeightLattice B) where
-    open Lattice.FiniteHeightLattice fhB using () renaming
-        ( _≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_
-        ; height to height₂
-        ; isLattice to isLattice₂
-        ; fixedHeight to fixedHeight₂
-        )
-
-    module _ {ks : List A} (uks : Unique ks) (≈₂-dec : Decidable _≈₂_) where
-        import Lattice.FiniteValueMap A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A isLattice₂ as FVM
-
-        FiniteHeightType = FVM.FiniteMap
-
-        ≈-dec = FVM.≈-dec ks ≈₂-dec
-
-        finiteHeightLattice = FVM.IterProdIsomorphism.finiteHeightLattice uks ≈₂-dec height₂ fixedHeight₂

Lattice/Bundles/IterProd.agda

@@ -1,38 +0,0 @@
-open import Lattice
-
-module Lattice.Bundles.IterProd {a} (A B : Set a) where
-open import Data.Nat using (ℕ)
-
-module _ (lA : Lattice A) (lB : Lattice B) where
-    open Lattice.Lattice lA using () renaming
-        ( _≈_ to _≈₁_; _⊔_ to _⊔₁_; _⊓_ to _⊓₁_
-        ; isLattice to isLattice₁
-        )
-
-    open Lattice.Lattice lB using () renaming
-        ( _≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_
-        ; isLattice to isLattice₂
-        )
-
-    module _ (k : ℕ) where
-        open import Lattice.IterProd _≈₁_ _≈₂_ _⊔₁_ _⊔₂_ _⊓₁_ _⊓₂_ isLattice₁ isLattice₂ using (lattice) public
-
-module _ (fhA : FiniteHeightLattice A) (fhB : FiniteHeightLattice B) where
-    open Lattice.FiniteHeightLattice fhA using () renaming
-        ( _≈_ to _≈₁_; _⊔_ to _⊔₁_; _⊓_ to _⊓₁_
-        ; height to height₁
-        ; isLattice to isLattice₁
-        ; fixedHeight to fixedHeight₁
-        )
-
-    open Lattice.FiniteHeightLattice fhB using () renaming
-        ( _≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_
-        ; height to height₂
-        ; isLattice to isLattice₂
-        ; fixedHeight to fixedHeight₂
-        )
-
-    module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) (k : ℕ) where
-        import Lattice.IterProd _≈₁_ _≈₂_ _⊔₁_ _⊔₂_ _⊓₁_ _⊓₂_ isLattice₁ isLattice₂ as IP
-
-        finiteHeightLattice = IP.finiteHeightLattice k ≈₁-dec ≈₂-dec height₁ height₂ fixedHeight₁ fixedHeight₂

Lattice/FiniteMap.agda

@@ -27,7 +27,6 @@ open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB as Map
         ; ⊓-idemp to ⊓ᵐ-idemp
         ; absorb-⊔-⊓ to absorb-⊔ᵐ-⊓ᵐ
         ; absorb-⊓-⊔ to absorb-⊓ᵐ-⊔ᵐ
-        ; ≈-dec to ≈ᵐ-dec
         )
 open import Data.Product using (_×_; _,_; Σ; proj₁ ; proj₂)
 open import Equivalence
@@ -39,9 +38,6 @@ module _ (ks : List A) where
     _≈_ : FiniteMap → FiniteMap → Set (a ⊔ℓ b)
     _≈_ (m₁ , _) (m₂ , _) = m₁ ≈ᵐ m₂
 
-    ≈-dec : IsDecidable _≈₂_ → IsDecidable _≈_
-    ≈-dec ≈₂-dec fm₁ fm₂ = ≈ᵐ-dec ≈₂-dec (proj₁ fm₁) (proj₁ fm₂)
-
     _⊔_ : FiniteMap → FiniteMap → FiniteMap
     _⊔_ (m₁ , km₁≡ks) (m₂ , km₂≡ks) = (m₁ ⊔ᵐ m₂ , trans (sym (⊔-equal-keys {m₁} {m₂} (trans (km₁≡ks) (sym km₂≡ks)))) km₁≡ks)
 

Lattice/FiniteValueMap.agda

@@ -271,4 +271,4 @@ module IterProdIsomorphism where
             (to-preserves-≈ uks) (from-preserves-≈ {ks})
             (to-⊔-distr uks) (from-⊔-distr {ks})
             (from-to-inverseʳ uks) (from-to-inverseˡ uks)
-            using (isFiniteHeightLattice; finiteHeightLattice) public
+            using (isFiniteHeightLattice) public

Lattice/Map.agda

@@ -582,7 +582,7 @@ Expr-Provenance k (e₁ ∩ e₂) k∈ke₁e₂
 ...   | no k∉ke₁ | yes k∈ke₂ = ⊥-elim (intersect-preserves-∉₁ {l₂ = proj₁ ⟦ e₂ ⟧} k∉ke₁ k∈ke₁e₂)
 ...   | no k∉ke₁ | no k∉ke₂ = ⊥-elim (intersect-preserves-∉₂ {l₁ = proj₁ ⟦ e₁ ⟧} k∉ke₂ k∈ke₁e₂)
 
-module _ (≈₂-dec : IsDecidable _≈₂_) where
+module _ (≈₂-dec : ∀ (b₁ b₂ : B) → Dec (b₁ ≈₂ b₂)) where
     private module _ where
         data SubsetInfo (m₁ m₂ : Map) : Set (a ⊔ℓ b) where
             extra : (k : A) → k ∈k m₁ → ¬ k ∈k m₂ → SubsetInfo m₁ m₂

Main.agda

@@ -1,69 +0,0 @@
-module Main where
-
-open import IO
-open import Level using (0ℓ)
-open import Data.Nat.Show using (show)
-open import Data.List using (List; _∷_; []; foldr)
-open import Data.String using (String; _++_) renaming (_≟_ to _≟ˢ_)
-open import Data.Unit using (⊤; tt) renaming (_≟_ to _≟ᵘ_)
-open import Data.Product using (_,_; _×_; proj₁; proj₂)
-open import Data.List.Relation.Unary.All using (_∷_; [])
-open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; subst; refl; trans)
-open import Relation.Nullary using (¬_)
-
-open import Utils using (Unique; push; empty)
-
-xyzw : List String
-xyzw = "x" ∷ "y" ∷ "z" ∷ "w" ∷ []
-
-xyzw-Unique : Unique xyzw
-xyzw-Unique = push ((λ ()) ∷ (λ ()) ∷ (λ ()) ∷ []) (push ((λ ()) ∷ (λ ()) ∷ []) (push ((λ ()) ∷ []) (push [] empty)))
-
-open import Lattice using (IsFiniteHeightLattice; FiniteHeightLattice; Monotonic)
-open import Lattice.AboveBelow ⊤ _≡_ (record { ≈-refl = refl; ≈-sym = sym; ≈-trans = trans }) _≟ᵘ_  as AB using () renaming (≈-dec to ≈ᵘ-dec)
-open AB.Plain using () renaming (finiteHeightLattice to finiteHeightLatticeᵘ)
-open import Lattice.Bundles.FiniteValueMap String AB.AboveBelow _≟ˢ_ renaming (finiteHeightLattice to finiteHeightLatticeᵐ; FiniteHeightType to FiniteHeightTypeᵐ; ≈-dec to ≈-dec)
-
-fhlᵘ = finiteHeightLatticeᵘ (Data.Unit.tt)
-
-FiniteHeightMap = FiniteHeightTypeᵐ fhlᵘ xyzw-Unique ≈ᵘ-dec
-
-showAboveBelow : AB.AboveBelow → String
-showAboveBelow AB.⊤ = "⊤"
-showAboveBelow AB.⊥ = "⊥"
-showAboveBelow (AB.[_] tt) = "()"
-
-showMap : ∀ {ks : List String} → FiniteHeightMap ks → String
-showMap ((kvs , _) , _) = "{" ++ foldr (λ (x , y) rest → x ++ " ↦ " ++ showAboveBelow y ++ ", " ++ rest) "" kvs ++ "}"
-
-fhlⁱᵖ = finiteHeightLatticeᵐ fhlᵘ xyzw-Unique ≈ᵘ-dec
-
-open FiniteHeightLattice fhlⁱᵖ using (_≈_; _⊔_; _⊓_; ⊔-idemp; _≼_; ≈-⊔-cong; ≈-refl; ≈-trans; ≈-sym; ⊔-assoc; ⊔-comm; ⊔-Monotonicˡ)
-open import Relation.Binary.Reasoning.Base.Single _≈_ (λ {m} → ≈-refl {m}) (λ {m₁} {m₂} {m₃} → ≈-trans {m₁} {m₂} {m₃}) -- why am I having to eta-expand here?
-
-smallestMap = proj₁ (proj₁ (proj₁ (FiniteHeightLattice.fixedHeight fhlⁱᵖ)))
-largestMap = proj₂ (proj₁ (proj₁ (FiniteHeightLattice.fixedHeight fhlⁱᵖ)))
-
-dumb : FiniteHeightMap xyzw
-dumb = ((("x" , AB.[_] tt) ∷ ("y" , AB.⊥) ∷ ("z" , AB.⊥) ∷ ("w" , AB.⊥) ∷ [] , xyzw-Unique) , refl)
-
-dumbFunction : FiniteHeightMap xyzw → FiniteHeightMap xyzw
-dumbFunction = _⊔_ dumb
-
-dumbFunction-Monotonic : Monotonic _≼_ _≼_ dumbFunction
-dumbFunction-Monotonic {m₁} {m₂} m₁≼m₂ = ⊔-Monotonicˡ dumb {m₁} {m₂} m₁≼m₂
-
-
-open import Fixedpoint {0ℓ} {FiniteHeightMap xyzw} {8} {_≈_} {_⊔_} {_⊓_} (≈-dec fhlᵘ xyzw-Unique ≈ᵘ-dec) (FiniteHeightLattice.isFiniteHeightLattice fhlⁱᵖ) dumbFunction (λ {m₁} {m₂} m₁≼m₂ → dumbFunction-Monotonic {m₁} {m₂} m₁≼m₂)
-
--- module Fixedpoint {a} {A : Set a}
---                   {h : ℕ}
---                   {_≈_ : A → A → Set a}
---                   {_⊔_ : A → A → A} {_⊓_ : A → A → A}
---                   (≈-dec : IsDecidable _≈_)
---                   (flA : IsFiniteHeightLattice A h _≈_ _⊔_ _⊓_)
---                   (f : A → A)
---                   (Monotonicᶠ : Monotonic (IsFiniteHeightLattice._≼_ flA)
---                                           (IsFiniteHeightLattice._≼_ flA) f) where
-
-main = run {0ℓ} (putStrLn (showMap aᶠ))