From 1c2bcc2d92a9e3f0e58d68b9c12e8b4d82904e20 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Mon, 16 Feb 2026 20:15:10 -0800 Subject: [PATCH] Require bottom element to actually be bottom; finish proof Signed-off-by: Danila Fedorin --- Lattice.agda | 8 +++++++- Lattice/Builder.agda | 11 +++++++---- 2 files changed, 14 insertions(+), 5 deletions(-) diff --git a/Lattice.agda b/Lattice.agda index d63aed5..23e10ad 100644 --- a/Lattice.agda +++ b/Lattice.agda @@ -260,6 +260,12 @@ record IsFiniteHeightLattice {a} (A : Set a) open MyChain.Height fixedHeight using (⊥; ⊤) public + Known-⊥ : Set a + Known-⊥ = ∀ (a : A) → ⊥ ≼ a + + Known-⊤ : Set a + Known-⊤ = ∀ (a : A) → a ≼ ⊤ + -- 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 @@ -267,7 +273,7 @@ record IsFiniteHeightLattice {a} (A : Set a) open MyChain.Height fixedHeight using (bounded; longestChain) - ⊥≼ : ∀ (a : A) → ⊥ ≼ a + ⊥≼ : Known-⊥ ⊥≼ a with ≈-dec a ⊥ ... | yes a≈⊥ = ≼-cong a≈⊥ ≈-refl (≼-refl a) ... | no a̷≈⊥ with ≈-dec ⊥ (a ⊓ ⊥) diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda index bea2a8a..9a41c62 100644 --- a/Lattice/Builder.agda +++ b/Lattice/Builder.agda @@ -607,7 +607,7 @@ record Graph : Set where ; absorb-⊓-⊔ = absorb-⊓-⊔ } - module Tagged (noCycles : NoCycles) (total-⊔ : Total-⊔) (total-⊓ : Total-⊓) (𝓛 : Node → Σ Set FiniteHeightLattice) where + module Tagged (noCycles : NoCycles) (total-⊔ : Total-⊔) (total-⊓ : Total-⊓) (𝓛 : Node → Σ Set λ L → Σ (FiniteHeightLattice L) λ fhl → FiniteHeightLattice.Known-⊥ fhl × FiniteHeightLattice.Known-⊤ fhl) where open Basic noCycles total-⊔ total-⊓ using () renaming (_⊔_ to _⊔ᵇ_; _⊓_ to _⊓ᵇ_; ⊔-idemp to ⊔ᵇ-idemp; ⊔-comm to ⊔ᵇ-comm; ⊔-assoc to ⊔ᵇ-assoc; _≼_ to _≼ᵇ_; isJoinSemilattice to isJoinSemilatticeᵇ; isMeetSemilattice to isMeetSemilatticeᵇ; isLattice to isLatticeᵇ) open IsLattice isLatticeᵇ using () renaming (≈-⊔-cong to ≡-⊔ᵇ-cong; x≼x⊔y to x≼ᵇx⊔ᵇy; ≼-antisym to ≼ᵇ-antisym; ⊔-Monotonicʳ to ⊔ᵇ-Monotonicʳ) @@ -619,7 +619,10 @@ record Graph : Set where LatticeT n = proj₁ (𝓛 n) FHL : (n : Node) → FiniteHeightLattice (LatticeT n) - FHL n = proj₂ (𝓛 n) + FHL n = proj₁ (proj₂ (𝓛 n)) + + ⊥≼x : ∀ {n : Node} (l : LatticeT n) → FiniteHeightLattice._≼_ (FHL n) (FiniteHeightLattice.⊥ (FHL n)) l + ⊥≼x {n} = proj₁ (proj₂ (proj₂ (𝓛 n))) data _≈_ : Elem → Elem → Set where ≈-lift : ∀ {n : Node} {l₁ l₂ : LatticeT n} → @@ -779,7 +782,7 @@ record Graph : Set where with n₁₂ ← n₁ ⊔ᵇ n₂ with n₃ ≟ n₁₂ ... | no n₃≢n₁₂ = ≈-refl - ... | yes refl rewrite d₁ rewrite d₂ = {!!} -- TODO: need ⊥ ⊔ n₃ ≡ n₃ + ... | yes refl rewrite d₁ rewrite d₂ = ≈-lift (⊥≼x l₃) -- TODO: need ⊥ ⊔ n₃ ≡ n₃ Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃) | no n≢n₁ | no n≢n₂ | no n≢n₃ with n₁₂ ← n₁ ⊔ᵇ n₂ @@ -825,7 +828,7 @@ record Graph : Set where with n₂₃ ← n₂ ⊔ᵇ n₃ with n₁ ≟ n₂₃ ... | no n₁≢n₂₃ = ≈-refl - ... | yes refl rewrite d₂ rewrite d₃ = {!!} -- TODO: need ⊥ ⊔ n₃ ≡ n₃ + ... | yes refl rewrite d₂ rewrite d₃ = ≈-lift (FiniteHeightLattice.≈-trans (FHL n₁) (FiniteHeightLattice.⊔-comm (FHL n₁) _ _) (⊥≼x l₁)) Reassocʳ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃) | no n₂≢n₁ | yes refl | yes refl rewrite ⊔ᵇ-idemp n₂