DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Add more cases for associativity lemma

Browse Source
This commit is contained in:
Danila Fedorin
2026-02-16 17:41:48 -08:00
parent 1c37141234
commit ba57e2558d
1 changed files with 62 additions and 4 deletions
Download Patch File Download Diff File Expand all files Collapse all files

66
Lattice/Builder.agda
View File

@@ -610,7 +610,7 @@ record Graph : Set where
module Tagged (noCycles : NoCycles) (total-⊔ : Total-⊔) (total-⊓ : Total-⊓) (𝓛 : Node → Σ Set FiniteHeightLattice) 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 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 : Set
Elem = Σ Node λ n → (proj₁ (𝓛 n)) Elem = Σ Node λ n → (proj₁ (𝓛 n))
@@ -694,11 +694,24 @@ record Graph : Set where
... | no _ | no _ | yes refl = l₃ ... | no _ | no _ | yes refl = l₃
... | no _ | no _ | no _ = FiniteHeightLattice.⊥ (proj₂ (𝓛 n)) ... | 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₃ → Reassocˡ : ∀ e₁ e₂ e₃ →
((e₁ ⊔ e₂) ⊔ e₃) ≈ (proj₁ ((e₁ ⊔ e₂) ⊔ e₃) , payloadˡ 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₃)
with n ← (n₁ ⊔ᵇ n₂) ⊔ᵇ n₃ in pⁿ 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₃) Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
| yes refl | yes refl | yes refl | yes refl | yes refl | yes refl
with (n₁ ⊔ᵇ n₁) ≟ n₁ with (n₁ ⊔ᵇ n₁) ≟ n₁
@@ -726,11 +739,56 @@ record Graph : Set where
... | _ | yes n₁≡n₂ = ⊥-elim (n₁≢n₂ n₁≡n₂) ... | _ | yes n₁≡n₂ = ⊥-elim (n₁≢n₂ n₁≡n₂)
... | yes refl | no _ = ≈-refl ... | yes refl | no _ = ≈-refl
Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃) 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₃ → Reassocʳ : ∀ e₁ e₂ e₃ →
(e₁ ⊔ (e₂ ⊔ e₃)) ≈ (proj₁ (e₁ ⊔ (e₂ ⊔ e₃)) , payloadʳ 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₁ e₂ e₃ : Elem) → ((e₁ ⊔ e₂) ⊔ e₃) ≈ (e₁ ⊔ (e₂ ⊔ e₃))
⊔-assoc e₁@(n₁ , l₁) e₂@(n₂ , l₂) e₃@(n₃ , l₃) ⊔-assoc e₁@(n₁ , l₁) e₂@(n₂ , l₂) e₃@(n₃ , l₃)