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

Make code less brittle for when \McL changes

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin
2026-02-16 19:43:10 -08:00
parent c64504b819
commit da2b6dd5c6
1 changed files with 26 additions and 20 deletions
Download Patch File Download Diff File Expand all files Collapse all files

46
Lattice/Builder.agda
View File

@@ -615,37 +615,43 @@ record Graph : Set where
Elem : Set Elem : Set
Elem = Σ Node λ n → (proj₁ (𝓛 n)) Elem = Σ Node λ n → (proj₁ (𝓛 n))
LatticeT : Node → Set
LatticeT n = proj₁ (𝓛 n)
FHL : (n : Node) → FiniteHeightLattice (LatticeT n)
FHL n = proj₂ (𝓛 n)
data _≈_ : Elem → Elem → Set where data _≈_ : Elem → Elem → Set where
≈-lift : ∀ {n : Node} {l₁ l₂ : proj₁ (𝓛 n)} → ≈-lift : ∀ {n : Node} {l₁ l₂ : LatticeT n} →
FiniteHeightLattice._≈_ (proj₂ (𝓛 n)) l₁ l₂ → FiniteHeightLattice._≈_ (FHL n) l₁ l₂ →
(n , l₁) ≈ (n , l₂) (n , l₁) ≈ (n , l₂)
≈-refl : ∀ {e : Elem} → e ≈ e ≈-refl : ∀ {e : Elem} → e ≈ e
≈-refl {n , l} = ≈-lift (FiniteHeightLattice.≈-refl (proj₂ (𝓛 n))) ≈-refl {n , l} = ≈-lift (FiniteHeightLattice.≈-refl (FHL n))
≈-sym : ∀ {e₁ e₂ : Elem} → e₁ ≈ e₂ → e₂ ≈ e₁ ≈-sym : ∀ {e₁ e₂ : Elem} → e₁ ≈ e₂ → e₂ ≈ e₁
≈-sym {n₁ , l₁} (≈-lift l₁≈l₂) = ≈-lift (FiniteHeightLattice.≈-sym (proj₂ (𝓛 n₁)) l₁≈l₂) ≈-sym {n₁ , l₁} (≈-lift l₁≈l₂) = ≈-lift (FiniteHeightLattice.≈-sym (FHL n₁) l₁≈l₂)
≈-trans : ∀ {e₁ e₂ e₃ : Elem} → e₁ ≈ e₂ → e₂ ≈ e₃ → e₁ ≈ e₃ ≈-trans : ∀ {e₁ e₂ e₃ : Elem} → e₁ ≈ e₂ → e₂ ≈ e₃ → e₁ ≈ e₃
≈-trans {n₁ , l₁} (≈-lift l₁≈l₂) (≈-lift l₂≈l₃) = ≈-lift (FiniteHeightLattice.≈-trans (proj₂ (𝓛 n₁)) l₁≈l₂ l₂≈l₃) ≈-trans {n₁ , l₁} (≈-lift l₁≈l₂) (≈-lift l₂≈l₃) = ≈-lift (FiniteHeightLattice.≈-trans (FHL n₁) l₁≈l₂ l₂≈l₃)
_⊔_ : Elem → Elem → Elem _⊔_ : Elem → Elem → Elem
_⊔_ e₁ e₂ _⊔_ e₁ e₂
using n₁ ← proj₁ e₁ using n₂ ← proj₁ e₂ using n₁ ← proj₁ e₁ using n₂ ← proj₁ e₂
using n' ← n₁ ⊔ᵇ n₂ = (n' , select n' e₁ e₂) using n' ← n₁ ⊔ᵇ n₂ = (n' , select n' e₁ e₂)
where where
select : ∀ n' e₁ e₂ → proj₁ (𝓛 n') select : ∀ n' e₁ e₂ → LatticeT n'
select n' (n₁ , l₁) (n₂ , l₂) select n' (n₁ , l₁) (n₂ , l₂)
with n' ≟ n₁ | n' ≟ n₂ with n' ≟ n₁ | n' ≟ n₂
... | yes refl | yes refl = FiniteHeightLattice._⊔_ (proj₂ (𝓛 n')) l₁ l₂ ... | yes refl | yes refl = FiniteHeightLattice._⊔_ (FHL n') l₁ l₂
... | yes refl | _ = l₁ ... | yes refl | _ = l₁
... | _ | yes refl = l₂ ... | _ | yes refl = l₂
... | no _ | no _ = FiniteHeightLattice.⊥ (proj₂ (𝓛 n')) ... | no _ | no _ = FiniteHeightLattice.⊥ (FHL n')
⊔-idemp : ∀ e → (e ⊔ e) ≈ e ⊔-idemp : ∀ e → (e ⊔ e) ≈ e
⊔-idemp (n , l) rewrite ⊔ᵇ-idemp n ⊔-idemp (n , l) rewrite ⊔ᵇ-idemp n
with n ≟ n with n ≟ n
... | yes refl = ≈-lift (FiniteHeightLattice.⊔-idemp (proj₂ (𝓛 n)) l) ... | yes refl = ≈-lift (FiniteHeightLattice.⊔-idemp (FHL n) l)
... | no n≢n = ⊥-elim (n≢n refl) ... | no n≢n = ⊥-elim (n≢n refl)
⊔-comm : ∀ (e₁ e₂ : Elem) → (e₁ ⊔ e₂) ≈ (e₂ ⊔ e₁) ⊔-comm : ∀ (e₁ e₂ : Elem) → (e₁ ⊔ e₂) ≈ (e₂ ⊔ e₁)
@@ -653,10 +659,10 @@ record Graph : Set where
rewrite ⊔ᵇ-comm n₁ n₂ rewrite ⊔ᵇ-comm n₁ n₂
with n ← n₂ ⊔ᵇ n₁ with n ← n₂ ⊔ᵇ n₁
with n ≟ n₁ | n ≟ n₂ with n ≟ n₁ | n ≟ n₂
... | yes refl | yes refl = ≈-lift (FiniteHeightLattice.⊔-comm (proj₂ (𝓛 n)) l₁ l₂) ... | yes refl | yes refl = ≈-lift (FiniteHeightLattice.⊔-comm (FHL n) l₁ l₂)
... | no _ | yes refl = ≈-lift (FiniteHeightLattice.≈-refl (proj₂ (𝓛 n))) ... | no _ | yes refl = ≈-lift (FiniteHeightLattice.≈-refl (FHL n))
... | yes refl | no _ = ≈-lift (FiniteHeightLattice.≈-refl (proj₂ (𝓛 n))) ... | yes refl | no _ = ≈-lift (FiniteHeightLattice.≈-refl (FHL n))
... | no _ | no _ = ≈-lift (FiniteHeightLattice.≈-refl (proj₂ (𝓛 n))) ... | no _ | no _ = ≈-lift (FiniteHeightLattice.≈-refl (FHL n))
private private
scary : ∀ (n₁ n₂ : Node) → (p : n₁ ≡ n₂) → (n₁ ≟ n₂) ≡ subst (λ n → Dec (n₁ ≡ n)) p (yes refl) scary : ∀ (n₁ n₂ : Node) → (p : n₁ ≡ n₂) → (n₁ ≟ n₂) ≡ subst (λ n → Dec (n₁ ≡ n)) p (yes refl)
@@ -665,10 +671,10 @@ record Graph : Set where
... | no n₁≢n₂ = ⊥-elim (n₁≢n₂ refl) ... | no n₁≢n₂ = ⊥-elim (n₁≢n₂ refl)
payloadˡ : ∀ e₁ e₂ e₃ → let n = proj₁ ((e₁ ⊔ e₂) ⊔ e₃) payloadˡ : ∀ e₁ e₂ e₃ → let n = proj₁ ((e₁ ⊔ e₂) ⊔ e₃)
in proj₁ (𝓛 n) in LatticeT n
payloadˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃) payloadˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
with n ← (n₁ ⊔ᵇ n₂) ⊔ᵇ n₃ with n ← (n₁ ⊔ᵇ n₂) ⊔ᵇ n₃
using _⊔ⁿ_ ← FiniteHeightLattice._⊔_ (proj₂ (𝓛 n)) using _⊔ⁿ_ ← FiniteHeightLattice._⊔_ (FHL n)
with n ≟ n₁ | n ≟ n₂ | n ≟ n₃ with n ≟ n₁ | n ≟ n₂ | n ≟ n₃
... | yes refl | yes refl | yes refl = (l₁ ⊔ⁿ l₂) ⊔ⁿ l₃ ... | yes refl | yes refl | yes refl = (l₁ ⊔ⁿ l₂) ⊔ⁿ l₃
... | yes refl | yes refl | no _ = l₁ ⊔ⁿ l₂ ... | yes refl | yes refl | no _ = l₁ ⊔ⁿ l₂
@@ -677,13 +683,13 @@ record Graph : Set where
... | no _ | yes refl | yes refl = l₂ ⊔ⁿ l₃ ... | no _ | yes refl | yes refl = l₂ ⊔ⁿ l₃
... | no _ | yes refl | no _ = l₂ ... | no _ | yes refl | no _ = l₂
... | no _ | no _ | yes refl = l₃ ... | no _ | no _ | yes refl = l₃
... | no _ | no _ | no _ = FiniteHeightLattice.⊥ (proj₂ (𝓛 n)) ... | no _ | no _ | no _ = FiniteHeightLattice.⊥ (FHL n)
payloadʳ : ∀ e₁ e₂ e₃ → let n = proj₁ (e₁ ⊔ (e₂ ⊔ e₃)) payloadʳ : ∀ e₁ e₂ e₃ → let n = proj₁ (e₁ ⊔ (e₂ ⊔ e₃))
in proj₁ (𝓛 n) in LatticeT n
payloadʳ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃) payloadʳ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
with n ← n₁ ⊔ᵇ (n₂ ⊔ᵇ n₃) with n ← n₁ ⊔ᵇ (n₂ ⊔ᵇ n₃)
using _⊔ⁿ_ ← FiniteHeightLattice._⊔_ (proj₂ (𝓛 n)) using _⊔ⁿ_ ← FiniteHeightLattice._⊔_ (FHL n)
with n ≟ n₁ | n ≟ n₂ | n ≟ n₃ with n ≟ n₁ | n ≟ n₂ | n ≟ n₃
... | yes refl | yes refl | yes refl = l₁ ⊔ⁿ (l₂ ⊔ⁿ l₃) ... | yes refl | yes refl | yes refl = l₁ ⊔ⁿ (l₂ ⊔ⁿ l₃)
... | yes refl | yes refl | no _ = l₁ ⊔ⁿ l₂ ... | yes refl | yes refl | no _ = l₁ ⊔ⁿ l₂
@@ -692,7 +698,7 @@ record Graph : Set where
... | no _ | yes refl | yes refl = l₂ ⊔ⁿ l₃ ... | no _ | yes refl | yes refl = l₂ ⊔ⁿ l₃
... | no _ | yes refl | no _ = l₂ ... | no _ | yes refl | no _ = l₂
... | no _ | no _ | yes refl = l₃ ... | no _ | no _ | yes refl = l₃
... | no _ | no _ | no _ = FiniteHeightLattice.⊥ (proj₂ (𝓛 n)) ... | no _ | no _ | no _ = FiniteHeightLattice.⊥ (FHL n)
⊔ᵇ-prop : ∀ n₁ n₂ n₃ → (n₁ ⊔ᵇ n₂) ⊔ᵇ n₃ ≡ n₁ → ⊔ᵇ-prop : ∀ n₁ n₂ n₃ → (n₁ ⊔ᵇ n₂) ⊔ᵇ n₃ ≡ n₁ →
(n₁ ⊔ᵇ n₂ ≡ n₁) × (n₁ ⊔ᵇ n₃ ≡ n₁) (n₁ ⊔ᵇ n₂ ≡ n₁) × (n₁ ⊔ᵇ n₃ ≡ n₁)
@@ -865,7 +871,7 @@ record Graph : Set where
rewrite trans (sym pˡ ) pʳ rewrite trans (sym pˡ ) pʳ
with nʳ ≟ n₁ | nʳ ≟ n₂ | nʳ ≟ n₃ with nʳ ≟ n₁ | nʳ ≟ n₂ | nʳ ≟ n₃
... | yes refl | yes refl | yes refl = ... | yes refl | yes refl | yes refl =
let l-assoc = FiniteHeightLattice.⊔-assoc (proj₂ (𝓛 n₁)) l₁ l₂ l₃ let l-assoc = FiniteHeightLattice.⊔-assoc (FHL n₁) l₁ l₂ l₃
in ≈-trans final₁ (≈-trans (≈-lift l-assoc) (≈-sym final₂)) in ≈-trans final₁ (≈-trans (≈-lift l-assoc) (≈-sym final₂))
... | yes refl | yes refl | no _ = ≈-trans final₁ (≈-sym final₂) ... | yes refl | yes refl | no _ = ≈-trans final₁ (≈-sym final₂)
... | yes refl | no _ | yes refl = ≈-trans final₁ (≈-sym final₂) ... | yes refl | no _ | yes refl = ≈-trans final₁ (≈-sym final₂)