From 4a9e7492f4fe75ca1071d3eceddd1f9e695c4122 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Mon, 16 Feb 2026 19:31:39 -0800
Subject: [PATCH] Prove the other direction for associativity

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 Lattice/Builder.agda | 68 ++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 66 insertions(+), 2 deletions(-)

diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda
index dbbd6f7..ed4ccf9 100644
--- a/Lattice/Builder.agda
+++ b/Lattice/Builder.agda
@@ -783,12 +783,76 @@ record Graph : Set where
             ...       | 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
+            ...       | no _ | no _ | 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₃)
-                    = {!!}
+                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₁@(n₁ , l₁) e₂@(n₂ , l₂) e₃@(n₃ , l₃)