Make progress on properties of the dependent product
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
@@ -237,13 +237,16 @@ record IsFiniteHeightLattice {a} (A : Set a)
|
|||||||
field
|
field
|
||||||
{{fixedHeight}} : FixedHeight h
|
{{fixedHeight}} : FixedHeight h
|
||||||
|
|
||||||
|
private
|
||||||
|
module MyChain = Chain _≈_ ≈-equiv _≺_ ≺-cong
|
||||||
|
|
||||||
|
open MyChain.Height fixedHeight using (⊥; ⊤) public
|
||||||
|
|
||||||
-- If the equality is decidable, we can prove that the top and bottom
|
-- If the equality is decidable, we can prove that the top and bottom
|
||||||
-- elements of the chain are least and greatest elements of the lattice
|
-- elements of the chain are least and greatest elements of the lattice
|
||||||
module _ {{≈-Decidable : IsDecidable _≈_}} where
|
module _ {{≈-Decidable : IsDecidable _≈_}} where
|
||||||
open IsDecidable ≈-Decidable using () renaming (R-dec to ≈-dec)
|
open IsDecidable ≈-Decidable using () renaming (R-dec to ≈-dec)
|
||||||
|
|
||||||
module MyChain = Chain _≈_ ≈-equiv _≺_ ≺-cong
|
|
||||||
open MyChain.Height fixedHeight using (⊥; ⊤) public
|
|
||||||
open MyChain.Height fixedHeight using (bounded; longestChain)
|
open MyChain.Height fixedHeight using (bounded; longestChain)
|
||||||
|
|
||||||
⊥≼ : ∀ (a : A) → ⊥ ≼ a
|
⊥≼ : ∀ (a : A) → ⊥ ≼ a
|
||||||
|
|||||||
@@ -456,7 +456,7 @@ record Graph : Set where
|
|||||||
Total-⊓? : Dec Total-⊓
|
Total-⊓? : Dec Total-⊓
|
||||||
Total-⊓? = P-Total? Have-⊓?
|
Total-⊓? = P-Total? Have-⊓?
|
||||||
|
|
||||||
module AssumeWellFormed (noCycles : NoCycles) (total-⊔ : Total-⊔) (total-⊓ : Total-⊓) where
|
module Basic (noCycles : NoCycles) (total-⊔ : Total-⊔) (total-⊓ : Total-⊓) where
|
||||||
n₁→n₂×n₂→n₁⇒n₁≡n₂ : ∀ {n₁ n₂} → PathExists n₁ n₂ → PathExists n₂ n₁ → n₁ ≡ n₂
|
n₁→n₂×n₂→n₁⇒n₁≡n₂ : ∀ {n₁ n₂} → PathExists n₁ n₂ → PathExists n₂ n₁ → n₁ ≡ n₂
|
||||||
n₁→n₂×n₂→n₁⇒n₁≡n₂ n₁→n₂ n₂→n₁
|
n₁→n₂×n₂→n₁⇒n₁≡n₂ n₁→n₂ n₂→n₁
|
||||||
with n₁→n₂ | n₂→n₁ | noCycles (n₁→n₂ ++ n₂→n₁)
|
with n₁→n₂ | n₂→n₁ | noCycles (n₁→n₂ ++ n₂→n₁)
|
||||||
@@ -606,3 +606,119 @@ record Graph : Set where
|
|||||||
{ absorb-⊔-⊓ = absorb-⊔-⊓
|
{ absorb-⊔-⊓ = absorb-⊔-⊓
|
||||||
; absorb-⊓-⊔ = absorb-⊓-⊔
|
; absorb-⊓-⊔ = absorb-⊓-⊔
|
||||||
}
|
}
|
||||||
|
|
||||||
|
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)
|
||||||
|
|
||||||
|
Elem : Set
|
||||||
|
Elem = Σ Node λ n → (proj₁ (𝓛 n))
|
||||||
|
|
||||||
|
data _≈_ : Elem → Elem → Set where
|
||||||
|
≈-lift : ∀ {n : Node} {l₁ l₂ : proj₁ (𝓛 n)} →
|
||||||
|
FiniteHeightLattice._≈_ (proj₂ (𝓛 n)) l₁ l₂ →
|
||||||
|
(n , l₁) ≈ (n , l₂)
|
||||||
|
|
||||||
|
≈-refl : ∀ {e : Elem} → e ≈ e
|
||||||
|
≈-refl {n , l} = ≈-lift (FiniteHeightLattice.≈-refl (proj₂ (𝓛 n)))
|
||||||
|
|
||||||
|
≈-sym : ∀ {e₁ e₂ : Elem} → e₁ ≈ e₂ → e₂ ≈ e₁
|
||||||
|
≈-sym {n₁ , l₁} (≈-lift l₁≈l₂) = ≈-lift (FiniteHeightLattice.≈-sym (proj₂ (𝓛 n₁)) l₁≈l₂)
|
||||||
|
|
||||||
|
≈-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₃)
|
||||||
|
|
||||||
|
_⊔_ : Elem → Elem → Elem
|
||||||
|
_⊔_ e₁ e₂
|
||||||
|
using n₁ ← proj₁ e₁ using n₂ ← proj₁ e₂
|
||||||
|
with n' ← n₁ ⊔ᵇ n₂
|
||||||
|
with n' ≟ n₁ | n' ≟ n₂
|
||||||
|
... | yes refl | yes refl = (n' , FiniteHeightLattice._⊔_ (proj₂ (𝓛 n')) (proj₂ e₁) (proj₂ e₂))
|
||||||
|
... | yes refl | _ = (n' , proj₂ e₁)
|
||||||
|
... | _ | yes refl = (n' , proj₂ e₂)
|
||||||
|
... | no _ | no _ = (n' , FiniteHeightLattice.⊥ (proj₂ (𝓛 n')))
|
||||||
|
|
||||||
|
⊔-idemp : ∀ e → (e ⊔ e) ≈ e
|
||||||
|
⊔-idemp (n , l) rewrite ⊔ᵇ-idemp n
|
||||||
|
with n ≟ n
|
||||||
|
... | yes refl = ≈-lift (FiniteHeightLattice.⊔-idemp (proj₂ (𝓛 n)) l)
|
||||||
|
... | no n≢n = ⊥-elim (n≢n refl)
|
||||||
|
|
||||||
|
⊔-comm : ∀ (e₁ e₂ : Elem) → (e₁ ⊔ e₂) ≈ (e₂ ⊔ e₁)
|
||||||
|
⊔-comm (n₁ , l₁) (n₂ , l₂)
|
||||||
|
rewrite ⊔ᵇ-comm n₁ n₂
|
||||||
|
with n ← n₂ ⊔ᵇ n₁
|
||||||
|
with n ≟ n₁ | n ≟ n₂
|
||||||
|
... | yes refl | yes refl = ≈-lift (FiniteHeightLattice.⊔-comm (proj₂ (𝓛 n)) l₁ l₂)
|
||||||
|
... | no _ | yes refl = ≈-lift (FiniteHeightLattice.≈-refl (proj₂ (𝓛 n)))
|
||||||
|
... | yes refl | no _ = ≈-lift (FiniteHeightLattice.≈-refl (proj₂ (𝓛 n)))
|
||||||
|
... | no _ | no _ = ≈-lift (FiniteHeightLattice.≈-refl (proj₂ (𝓛 n)))
|
||||||
|
|
||||||
|
private
|
||||||
|
data Expr (A : Set) : Set where
|
||||||
|
`_ : A → Expr A
|
||||||
|
_⊔ᵉ_ : Expr A → Expr A → Expr A
|
||||||
|
|
||||||
|
eval : ∀ {A} → (A → A → A) → Expr A → A
|
||||||
|
eval _ (` v) = v
|
||||||
|
eval f (e₁ ⊔ᵉ e₂) = f (eval f e₁) (eval f e₂)
|
||||||
|
|
||||||
|
mapᵉ : ∀ {A B} → (A → B) → Expr A → Expr B
|
||||||
|
mapᵉ f (` a) = ` (f a)
|
||||||
|
mapᵉ f (e₁ ⊔ᵉ e₂) = (mapᵉ f e₁) ⊔ᵉ (mapᵉ f e₂)
|
||||||
|
|
||||||
|
filterᵉ : ∀ (n : Node) → Expr Elem → Maybe (Expr (proj₁ (𝓛 n)))
|
||||||
|
filterᵉ n (` (n' , l'))
|
||||||
|
with n ≟ n'
|
||||||
|
... | yes refl = just (` l')
|
||||||
|
... | no _ = nothing
|
||||||
|
filterᵉ n (e₁ ⊔ᵉ e₂)
|
||||||
|
with filterᵉ n e₁ | filterᵉ n e₂
|
||||||
|
... | just e₁' | just e₂' = just (e₁' ⊔ᵉ e₂')
|
||||||
|
... | just e₁' | nothing = just e₁'
|
||||||
|
... | nothing | just e₂' = just e₂'
|
||||||
|
... | nothing | nothing = nothing
|
||||||
|
|
||||||
|
Node-homo : ∀ e → proj₁ (eval _⊔_ e) ≡ eval _⊔ᵇ_ (mapᵉ proj₁ e)
|
||||||
|
Node-homo (` _) = refl
|
||||||
|
Node-homo (e₁ ⊔ᵉ e₂)
|
||||||
|
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 subsubed. 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 = eval _⊔ᵇ_ (mapᵉ proj₁ 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₁@(n₁ , l₁) e₂@(n₂ , l₂) e₃@(n₃ , l₃)
|
||||||
|
using exprˡ ← (((` e₁) ⊔ᵉ (` e₂)) ⊔ᵉ (` e₃))
|
||||||
|
using exprʳ ← ((` e₁) ⊔ᵉ ((` e₂) ⊔ᵉ (` e₃)))
|
||||||
|
with nˡ ← eval _⊔ᵇ_ (mapᵉ proj₁ exprˡ) in pˡ
|
||||||
|
with nʳ ← eval _⊔ᵇ_ (mapᵉ proj₁ exprʳ) in pʳ
|
||||||
|
with final₁ ← Expr-final exprˡ
|
||||||
|
with final₂ ← Expr-final exprʳ
|
||||||
|
rewrite pˡ rewrite pʳ
|
||||||
|
rewrite ⊔ᵇ-assoc n₁ n₂ n₃
|
||||||
|
rewrite trans (sym pˡ ) pʳ
|
||||||
|
with nʳ ≟ n₁ | nʳ ≟ n₂ | nʳ ≟ n₃
|
||||||
|
... | yes refl | yes refl | yes refl =
|
||||||
|
let l-assoc = FiniteHeightLattice.⊔-assoc (proj₂ (𝓛 n₁)) l₁ l₂ l₃
|
||||||
|
in ≈-trans final₁ (≈-trans (≈-lift l-assoc) (≈-sym final₂))
|
||||||
|
... | yes refl | yes refl | no _ = ≈-trans final₁ (≈-sym final₂)
|
||||||
|
... | yes refl | no _ | yes refl = ≈-trans final₁ (≈-sym final₂)
|
||||||
|
... | yes refl | no _ | no _ = ≈-trans final₁ (≈-sym final₂)
|
||||||
|
... | no _ | yes refl | yes refl = ≈-trans final₁ (≈-sym final₂)
|
||||||
|
... | no _ | yes refl | no _ = ≈-trans final₁ (≈-sym final₂)
|
||||||
|
... | no _ | no _ | yes refl = ≈-trans final₁ (≈-sym final₂)
|
||||||
|
... | no _ | no _ | no _ = ≈-trans final₁ (≈-sym final₂)
|
||||||
|
|||||||
Reference in New Issue
Block a user