From 85154913275c63a40ee8598827d7a8e3a6acccde Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 10 Mar 2024 18:43:10 -0700 Subject: [PATCH] Simplify AboveBelow a bit to avoid nested modules Signed-off-by: Danila Fedorin --- Analysis/Sign.agda | 14 ++++----- Lattice/AboveBelow.agda | 64 +++++++++++++++++++++-------------------- Main.agda | 4 +-- 3 files changed, 39 insertions(+), 43 deletions(-) diff --git a/Analysis/Sign.agda b/Analysis/Sign.agda index 9781bd8..4767dfd 100644 --- a/Analysis/Sign.agda +++ b/Analysis/Sign.agda @@ -42,22 +42,18 @@ open import Lattice.AboveBelow Sign _≡_ (record { ≈-refl = refl; ≈-sym = s ; ⊥ to ⊥ᵍ ; ⊤ to ⊤ᵍ ; [_] to [_]ᵍ + ; _≈_ to _≈ᵍ_ ; ≈-⊥-⊥ to ≈ᵍ-⊥ᵍ-⊥ᵍ ; ≈-⊤-⊤ to ≈ᵍ-⊤ᵍ-⊤ᵍ ; ≈-lift to ≈ᵍ-lift + ; ≈-refl to ≈ᵍ-refl ) -- 'sign' has no underlying lattice structure, so use the 'plain' above-below lattice. -open AB.Plain using () renaming (finiteHeightLattice to finiteHeightLatticeᵍ-if-inhabited) - -finiteHeightLatticeᵍ = finiteHeightLatticeᵍ-if-inhabited 0ˢ - -open FiniteHeightLattice finiteHeightLatticeᵍ - using () +open AB.Plain 0ˢ using () renaming - ( _≼_ to _≼ᵍ_ - ; _≈_ to _≈ᵍ_ + ( finiteHeightLattice to finiteHeightLatticeᵍ + ; _≼_ to _≼ᵍ_ ; _⊔_ to _⊔ᵍ_ - ; ≈-refl to ≈ᵍ-refl ) plus : SignLattice → SignLattice → SignLattice diff --git a/Lattice/AboveBelow.agda b/Lattice/AboveBelow.agda index b1ad4ca..71c1349 100644 --- a/Lattice/AboveBelow.agda +++ b/Lattice/AboveBelow.agda @@ -68,7 +68,10 @@ data _≈_ : AboveBelow → AboveBelow → Set a where -- Any object can be wrapped in an 'above below' to make it a lattice, -- since ⊤ and ⊥ are the largest and least elements, and the rest are left -- unordered. That's what this module does. -module Plain where +-- +-- For convenience, ask for the underlying type to always be inhabited, to +-- avoid requiring additional constraints in some of the proofs below. +module Plain (x : A) where _⊔_ : AboveBelow → AboveBelow → AboveBelow ⊥ ⊔ x = x ⊤ ⊔ x = ⊤ @@ -296,7 +299,7 @@ module Plain where ; isLattice = isLattice } - open IsLattice isLattice using (_≼_; _≺_) + open IsLattice isLattice using (_≼_; _≺_) public ⊥≺[x] : ∀ (x : A) → ⊥ ≺ [ x ] ⊥≺[x] x = (≈-refl , λ ()) @@ -322,36 +325,35 @@ module Plain where open Chain _≈_ ≈-equiv (IsLattice._≺_ isLattice) (IsLattice.≺-cong isLattice) - module _ (x : A) where - longestChain : Chain ⊥ ⊤ 2 - longestChain = step (⊥≺[x] x) ≈-refl (step ([x]≺⊤ x) ≈-⊤-⊤ (done ≈-⊤-⊤)) + longestChain : Chain ⊥ ⊤ 2 + longestChain = step (⊥≺[x] x) ≈-refl (step ([x]≺⊤ x) ≈-⊤-⊤ (done ≈-⊤-⊤)) - ¬-Chain-⊤ : ∀ {ab : AboveBelow} {n : ℕ} → ¬ Chain ⊤ ab (suc n) - ¬-Chain-⊤ {x} (step (⊤⊔x≈x , ⊤̷≈x) _ _) rewrite ⊤⊔x≡⊤ x = ⊥-elim (⊤̷≈x ⊤⊔x≈x) + ¬-Chain-⊤ : ∀ {ab : AboveBelow} {n : ℕ} → ¬ Chain ⊤ ab (suc n) + ¬-Chain-⊤ {x} (step (⊤⊔x≈x , ⊤̷≈x) _ _) rewrite ⊤⊔x≡⊤ x = ⊥-elim (⊤̷≈x ⊤⊔x≈x) - isLongest : ∀ {ab₁ ab₂ : AboveBelow} {n : ℕ} → Chain ab₁ ab₂ n → n ≤ 2 - isLongest (done _) = z≤n - isLongest (step _ _ (done _)) = s≤s z≤n - isLongest (step _ _ (step _ _ (done _))) = s≤s (s≤s z≤n) - isLongest {⊤} c@(step _ _ _) = ⊥-elim (¬-Chain-⊤ c) - isLongest {[ x ]} (step {_} {y} [x]≺y y≈y' c@(step _ _ _)) - rewrite [x]≺y⇒y≡⊤ x y [x]≺y with ≈-⊤-⊤ ← y≈y' = ⊥-elim (¬-Chain-⊤ c) - isLongest {⊥} (step {_} {⊥} (_ , ⊥̷≈⊥) _ _) = ⊥-elim (⊥̷≈⊥ ≈-⊥-⊥) - isLongest {⊥} (step {_} {⊤} _ ≈-⊤-⊤ c@(step _ _ _)) = ⊥-elim (¬-Chain-⊤ c) - isLongest {⊥} (step {_} {[ x ]} _ (≈-lift _) (step [x]≺y y≈z c@(step _ _ _))) - rewrite [x]≺y⇒y≡⊤ _ _ [x]≺y with ≈-⊤-⊤ ← y≈z = ⊥-elim (¬-Chain-⊤ c) + isLongest : ∀ {ab₁ ab₂ : AboveBelow} {n : ℕ} → Chain ab₁ ab₂ n → n ≤ 2 + isLongest (done _) = z≤n + isLongest (step _ _ (done _)) = s≤s z≤n + isLongest (step _ _ (step _ _ (done _))) = s≤s (s≤s z≤n) + isLongest {⊤} c@(step _ _ _) = ⊥-elim (¬-Chain-⊤ c) + isLongest {[ x ]} (step {_} {y} [x]≺y y≈y' c@(step _ _ _)) + rewrite [x]≺y⇒y≡⊤ x y [x]≺y with ≈-⊤-⊤ ← y≈y' = ⊥-elim (¬-Chain-⊤ c) + isLongest {⊥} (step {_} {⊥} (_ , ⊥̷≈⊥) _ _) = ⊥-elim (⊥̷≈⊥ ≈-⊥-⊥) + isLongest {⊥} (step {_} {⊤} _ ≈-⊤-⊤ c@(step _ _ _)) = ⊥-elim (¬-Chain-⊤ c) + isLongest {⊥} (step {_} {[ x ]} _ (≈-lift _) (step [x]≺y y≈z c@(step _ _ _))) + rewrite [x]≺y⇒y≡⊤ _ _ [x]≺y with ≈-⊤-⊤ ← y≈z = ⊥-elim (¬-Chain-⊤ c) - isFiniteHeightLattice : IsFiniteHeightLattice AboveBelow 2 _≈_ _⊔_ _⊓_ - isFiniteHeightLattice = record - { isLattice = isLattice - ; fixedHeight = (((⊥ , ⊤) , longestChain) , isLongest) - } + isFiniteHeightLattice : IsFiniteHeightLattice AboveBelow 2 _≈_ _⊔_ _⊓_ + isFiniteHeightLattice = record + { isLattice = isLattice + ; fixedHeight = (((⊥ , ⊤) , longestChain) , isLongest) + } - finiteHeightLattice : FiniteHeightLattice AboveBelow - finiteHeightLattice = record - { height = 2 - ; _≈_ = _≈_ - ; _⊔_ = _⊔_ - ; _⊓_ = _⊓_ - ; isFiniteHeightLattice = isFiniteHeightLattice - } + finiteHeightLattice : FiniteHeightLattice AboveBelow + finiteHeightLattice = record + { height = 2 + ; _≈_ = _≈_ + ; _⊔_ = _⊔_ + ; _⊓_ = _⊓_ + ; isFiniteHeightLattice = isFiniteHeightLattice + } diff --git a/Main.agda b/Main.agda index ce7fe61..8230d58 100644 --- a/Main.agda +++ b/Main.agda @@ -22,15 +22,13 @@ xyzw-Unique = push ((λ ()) ∷ (λ ()) ∷ (λ ()) ∷ []) (push ((λ ()) ∷ ( 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 AB.Plain (Data.Unit.tt) using () renaming (finiteHeightLattice to fhlᵘ) showAboveBelow : AB.AboveBelow → String showAboveBelow AB.⊤ = "⊤" showAboveBelow AB.⊥ = "⊥" showAboveBelow (AB.[_] tt) = "()" -fhlᵘ = finiteHeightLatticeᵘ (Data.Unit.tt) - import Lattice.Bundles.FiniteValueMap open Lattice.Bundles.FiniteValueMap.FromFiniteHeightLattice String AB.AboveBelow _≟ˢ_ fhlᵘ xyzw-Unique ≈ᵘ-dec using (FiniteMap; ≈-dec) renaming (finiteHeightLattice to fhlⁱᵖ)