Add some cases for associativity lemma
This commit is contained in:
@@ -608,7 +608,9 @@ 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 _≼ᵇ_)
|
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)
|
||||||
|
|
||||||
Elem : Set
|
Elem : Set
|
||||||
Elem = Σ Node λ n → (proj₁ (𝓛 n))
|
Elem = Σ Node λ n → (proj₁ (𝓛 n))
|
||||||
@@ -657,60 +659,85 @@ record Graph : Set where
|
|||||||
... | no _ | no _ = ≈-lift (FiniteHeightLattice.≈-refl (proj₂ (𝓛 n)))
|
... | no _ | no _ = ≈-lift (FiniteHeightLattice.≈-refl (proj₂ (𝓛 n)))
|
||||||
|
|
||||||
private
|
private
|
||||||
data Expr (A : Set) : Set where
|
scary : ∀ (n₁ n₂ : Node) → (p : n₁ ≡ n₂) → (n₁ ≟ n₂) ≡ subst (λ n → Dec (n₁ ≡ n)) p (yes refl)
|
||||||
`_ : A → Expr A
|
scary n₁ n₂ refl with n₁ ≟ n₂
|
||||||
_⊔ᵉ_ : Expr A → Expr A → Expr A
|
... | yes refl = refl
|
||||||
|
... | no n₁≢n₂ = ⊥-elim (n₁≢n₂ refl)
|
||||||
|
|
||||||
eval : ∀ {A} → (A → A → A) → Expr A → A
|
payloadˡ : ∀ e₁ e₂ e₃ → let n = proj₁ ((e₁ ⊔ e₂) ⊔ e₃)
|
||||||
eval _ (` v) = v
|
in proj₁ (𝓛 n)
|
||||||
eval f (e₁ ⊔ᵉ e₂) = f (eval f e₁) (eval f e₂)
|
payloadˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
|
||||||
|
with n ← (n₁ ⊔ᵇ n₂) ⊔ᵇ n₃
|
||||||
|
using _⊔ⁿ_ ← FiniteHeightLattice._⊔_ (proj₂ (𝓛 n))
|
||||||
|
with n ≟ n₁ | n ≟ n₂ | n ≟ n₃
|
||||||
|
... | yes refl | yes refl | yes refl = (l₁ ⊔ⁿ l₂) ⊔ⁿ l₃
|
||||||
|
... | yes refl | yes refl | no _ = l₁ ⊔ⁿ l₂
|
||||||
|
... | yes refl | no _ | yes refl = l₁ ⊔ⁿ l₃
|
||||||
|
... | yes refl | no _ | no _ = l₁
|
||||||
|
... | no _ | yes refl | yes refl = l₂ ⊔ⁿ l₃
|
||||||
|
... | no _ | yes refl | no _ = l₂
|
||||||
|
... | no _ | no _ | yes refl = l₃
|
||||||
|
... | no _ | no _ | no _ = FiniteHeightLattice.⊥ (proj₂ (𝓛 n))
|
||||||
|
|
||||||
mapᵉ : ∀ {A B} → (A → B) → Expr A → Expr B
|
payloadʳ : ∀ e₁ e₂ e₃ → let n = proj₁ (e₁ ⊔ (e₂ ⊔ e₃))
|
||||||
mapᵉ f (` a) = ` (f a)
|
in proj₁ (𝓛 n)
|
||||||
mapᵉ f (e₁ ⊔ᵉ e₂) = (mapᵉ f e₁) ⊔ᵉ (mapᵉ f e₂)
|
payloadʳ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
|
||||||
|
with n ← n₁ ⊔ᵇ (n₂ ⊔ᵇ n₃)
|
||||||
|
using _⊔ⁿ_ ← FiniteHeightLattice._⊔_ (proj₂ (𝓛 n))
|
||||||
|
with n ≟ n₁ | n ≟ n₂ | n ≟ n₃
|
||||||
|
... | yes refl | yes refl | yes refl = l₁ ⊔ⁿ (l₂ ⊔ⁿ l₃)
|
||||||
|
... | yes refl | yes refl | no _ = l₁ ⊔ⁿ l₂
|
||||||
|
... | yes refl | no _ | yes refl = l₁ ⊔ⁿ l₃
|
||||||
|
... | yes refl | no _ | no _ = l₁
|
||||||
|
... | no _ | yes refl | yes refl = l₂ ⊔ⁿ l₃
|
||||||
|
... | no _ | yes refl | no _ = l₂
|
||||||
|
... | no _ | no _ | yes refl = l₃
|
||||||
|
... | no _ | no _ | no _ = FiniteHeightLattice.⊥ (proj₂ (𝓛 n))
|
||||||
|
|
||||||
filterᵉ : ∀ (n : Node) → Expr Elem → Maybe (Expr (proj₁ (𝓛 n)))
|
Reassocˡ : ∀ e₁ e₂ e₃ →
|
||||||
filterᵉ n (` (n' , l'))
|
((e₁ ⊔ e₂) ⊔ e₃) ≈ (proj₁ ((e₁ ⊔ e₂) ⊔ e₃) , payloadˡ e₁ e₂ e₃)
|
||||||
with n ≟ n'
|
Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
|
||||||
... | yes refl = just (` l')
|
with n ← (n₁ ⊔ᵇ n₂) ⊔ᵇ n₃ in pⁿ
|
||||||
... | no _ = nothing
|
with n ≟ n₁ | n ≟ n₂ | n ≟ n₃
|
||||||
filterᵉ n (e₁ ⊔ᵉ e₂)
|
Reassocˡ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃)
|
||||||
with filterᵉ n e₁ | filterᵉ n e₂
|
| yes refl | yes refl | yes refl
|
||||||
... | just e₁' | just e₂' = just (e₁' ⊔ᵉ e₂')
|
with (n₁ ⊔ᵇ n₁) ≟ n₁
|
||||||
... | just e₁' | nothing = just e₁'
|
... | no n₁≢n₁ = ⊥-elim (n₁≢n₁ (⊔ᵇ-idemp n₁))
|
||||||
... | nothing | just e₂' = just e₂'
|
... | yes p rewrite p
|
||||||
... | nothing | nothing = nothing
|
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 _
|
||||||
|
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 p₁@refl | no n₁≢n₂ | yes p₃@refl
|
||||||
|
using n₁⊔n₂≡n₁ ← trans (trans (trans (≡-⊔ᵇ-cong (sym (⊔ᵇ-idemp n₁)) (refl {x = n₂})) (⊔ᵇ-assoc n₁ n₁ n₂)) (⊔ᵇ-comm 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₃)
|
||||||
|
| yes p₁@refl | no n₁≢n₂ | no n₁≢n₃ = {!!}
|
||||||
|
|
||||||
Node-homo : ∀ e → proj₁ (eval _⊔_ e) ≡ eval _⊔ᵇ_ (mapᵉ proj₁ e)
|
Reassocʳ : ∀ e₁ e₂ e₃ →
|
||||||
Node-homo (` _) = refl
|
(e₁ ⊔ (e₂ ⊔ e₃)) ≈ (proj₁ (e₁ ⊔ (e₂ ⊔ e₃)) , payloadʳ e₁ e₂ e₃)
|
||||||
Node-homo (e₁ ⊔ᵉ e₂)
|
Reassocʳ (n₁ , l₁) (n₂ , l₂) (n₃ , l₃) = {!!}
|
||||||
with IH₁ ← Node-homo e₁ with IH₂ ← Node-homo e₂
|
|
||||||
with (n₁ , l₁) ← eval _⊔_ e₁ with (n₂ , l₂) ← eval _⊔_ e₂
|
|
||||||
with n ← n₁ ⊔ᵇ n₂ in p
|
|
||||||
with n ≟ n₁ | n ≟ n₂
|
|
||||||
... | yes refl | yes refl rewrite sym IH₁ rewrite sym IH₂ = sym (⊔ᵇ-idemp n)
|
|
||||||
... | yes refl | no _ rewrite sym IH₁ rewrite sym IH₂ = sym p
|
|
||||||
... | no _ | yes refl rewrite sym IH₁ rewrite sym IH₂ = sym p
|
|
||||||
... | no _ | no _ rewrite sym IH₁ rewrite sym IH₂ = sym p
|
|
||||||
|
|
||||||
-- A key simplifying property is that notionally, only the
|
|
||||||
-- "elements with the final tag" in the expression matter. All
|
|
||||||
-- others are subsumed. If none of the elments have the final tag,
|
|
||||||
-- we've found a better supremum and the second element will be ⊥.
|
|
||||||
Expr-final : ∀ e → let n = proj₁ (eval _⊔_ e)
|
|
||||||
⊥ⁿ = FiniteHeightLattice.⊥ (proj₂ (𝓛 n))
|
|
||||||
_⊔ⁿ_ = FiniteHeightLattice._⊔_ (proj₂ (𝓛 n))
|
|
||||||
in (eval _⊔_ e) ≈ (n , Maybe.maybe′ (eval _⊔ⁿ_) ⊥ⁿ (filterᵉ n e))
|
|
||||||
Expr-final = {!!}
|
|
||||||
|
|
||||||
⊔-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₃)
|
||||||
using exprˡ ← (((` e₁) ⊔ᵉ (` e₂)) ⊔ᵉ (` e₃))
|
with nˡ ← proj₁ ((e₁ ⊔ e₂) ⊔ e₃) in pˡ
|
||||||
using exprʳ ← ((` e₁) ⊔ᵉ ((` e₂) ⊔ᵉ (` e₃)))
|
with nʳ ← proj₁ (e₁ ⊔ (e₂ ⊔ e₃)) in pʳ
|
||||||
with nˡ ← proj₁ (eval _⊔_ exprˡ) in pˡ
|
with final₁ ← Reassocˡ e₁ e₂ e₃
|
||||||
with nʳ ← proj₁ (eval _⊔_ exprʳ) in pʳ
|
with final₂ ← Reassocʳ e₁ e₂ e₃
|
||||||
with final₁ ← Expr-final exprˡ
|
|
||||||
with final₂ ← Expr-final exprʳ
|
|
||||||
rewrite pˡ rewrite pʳ
|
rewrite pˡ rewrite pʳ
|
||||||
rewrite ⊔ᵇ-assoc n₁ n₂ n₃
|
rewrite ⊔ᵇ-assoc n₁ n₂ n₃
|
||||||
rewrite trans (sym pˡ ) pʳ
|
rewrite trans (sym pˡ ) pʳ
|
||||||
|
|||||||
Reference in New Issue
Block a user