From 16fa4cd1d81c49bd7ca07b9e4d90e134ece3b85c Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Thu, 9 May 2024 20:11:04 -0700 Subject: [PATCH] Use records rather than nested pairs to represent 'fixed height' Signed-off-by: Danila Fedorin --- Analysis/Forward.agda | 3 ++- Chain.agda | 13 +++++++++---- Fixedpoint.agda | 16 +++++++++++----- Isomorphism.agda | 16 ++++++++++++---- Lattice/AboveBelow.agda | 7 ++++++- Lattice/IterProd.agda | 7 ++++--- Lattice/Prod.agda | 32 ++++++++++++-------------------- Lattice/Unit.agda | 7 ++++++- 8 files changed, 62 insertions(+), 39 deletions(-) diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda index a5edcd9..b4ab689 100644 --- a/Analysis/Forward.agda +++ b/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 diff --git a/Chain.agda b/Chain.agda index 44c6bf7..5986083 100644 --- a/Chain.agda +++ b/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 - Height height = (Σ (A × A) (λ (a₁ , a₂) → Chain a₁ a₂ height) × Bounded height) + record Height (height : ℕ) : Set a where + field + ⊥ : A + ⊤ : A + + longestChain : Chain ⊥ ⊤ height + bounded : Bounded height diff --git a/Fixedpoint.agda b/Fixedpoint.agda index 3e6ca39..5e9f109 100644 --- a/Fixedpoint.agda +++ b/Fixedpoint.agda @@ -23,15 +23,21 @@ import Chain module ChainA = Chain _≈_ ≈-equiv _≺_ ≺-cong private - ⊥ᴬ : A - ⊥ᴬ = proj₁ (proj₁ (proj₁ fixedHeight)) + open ChainA.Height 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 diff --git a/Isomorphism.agda b/Isomorphism.agda index 5e731ec..cc79eb8 100644 --- a/Isomorphism.agda +++ b/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₁) - open import Chain _≈₂_ ≈₂-equiv _≺₂_ ≺₂-cong using () renaming (Chain to Chain₂; done to done₂; step to step₂) + import Chain + 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 diff --git a/Lattice/AboveBelow.agda b/Lattice/AboveBelow.agda index 970968a..f85bc45 100644 --- a/Lattice/AboveBelow.agda +++ 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 diff --git a/Lattice/IterProd.agda b/Lattice/IterProd.agda index 8eb1ec2..249f58e 100644 --- a/Lattice/IterProd.agda +++ b/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 diff --git a/Lattice/Prod.agda b/Lattice/Prod.agda index 5218848..369bb81 100644 --- a/Lattice/Prod.agda +++ b/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 - ⊥₁ = proj₁ (proj₁ (proj₁ fhA)) - - ⊤₁ : A - ⊤₁ = proj₂ (proj₁ (proj₁ fhA)) - - ⊥₂ : B - ⊥₂ = proj₁ (proj₁ (proj₁ fhB)) - - ⊤₂ : B - ⊤₂ = proj₂ (proj₁ (proj₁ fhB)) + open ChainA.Height fhA using () renaming (⊥ to ⊥₁; ⊤ to ⊤₁; longestChain to longestChain₁; bounded to bounded₁) + open ChainB.Height fhB using () renaming (⊥ to ⊥₂; ⊤ to ⊤₂; longestChain to longestChain₂; bounded to bounded₂) 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 = - ( ( ((⊥₁ , ⊥₂) , (⊤₁ , ⊤₂)) - , concat - (ChainMapping₁.Chain-map (λ a → (a , ⊥₂)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) (proj₂ (proj₁ fhA))) - (ChainMapping₂.Chain-map (λ b → (⊤₁ , 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₂)) - ) + fixedHeight = record + { ⊥ = (⊥₁ , ⊥₂) + ; ⊤ = (⊤₁ , ⊤₂) + ; longestChain = concat + (ChainMapping₁.Chain-map (λ a → (a , ⊥₂)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) longestChain₁) + (ChainMapping₂.Chain-map (λ b → (⊤₁ , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) longestChain₂) + ; bounded = λ 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-≤ (bounded₁ a₁a₂) (bounded₂ b₁b₂)) + } isFiniteHeightLattice : IsFiniteHeightLattice (A × B) (h₁ + h₂) _≈_ _⊔_ _⊓_ isFiniteHeightLattice = record diff --git a/Lattice/Unit.agda b/Lattice/Unit.agda index ab3578b..e4d0685 100644 --- a/Lattice/Unit.agda +++ b/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