From ba57e2558db98fe83db4f1026e8561b822d540f1 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Mon, 16 Feb 2026 17:41:48 -0800 Subject: [PATCH] Add more cases for associativity lemma --- Lattice/Builder.agda | 66 +++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 62 insertions(+), 4 deletions(-) diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda index dfdbaa5..dbbd6f7 100644 --- a/Lattice/Builder.agda +++ b/Lattice/Builder.agda @@ -610,7 +610,7 @@ record Graph : Set where module Tagged (noCycles : NoCycles) (total-⊔ : Total-⊔) (total-⊓ : Total-⊓) (𝓛 : Node → Σ Set FiniteHeightLattice) 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) + open IsLattice isLatticeᵇ using () renaming (≈-⊔-cong to ≡-⊔ᵇ-cong; x≼x⊔y to x≼ᵇx⊔ᵇy; ≼-antisym to ≼ᵇ-antisym; ⊔-Monotonicʳ to ⊔ᵇ-Monotonicʳ) Elem : Set Elem = Σ Node λ n → (proj₁ (𝓛 n)) @@ -694,11 +694,24 @@ record Graph : Set where ... | no _ | no _ | yes refl = l₃ ... | no _ | no _ | no _ = FiniteHeightLattice.⊥ (proj₂ (𝓛 n)) + ⊔ᵇ-prop : ∀ n₁ n₂ n₃ → (n₁ ⊔ᵇ n₂) ⊔ᵇ n₃ ≡ n₁ → + (n₁ ⊔ᵇ n₂ ≡ n₁) × (n₁ ⊔ᵇ n₃ ≡ n₁) + ⊔ᵇ-prop n₁ n₂ n₃ pⁿ = + let n₁≼n₁⊔n₂ = x≼ᵇx⊔ᵇy n₁ n₂ + n₁⊔n₂≼n₁₂⊔n₃ = x≼ᵇx⊔ᵇy (n₁ ⊔ᵇ n₂) n₃ + n₁⊔n₂≼n₁ = trans (trans (≡-⊔ᵇ-cong refl (sym pⁿ)) (n₁⊔n₂≼n₁₂⊔n₃)) pⁿ + n₁⊔n₂≡n₁ = ≼ᵇ-antisym n₁⊔n₂≼n₁ n₁≼n₁⊔n₂ + n₁≼n₁⊔n₃ = x≼ᵇx⊔ᵇy n₁ n₃ + n₁⊔n₃≼n₁₂⊔n₃ = ⊔ᵇ-Monotonicʳ n₃ n₁≼n₁⊔n₂ + n₁⊔n₃≼n₁ = trans (trans (≡-⊔ᵇ-cong refl (sym pⁿ)) (n₁⊔n₃≼n₁₂⊔n₃)) pⁿ + n₁⊔n₃≡n₁ = ≼ᵇ-antisym n₁⊔n₃≼n₁ n₁≼n₁⊔n₃ + in (n₁⊔n₂≡n₁ , n₁⊔n₃≡n₁) + Reassocˡ : ∀ e₁ e₂ e₃ → ((e₁ ⊔ e₂) ⊔ e₃) ≈ (proj₁ ((e₁ ⊔ e₂) ⊔ e₃) , payloadˡ e₁ e₂ e₃) Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃) with n ← (n₁ ⊔ᵇ n₂) ⊔ᵇ n₃ in pⁿ - with n ≟ n₁ | n ≟ n₂ | n ≟ n₃ + with n ≟ n₁ in d₁ | n ≟ n₂ in d₂ | n ≟ n₃ in d₃ Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃) | yes refl | yes refl | yes refl with (n₁ ⊔ᵇ n₁) ≟ n₁ @@ -726,11 +739,56 @@ record Graph : Set where ... | _ | yes n₁≡n₂ = ⊥-elim (n₁≢n₂ n₁≡n₂) ... | yes refl | no _ = ≈-refl Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃) - | yes p₁@refl | no n₁≢n₂ | no n₁≢n₃ = {!!} + | yes p₁@refl | no n₁≢n₂ | no n₁≢n₃ + using (n₁⊔n₂≡n₁ , n₁⊔n₃≡n₁) ← ⊔ᵇ-prop n₁ n₂ n₃ pⁿ + with n₁ ⊔ᵇ n₂ ≟ n₁ + ... | no n₁⊔n₂≢n₁ = ⊥-elim (n₁⊔n₂≢n₁ n₁⊔n₂≡n₁) + ... | yes p rewrite p + with n₁ ≟ n₁ | n₁ ≟ n₂ + ... | no n₁≢n₁ | _ = ⊥-elim (n₁≢n₁ refl) + ... | _ | yes n₁≡n₂ = ⊥-elim (n₁≢n₂ n₁≡n₂) + ... | yes refl | no _ = ≈-refl + Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃) + | no n₂≢n₁ | yes p₂@refl | yes p₃@refl + using n₁⊔n₂≡n₂ ← trans (trans (≡-⊔ᵇ-cong (refl {x = n₁}) (sym (⊔ᵇ-idemp n₂))) (sym (⊔ᵇ-assoc n₁ n₂ n₂))) pⁿ + with (n₁ ⊔ᵇ n₂) ≟ n₂ + ... | no n₁⊔n₂≢n₂ = ⊥-elim (n₁⊔n₂≢n₂ n₁⊔n₂≡n₂) + ... | yes p rewrite p + with n₂ ≟ n₁ | n₂ ≟ n₂ + ... | yes n₂≡n₁ | _ = ⊥-elim (n₂≢n₁ n₂≡n₁) + ... | _ | no n₂≢n₂ = ⊥-elim (n₂≢n₂ refl) + ... | no _ | yes refl = ≈-refl + Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃) + | no n₂≢n₁ | yes p₂@refl | no n₂≢n₃ + using (n₂⊔n₁≡n₂ , n₂⊔n₃≡n₂) ← ⊔ᵇ-prop n₂ n₁ n₃ (trans (≡-⊔ᵇ-cong (⊔ᵇ-comm n₂ n₁) (refl {x = n₃})) pⁿ) + with (n₁ ⊔ᵇ n₂) ≟ n₁ | (n₁ ⊔ᵇ n₂) ≟ n₂ + ... | yes n₁⊔n₂≡n₁ | _ = ⊥-elim (n₂≢n₁ (trans (sym n₂⊔n₁≡n₂) (trans (⊔ᵇ-comm n₂ n₁) (n₁⊔n₂≡n₁)))) + ... | _ | no n₁⊔n₂≢n₂ = ⊥-elim (n₁⊔n₂≢n₂ (trans (⊔ᵇ-comm n₁ n₂) n₂⊔n₁≡n₂)) + ... | no n₁⊔n₂≢n₁ | yes p rewrite p + with n₂ ≟ n₂ + ... | no n₂≢n₂ = ⊥-elim (n₂≢n₂ refl) + ... | yes refl = ≈-refl + Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃) + | no n₃≢n₁ | no n₃≢n₂ | yes p₃@refl + with n₁₂ ← n₁ ⊔ᵇ n₂ + with n₃ ≟ n₁₂ + ... | no n₃≢n₁₂ = ≈-refl + ... | yes refl rewrite d₁ rewrite d₂ = {!!} -- TODO: need ⊥ ⊔ n₃ ≡ n₃ + Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃) + | no n≢n₁ | no n≢n₂ | no n≢n₃ + with n₁₂ ← n₁ ⊔ᵇ n₂ + with n₁₂ ≟ n₁ | n₁₂ ≟ n₂ | n ≟ n₃ | n ≟ n₁₂ + ... | _ | _ | yes n≡n₃ | _ = ⊥-elim (n≢n₃ n≡n₃) + ... | _ | _ | no _ | no n≢n₁₂ = ≈-refl + ... | yes refl | yes refl | no _ | yes refl = ⊥-elim (n≢n₁ refl) + ... | yes refl | no n₁₂≢n₂ | no _ | yes refl = ⊥-elim (n≢n₁ refl) + ... | no n₁₂≢n₁ | yes refl | no _ | yes refl = ⊥-elim (n≢n₂ refl) + ... | no n₁₂≢n₁ | no n₁₂≢n₂ | no _ | yes refl = ≈-refl Reassocʳ : ∀ e₁ e₂ e₃ → (e₁ ⊔ (e₂ ⊔ e₃)) ≈ (proj₁ (e₁ ⊔ (e₂ ⊔ e₃)) , payloadʳ e₁ e₂ e₃) - Reassocʳ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃) = {!!} + Reassocʳ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃) + = {!!} ⊔-assoc : ∀ (e₁ e₂ e₃ : Elem) → ((e₁ ⊔ e₂) ⊔ e₃) ≈ (e₁ ⊔ (e₂ ⊔ e₃)) ⊔-assoc e₁@(n₁ , l₁) e₂@(n₂ , l₂) e₃@(n₃ , l₃)