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

Prove the other direction for associativity

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin
2026-02-16 19:31:39 -08:00
parent ba57e2558d
commit 4a9e7492f4
1 changed files with 66 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

68
Lattice/Builder.agda
View File

@@ -783,12 +783,76 @@ record Graph : Set where
... | yes refl | yes refl | no _ | yes refl = ⊥-elim (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) ... | 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₁ | yes refl | no _ | yes refl = ⊥-elim (n≢n₂ refl)
... | no n₁₂≢n₁ | no n₁₂≢n₂ | no _ | yes refl = ≈-refl ... | no _ | no _ | 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₃)
= {!!} with n ← n₁ ⊔ᵇ (n₂ ⊔ᵇ n₃) in pⁿ
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₁
... | no n₁≢n₁ = ⊥-elim (n₁≢n₁ (⊔ᵇ-idemp 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₃)
| yes refl | yes refl | no n₁≢n₃
using n₁⊔n₃≡n₁ ← trans (≡-⊔ᵇ-cong (sym (⊔ᵇ-idemp n₁)) (refl {x = n₃})) (trans (⊔ᵇ-assoc n₁ n₁ n₃) pⁿ)
rewrite n₁⊔n₃≡n₁
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₃)
| yes refl | no n₁≢n₂ | yes refl
using n₂⊔n₁≡n₁ ← trans (trans (trans (≡-⊔ᵇ-cong (refl {x = n₂}) (sym (⊔ᵇ-idemp n₁))) (sym (⊔ᵇ-assoc n₂ n₁ n₁))) (⊔ᵇ-comm _ _)) pⁿ
rewrite n₂⊔n₁≡n₁
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₃)
| yes refl | no n₁≢n₂ | no n₁≢n₃
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₁ | yes refl | yes refl
rewrite ⊔ᵇ-idemp n₂
with n₂ ≟ n₂
... | no n₂≢n₂ = ⊥-elim (n₂≢n₂ refl)
... | yes refl = ≈-refl
Reassocʳ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
| no n₂≢n₁ | yes refl | no n₂≢n₃
using (n₂⊔n₃=n₂ , n₂⊔n₁=n₂) ← ⊔ᵇ-prop n₂ n₃ n₁ (trans (⊔ᵇ-comm _ _) pⁿ)
rewrite n₂⊔n₃=n₂
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₁ | no n₃≢n₂ | yes refl
using (n₃⊔n₂≡n₃ , n₃⊔n₁≡n₃) ← ⊔ᵇ-prop n₃ n₂ n₁ (trans (⊔ᵇ-comm _ _) (trans (≡-⊔ᵇ-cong (refl {x = n₁}) (⊔ᵇ-comm n₃ n₂)) pⁿ))
rewrite trans (⊔ᵇ-comm _ _) n₃⊔n₂≡n₃
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₁ | 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 _ = ≈-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
⊔-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₃)