From f5457d884144b1592d5ef7ba7706546b2f092e27 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 26 Jul 2025 13:16:22 +0200 Subject: [PATCH] Move proof of least element into FiniteHeightLattice Signed-off-by: Danila Fedorin --- Analysis/Forward.agda | 4 ++-- Fixedpoint.agda | 23 ++++------------------- Isomorphism.agda | 1 + Lattice.agda | 25 ++++++++++++++++++++++++- 4 files changed, 31 insertions(+), 22 deletions(-) diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda index fba6e22..7db25c2 100644 --- a/Analysis/Forward.agda +++ b/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 diff --git a/Fixedpoint.agda b/Fixedpoint.agda index 88009e3..c266dd7 100644 --- a/Fixedpoint.agda +++ b/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 ⊥ᴬ)) diff --git a/Isomorphism.agda b/Isomorphism.agda index b4f30b6..4c856bf 100644 --- a/Isomorphism.agda +++ b/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 ⊤₁ diff --git a/Lattice.agda b/Lattice.agda index 2fe2660..1ede49c 100644 --- a/Lattice.agda +++ b/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}