Compare commits

..

No commits in common. "3d2a507f2ffabc096c08534d9a9a3826ee12c2a9" and "f0b0d51b488be7f4aab036bc8527ef4fd0734585" have entirely different histories.

14 changed files with 136 additions and 333 deletions

View File

@ -10,18 +10,16 @@ module Analysis.Forward
open import Data.Empty using (⊥-elim)
open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
open import Data.Nat using (suc)
open import Data.Product using (_×_; proj₁; proj₂; _,_)
open import Data.Sum using (inj₁; inj₂)
open import Data.Product using (_×_; proj₁; _,_)
open import Data.List using (List; _∷_; []; foldr; foldl; cartesianProduct; cartesianProductWith)
open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_)
open import Data.List.Relation.Unary.Any as Any using ()
open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong; sym; trans; subst)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Data.Unit using ()
open import Function using (_∘_; flip)
import Chain
open import Utils using (Pairwise; _⇒_; __)
open import Utils using (Pairwise; _⇒_)
import Lattice.FiniteValueMap
open IsFiniteHeightLattice isFiniteHeightLatticeˡ
@ -64,32 +62,25 @@ module WithProg (prog : Program) where
; ⊔-Monotonicʳ to ⊔ᵛ-Monotonicʳ
; ⊔-idemp to ⊔ᵛ-idemp
)
open Lattice.FiniteValueMap.IterProdIsomorphism _≟ˢ_ isLatticeˡ
using ()
renaming
( Provenance-union to Provenance-unionᵐ
)
open Lattice.FiniteValueMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟ˢ_ isLatticeˡ vars-Unique ≈ˡ-dec _ fixedHeightˡ
using ()
renaming
( isFiniteHeightLattice to isFiniteHeightLatticeᵛ
; ⊥-contains-bottoms to ⊥ᵛ-contains-bottoms
)
≈ᵛ-dec = ≈ˡ-dec⇒≈ᵛ-dec ≈ˡ-dec
joinSemilatticeᵛ = IsFiniteHeightLattice.joinSemilattice isFiniteHeightLatticeᵛ
fixedHeightᵛ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵛ
⊥ᵛ = Chain.Height.⊥ fixedHeightᵛ
⊥ᵛ = proj₁ (proj₁ (proj₁ fixedHeightᵛ))
-- Finally, the map we care about is (state -> (variables -> value)). Bring that in.
module StateVariablesFiniteMap = Lattice.FiniteValueMap.WithKeys _≟_ isLatticeᵛ states
open StateVariablesFiniteMap
using (_[_]; []-∈; m₁≼m₂⇒m₁[ks]≼m₂[ks]; m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂)
using (_[_]; m₁≼m₂⇒m₁[ks]≼m₂[ks])
renaming
( FiniteMap to StateVariables
; isLattice to isLatticeᵐ
; _≈_ to _≈ᵐ_
; _∈_ to _∈ᵐ_
; _∈k_ to _∈kᵐ_
; locate to locateᵐ
; _≼_ to _≼ᵐ_
@ -122,13 +113,8 @@ module WithProg (prog : Program) where
variablesAt : State StateVariables VariableValues
variablesAt s sv = proj₁ (locateᵐ {s} {sv} (states-in-Map s sv))
variablesAt-∈ : (s : State) (sv : StateVariables) (s , variablesAt s sv) ∈ᵐ sv
variablesAt-∈ s sv = proj₂ (locateᵐ {s} {sv} (states-in-Map s sv))
variablesAt-≈ : s sv₁ sv₂ sv₁ ≈ᵐ sv₂ variablesAt s sv₁ ≈ᵛ variablesAt s sv₂
variablesAt-≈ s sv₁ sv₂ sv₁≈sv₂ =
m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ sv₁ sv₂ sv₁≈sv₂
(states-in-Map s sv₁) (states-in-Map s sv₂)
variablesAt-≈ = {!!}
-- build up the 'join' function, which follows from Exercise 4.26's
--
@ -246,17 +232,11 @@ module WithProg (prog : Program) where
module WithInterpretation (latticeInterpretationˡ : LatticeInterpretation isLatticeˡ) where
open LatticeInterpretation latticeInterpretationˡ
using ()
renaming
( ⟦_⟧ to ⟦_⟧ˡ
; ⟦⟧-respects-≈ to ⟦⟧ˡ-respects-≈ˡ
; ⟦⟧-⊔- to ⟦⟧ˡ-⊔ˡ-
)
renaming (⟦_⟧ to ⟦_⟧ˡ; ⟦⟧-respects-≈ to ⟦⟧ˡ-respects-≈ˡ)
⟦_⟧ᵛ : VariableValues Env Set
⟦_⟧ᵛ vs ρ = {k l} (k , l) ∈ᵛ vs {v} (k , v) Language.∈ ρ l ⟧ˡ v
⟦⊥ᵛ⟧ᵛ∅ : ⊥ᵛ ⟧ᵛ []
⟦⊥ᵛ⟧ᵛ∅ _ ()
⟦⟧ᵛ-respects-≈ᵛ : {vs₁ vs₂ : VariableValues} vs₁ ≈ᵛ vs₂ vs₁ ⟧ᵛ vs₂ ⟧ᵛ
⟦⟧ᵛ-respects-≈ᵛ {m₁ , _} {m₂ , _}
@ -267,21 +247,9 @@ module WithProg (prog : Program) where
in
⟦⟧ˡ-respects-≈ˡ (≈ˡ-sym l≈l') v ⟦l'⟧v
⟦⟧ᵛ-⊔ᵛ- : {vs₁ vs₂ : VariableValues} ( vs₁ ⟧ᵛ vs₂ ⟧ᵛ) vs₁ ⊔ᵛ vs₂ ⟧ᵛ
⟦⟧ᵛ-⊔ᵛ- {vs₁} {vs₂} ρ ⟦vs₁⟧ρ⟦vs₂⟧ρ {k} {l} k,l∈vs₁₂ {v} k,v∈ρ
with ((l₁ , l₂) , (refl , (k,l₁∈vs₁ , k,l₂∈vs₂)))
Provenance-unionᵐ vs₁ vs₂ k,l∈vs₁₂
with ⟦vs₁⟧ρ⟦vs₂⟧ρ
... | inj₁ ⟦vs₁⟧ρ = ⟦⟧ˡ-⊔ˡ- {l₁} {l₂} v (inj₁ (⟦vs₁⟧ρ k,l₁∈vs₁ k,v∈ρ))
... | inj₂ ⟦vs₂⟧ρ = ⟦⟧ˡ-⊔ˡ- {l₁} {l₂} v (inj₂ (⟦vs₂⟧ρ k,l₂∈vs₂ k,v∈ρ))
⟦⟧ᵛ-foldr : {vs : VariableValues} {vss : List VariableValues} {ρ : Env}
vs ⟧ᵛ ρ vs ∈ˡ vss foldr _⊔ᵛ_ ⊥ᵛ vss ⟧ᵛ ρ
⟦⟧ᵛ-foldr {vs} {vs vss'} {ρ = ρ} ⟦vs⟧ρ (Any.here refl) =
⟦⟧ᵛ-⊔ᵛ- {vs₁ = vs} {vs₂ = foldr _⊔ᵛ_ ⊥ᵛ vss'} ρ (inj₁ ⟦vs⟧ρ)
⟦⟧ᵛ-foldr {vs} {vs' vss'} {ρ = ρ} ⟦vs⟧ρ (Any.there vs∈vss') =
⟦⟧ᵛ-⊔ᵛ- {vs₁ = vs'} {vs₂ = foldr _⊔ᵛ_ ⊥ᵛ vss'} ρ
(inj₂ (⟦⟧ᵛ-foldr ⟦vs⟧ρ vs∈vss'))
⟦⟧ᵛ-foldr = {!!}
InterpretationValid : Set
InterpretationValid = {vs ρ e v} ρ , e ⇒ᵉ v vs ⟧ᵛ ρ eval e vs ⟧ˡ v
@ -307,17 +275,13 @@ module WithProg (prog : Program) where
updateVariablesFromStmt-fold-matches : {bss vs ρ₁ ρ₂} ρ₁ , bss ⇒ᵇˢ ρ₂ vs ⟧ᵛ ρ₁ foldl (flip updateVariablesFromStmt) vs bss ⟧ᵛ ρ₂
updateVariablesFromStmt-fold-matches [] ⟦vs⟧ρ = ⟦vs⟧ρ
updateVariablesFromStmt-fold-matches {bs bss'} {vs} {ρ₁} {ρ₂} (ρ₁,bs⇒ρ ρ,bss'⇒ρ₂) ⟦vs⟧ρ =
updateVariablesFromStmt-fold-matches
{bss'} {updateVariablesFromStmt bs vs} ρ,bss'⇒ρ₂
(updateVariablesFromStmt-matches ρ₁,bs⇒ρ ⟦vs⟧ρ)
updateVariablesFromStmt-fold-matches {bss'} {updateVariablesFromStmt bs vs} ρ,bss'⇒ρ₂ (updateVariablesFromStmt-matches ρ₁,bs⇒ρ ⟦vs⟧ρ)
updateVariablesForState-matches : {s sv ρ₁ ρ₂} ρ₁ , (code s) ⇒ᵇˢ ρ₂ variablesAt s sv ⟧ᵛ ρ₁ updateVariablesForState s sv ⟧ᵛ ρ₂
updateVariablesForState-matches =
updateVariablesFromStmt-fold-matches
updateVariablesForState-matches = updateVariablesFromStmt-fold-matches
updateAll-matches : {s sv ρ₁ ρ₂} ρ₁ , (code s) ⇒ᵇˢ ρ₂ variablesAt s sv ⟧ᵛ ρ₁ variablesAt s (updateAll sv) ⟧ᵛ ρ₂
updateAll-matches {s} {sv} ρ₁,bss⇒ρ ⟦vs⟧ρ
rewrite variablesAt-updateAll s sv =
updateAll-matches {s} {sv} ρ₁,bss⇒ρ ⟦vs⟧ρ rewrite variablesAt-updateAll s sv =
updateVariablesForState-matches {s} {sv} ρ₁,bss⇒ρ ⟦vs⟧ρ
@ -325,44 +289,12 @@ module WithProg (prog : Program) where
stepTrace {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ ρ₁,bss⇒ρ =
let
-- I'd use rewrite, but Agda gets a memory overflow (?!).
⟦joinAll-result⟧ρ =
subst (λ vs vs ⟧ᵛ ρ₁)
(sym (variablesAt-joinAll s₁ result))
⟦joinForKey-s₁⟧ρ
⟦analyze-result⟧ρ =
updateAll-matches {sv = joinAll result}
ρ₁,bss⇒ρ ⟦joinAll-result⟧ρ
analyze-result≈result =
≈ᵐ-sym {result} {updateAll (joinAll result)}
result≈analyze-result
analyze-s₁≈s₁ =
variablesAt-≈ s₁ (updateAll (joinAll result))
result (analyze-result≈result)
⟦joinAll-result⟧ρ = subst (λ vs vs ⟧ᵛ ρ₁) (sym (variablesAt-joinAll s₁ result)) ⟦joinForKey-s₁⟧ρ
⟦analyze-result⟧ρ = updateAll-matches {sv = joinAll result} ρ₁,bss⇒ρ ⟦joinAll-result⟧ρ
analyze-result≈result = ≈ᵐ-sym {result} {updateAll (joinAll result)} result≈analyze-result
analyze-s₁≈s₁ = variablesAt-≈ s₁ (updateAll (joinAll result)) result (analyze-result≈result)
in
⟦⟧ᵛ-respects-≈ᵛ {variablesAt s₁ (updateAll (joinAll result))} {variablesAt s₁ result} (analyze-s₁≈s₁) ρ₂ ⟦analyze-result⟧ρ
walkTrace : {s₁ s₂ ρ₁ ρ₂} joinForKey s₁ result ⟧ᵛ ρ₁ Trace {graph} s₁ s₂ ρ₁ ρ₂ variablesAt s₂ result ⟧ᵛ ρ₂
walkTrace {s₁} {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ (Trace-single ρ₁,bss⇒ρ) =
stepTrace {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ ρ₁,bss⇒ρ
walkTrace {s₁} {s₂} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ (Trace-edge {ρ₂ = ρ} {idx₂ = s} ρ₁,bss⇒ρ s₁→s₂ tr) =
let
⟦result-s₁⟧ρ =
stepTrace {s₁} {ρ₁} {ρ} ⟦joinForKey-s₁⟧ρ ρ₁,bss⇒ρ
s₁∈incomingStates =
[]-∈ result (edge⇒incoming s₁→s₂)
(variablesAt-∈ s₁ result)
⟦joinForKey-s⟧ρ =
⟦⟧ᵛ-foldr ⟦result-s₁⟧ρ s₁∈incomingStates
in
walkTrace ⟦joinForKey-s⟧ρ tr
postulate initialState-pred-∅ : incoming initialState []
joinForKey-initialState-⊥ᵛ : joinForKey initialState result ⊥ᵛ
joinForKey-initialState-⊥ᵛ = cong (λ ins foldr _⊔ᵛ_ ⊥ᵛ (result [ ins ])) initialState-pred-∅
⟦joinAll-initialState⟧ᵛ∅ : joinForKey initialState result ⟧ᵛ []
⟦joinAll-initialState⟧ᵛ∅ = subst (λ vs vs ⟧ᵛ []) (sym joinForKey-initialState-⊥ᵛ) ⟦⊥ᵛ⟧ᵛ∅
analyze-correct : {ρ : Env} [] , rootStmt ⇒ˢ ρ variablesAt finalState result ⟧ᵛ ρ
analyze-correct {ρ} ∅,s⇒ρ = walkTrace {initialState} {finalState} {[]} {ρ} ⟦joinAll-initialState⟧ᵛ∅ (trace ∅,s⇒ρ)
walkTrace {s₁} {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ (Trace-single ρ₁,bss⇒ρ) = stepTrace {s₁} {ρ₁} {ρ₂} ⟦joinForKey-s₁⟧ρ ρ₁,bss⇒ρ

View File

@ -10,7 +10,7 @@ open import Data.Nat using (; suc; _+_; _≤_)
open import Data.Nat.Properties using (+-comm; m+1+n≰m)
open import Data.Product using (_×_; Σ; _,_)
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl)
open import Data.Empty as Empty using ()
open import Data.Empty using ()
open IsEquivalence ≈-equiv
@ -38,16 +38,11 @@ module _ where
Bounded : Set a
Bounded bound = {a₁ a₂ : A} {n : } Chain a₁ a₂ n n bound
Bounded-suc-n : {a₁ a₂ : A} {n : } Bounded n Chain a₁ a₂ (suc n) Empty.
Bounded-suc-n : {a₁ a₂ : A} {n : } Bounded n Chain a₁ a₂ (suc n)
Bounded-suc-n {a₁} {a₂} {n} bounded c = (m+1+n≰m n n+1≤n)
where
n+1≤n : n + 1 n
n+1≤n rewrite (+-comm n 1) = bounded c
record Height (height : ) : Set a where
field
: A
: A
longestChain : Chain height
bounded : Bounded height
Height : Set a
Height height = (Σ (A × A) (λ (a₁ , a₂) Chain a₁ a₂ height) × Bounded height)

View File

@ -23,21 +23,15 @@ import Chain
module ChainA = Chain _≈_ ≈-equiv _≺_ ≺-cong
private
open ChainA.Height fixedHeight
using ()
renaming
( to ⊥ᴬ
; longestChain to longestChainᴬ
; bounded to boundedᴬ
)
⊥ᴬ : A
⊥ᴬ = proj₁ (proj₁ (proj₁ fixedHeight))
⊥ᴬ≼ : (a : A) ⊥ᴬ a
⊥ᴬ≼ a with ≈-dec a ⊥ᴬ
... | yes a≈⊥ᴬ = ≼-cong a≈⊥ᴬ ≈-refl (≼-refl a)
... | no a̷≈⊥ᴬ with ≈-dec ⊥ᴬ (a ⊥ᴬ)
... | yes ⊥ᴬ≈a⊓⊥ᴬ = ≈-trans (⊔-comm ⊥ᴬ a) (≈-trans (≈-⊔-cong (≈-refl {a}) ⊥ᴬ≈a⊓⊥ᴬ) (absorb-⊔-⊓ a ⊥ᴬ))
... | no ⊥ᴬ̷≈a⊓⊥ᴬ = ⊥-elim (ChainA.Bounded-suc-n boundedᴬ (ChainA.step x≺⊥ᴬ ≈-refl longestChainᴬ))
... | no ⊥ᴬ̷≈a⊓⊥ᴬ = ⊥-elim (ChainA.Bounded-suc-n (proj₂ fixedHeight) (ChainA.step x≺⊥ᴬ ≈-refl (proj₂ (proj₁ fixedHeight))))
where
⊥ᴬ⊓a̷≈⊥ᴬ : ¬ (⊥ᴬ a) ⊥ᴬ
⊥ᴬ⊓a̷≈⊥ᴬ = λ ⊥ᴬ⊓a≈⊥ᴬ ⊥ᴬ̷≈a⊓⊥ᴬ (≈-trans (≈-sym ⊥ᴬ⊓a≈⊥ᴬ) (⊓-comm _ _))
@ -51,7 +45,7 @@ private
-- out, we have exceeded h steps, which shouldn't be possible.
doStep : (g hᶜ : ) (a₁ a₂ : A) (c : ChainA.Chain a₁ a₂ hᶜ) (g+hᶜ≡h : g + hᶜ suc h) (a₂≼fa₂ : a₂ f a₂) Σ A (λ a a f a)
doStep 0 hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite g+hᶜ≡sh = ⊥-elim (ChainA.Bounded-suc-n boundedᴬ c)
doStep 0 hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite g+hᶜ≡sh = ⊥-elim (ChainA.Bounded-suc-n (proj₂ fixedHeight) c)
doStep (suc g') hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite sym (+-suc g' hᶜ)
with ≈-dec a₂ (f a₂)
... | yes a₂≈fa₂ = (a₂ , a₂≈fa₂)
@ -77,7 +71,7 @@ private
(c : ChainA.Chain a₁ a₂ hᶜ) (g+hᶜ≡h : g + hᶜ suc h)
(a₂≼fa₂ : a₂ f a₂)
proj₁ (doStep g hᶜ a₁ a₂ c g+hᶜ≡h a₂≼fa₂) a
stepPreservesLess 0 _ _ _ _ _ _ c g+hᶜ≡sh _ rewrite g+hᶜ≡sh = ⊥-elim (ChainA.Bounded-suc-n boundedᴬ c)
stepPreservesLess 0 _ _ _ _ _ _ c g+hᶜ≡sh _ rewrite g+hᶜ≡sh = ⊥-elim (ChainA.Bounded-suc-n (proj₂ fixedHeight) c)
stepPreservesLess (suc g') hᶜ a₁ a₂ a a≈fa a₂≼a c g+hᶜ≡sh a₂≼fa₂ rewrite sym (+-suc g' hᶜ)
with ≈-dec a₂ (f a₂)
... | yes _ = a₂≼a

View File

@ -38,9 +38,8 @@ module TransportFiniteHeight
open IsEquivalence ≈₁-equiv using () renaming (≈-sym to ≈₁-sym; ≈-trans to ≈₁-trans)
open IsEquivalence ≈₂-equiv using () renaming (≈-sym to ≈₂-sym; ≈-trans to ≈₂-trans)
import Chain
open Chain _≈₁_ ≈₁-equiv _≺₁_ ≺₁-cong using () renaming (Chain to Chain₁; done to done₁; step to step₁)
open Chain _≈₂_ ≈₂-equiv _≺₂_ ≺₂-cong using () renaming (Chain to Chain₂; done to done₂; step to step₂)
open import Chain _≈₁_ ≈₁-equiv _≺₁_ ≺₁-cong using () renaming (Chain to Chain₁; done to done₁; step to step₁)
open import Chain _≈₂_ ≈₂-equiv _≺₂_ ≺₂-cong using () renaming (Chain to Chain₂; done to done₂; step to step₂)
private
f-Injective : Injective _≈₁_ _≈₂_ f
@ -66,17 +65,10 @@ module TransportFiniteHeight
isFiniteHeightLattice : IsFiniteHeightLattice B height _≈₂_ _⊔₂_ _⊓₂_
isFiniteHeightLattice =
let
open Chain.Height (IsFiniteHeightLattice.fixedHeight fhlA)
using ()
renaming ( to ⊥₁; to ⊤₁; bounded to bounded₁; longestChain to c)
(((a₁ , a₂) , c) , bounded₁) = IsFiniteHeightLattice.fixedHeight fhlA
in record
{ isLattice = lB
; fixedHeight = record
{ = f ⊥₁
; = f ⊤₁
; longestChain = portChain₁ c
; bounded = λ c' bounded₁ (portChain₂ c')
}
; fixedHeight = (((f a₁ , f a₂), portChain₁ c) , λ c' bounded₁ (portChain₂ c'))
}
finiteHeightLattice : FiniteHeightLattice B

View File

@ -10,7 +10,7 @@ open import Data.Fin using (Fin; suc; zero)
open import Data.Fin.Properties as FinProp using (suc-injective)
open import Data.List as List using (List; []; _∷_)
open import Data.List.Membership.Propositional as ListMem using ()
open import Data.List.Membership.Propositional.Properties as ListMemProp using (∈-filter⁺)
open import Data.List.Relation.Unary.All using (All; []; _∷_)
open import Data.List.Relation.Unary.Any as RelAny using ()
open import Data.Nat using (; suc)
open import Data.Product using (_,_; Σ; proj₁; proj₂)
@ -27,26 +27,43 @@ open import Lattice.MapSet _≟ˢ_ using ()
; to-List to to-Listˢ
)
private
z≢sf : {n : } (f : Fin n) ¬ (zero suc f)
z≢sf f ()
z≢mapsfs : {n : } (fs : List (Fin n)) All (λ sf ¬ zero sf) (List.map suc fs)
z≢mapsfs [] = []
z≢mapsfs (f fs') = z≢sf f z≢mapsfs fs'
indices : (n : ) Σ (List (Fin n)) Unique
indices 0 = ([] , Utils.empty)
indices (suc n') =
let
(inds' , unids') = indices n'
in
( zero List.map suc inds'
, push (z≢mapsfs inds') (Unique-map suc suc-injective unids')
)
indices-complete : (n : ) (f : Fin n) f ListMem.∈ (proj₁ (indices n))
indices-complete (suc n') zero = RelAny.here refl
indices-complete (suc n') (suc f') = RelAny.there (x∈xs⇒fx∈fxs suc (indices-complete n' f'))
record Program : Set where
field
rootStmt : Stmt
graph : Graph
graph = wrap (buildCfg rootStmt)
graph = buildCfg rootStmt
State : Set
State = Graph.Index graph
initialState : State
initialState = proj₁ (wrap-input (buildCfg rootStmt))
initialState = proj₁ (buildCfg-input rootStmt)
finalState : State
finalState = proj₁ (wrap-output (buildCfg rootStmt))
trace : {ρ : Env} [] , rootStmt ⇒ˢ ρ Trace {graph} initialState finalState [] ρ
trace {ρ} ∅,s⇒ρ
with MkEndToEndTrace idx₁ (RelAny.here refl) idx₂ (RelAny.here refl) tr
EndToEndTrace-wrap (buildCfg-sufficient ∅,s⇒ρ) = tr
finalState = proj₁ (buildCfg-output rootStmt)
private
vars-Set : StringSet
@ -59,13 +76,13 @@ record Program : Set where
vars-Unique = proj₂ vars-Set
states : List State
states = indices graph
states = proj₁ (indices (Graph.size graph))
states-complete : (s : State) s ListMem.∈ states
states-complete = indices-complete graph
states-complete = indices-complete (Graph.size graph)
states-Unique : Unique states
states-Unique = indices-Unique graph
states-Unique = proj₂ (indices (Graph.size graph))
code : State List BasicStmt
code st = graph [ st ]
@ -82,10 +99,4 @@ record Program : Set where
open import Data.List.Membership.DecPropositional _≟ᵉ_ using (_∈?_)
incoming : State List State
incoming = predecessors graph
edge⇒incoming : {s₁ s₂ : State} (s₁ , s₂) ListMem.∈ (Graph.edges graph)
s₁ ListMem.∈ (incoming s₂)
edge⇒incoming {s₁} {s₂} s₁,s₂∈es =
∈-filter⁺ (λ s' (s' , s₂) ∈? (Graph.edges graph))
(states-complete s₁) s₁,s₂∈es
incoming idx = List.filter (λ idx' (idx' , idx) ∈? (Graph.edges graph)) states

View File

@ -7,19 +7,15 @@ open import Data.Fin.Properties as FinProp using (suc-injective)
open import Data.List as List using (List; []; _∷_)
open import Data.List.Membership.Propositional as ListMem using ()
open import Data.List.Membership.Propositional.Properties as ListMemProp using ()
open import Data.List.Relation.Unary.All using (All; []; _∷_)
open import Data.List.Relation.Unary.Any as RelAny using ()
open import Data.Nat as Nat using (; suc)
open import Data.Nat.Properties using (+-assoc; +-comm)
open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
open import Data.Product.Properties as ProdProp using ()
open import Data.Product using (_×_; Σ; _,_)
open import Data.Vec using (Vec; []; _∷_; lookup; cast; _++_)
open import Data.Vec.Properties using (cast-is-id; ++-assoc; lookup-++ˡ; cast-sym; ++-identityʳ; lookup-++ʳ)
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; refl; subst; trans)
open import Relation.Nullary using (¬_)
open import Lattice
open import Utils using (Unique; push; Unique-map; x∈xs⇒fx∈fxs; ∈-cartesianProduct)
open import Utils using (x∈xs⇒fx∈fxs; ∈-cartesianProduct)
record Graph : Set where
constructor MkGraph
@ -116,48 +112,8 @@ singleton bss = record
; outputs = zero []
}
wrap : Graph Graph
wrap g = singleton [] g singleton []
buildCfg : Stmt Graph
buildCfg bs₁ = singleton (bs₁ [])
buildCfg (s₁ then s₂) = buildCfg s₁ buildCfg s₂
buildCfg (if _ then s₁ else s₂) = singleton [] (buildCfg s₁ buildCfg s₂) singleton []
buildCfg (while _ repeat s) = loop (buildCfg s)
private
z≢sf : {n : } (f : Fin n) ¬ (zero suc f)
z≢sf f ()
z≢mapsfs : {n : } (fs : List (Fin n)) All (λ sf ¬ zero sf) (List.map suc fs)
z≢mapsfs [] = []
z≢mapsfs (f fs') = z≢sf f z≢mapsfs fs'
finValues : (n : ) Σ (List (Fin n)) Unique
finValues 0 = ([] , Utils.empty)
finValues (suc n') =
let
(inds' , unids') = finValues n'
in
( zero List.map suc inds'
, push (z≢mapsfs inds') (Unique-map suc suc-injective unids')
)
finValues-complete : (n : ) (f : Fin n) f ListMem.∈ (proj₁ (finValues n))
finValues-complete (suc n') zero = RelAny.here refl
finValues-complete (suc n') (suc f') = RelAny.there (x∈xs⇒fx∈fxs suc (finValues-complete n' f'))
module _ (g : Graph) where
open import Data.List.Membership.DecPropositional (ProdProp.≡-dec (FinProp._≟_ {Graph.size g}) (FinProp._≟_ {Graph.size g})) using (_∈?_)
indices : List (Graph.Index g)
indices = proj₁ (finValues (Graph.size g))
indices-complete : (idx : (Graph.Index g)) idx ListMem.∈ indices
indices-complete = finValues-complete (Graph.size g)
indices-Unique : Unique indices
indices-Unique = proj₂ (finValues (Graph.size g))
predecessors : (Graph.Index g) List (Graph.Index g)
predecessors idx = List.filter (λ idx' (idx' , idx) ∈? (Graph.edges g)) indices

View File

@ -18,11 +18,22 @@ open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym)
open import Utils using (x∈xs⇒fx∈fxs; ∈-cartesianProduct; concat-∈)
wrap-input : (g : Graph) Σ (Graph.Index (wrap g)) (λ idx Graph.inputs (wrap g) idx [])
wrap-input g = (_ , refl)
wrap-output : (g : Graph) Σ (Graph.Index (wrap g)) (λ idx Graph.outputs (wrap g) idx [])
wrap-output g = (_ , refl)
buildCfg-input : (s : Stmt) let g = buildCfg s in Σ (Graph.Index g) (λ idx Graph.inputs g idx [])
buildCfg-input bs₁ = (zero , refl)
buildCfg-input (s₁ then s₂)
with (idx , p) buildCfg-input s₁ rewrite p = (_ , refl)
buildCfg-input (if _ then s₁ else s₂) = (zero , refl)
buildCfg-input (while _ repeat s)
with (idx , p) buildCfg-input s rewrite p = (_ , refl)
buildCfg-output : (s : Stmt) let g = buildCfg s in Σ (Graph.Index g) (λ idx Graph.outputs g idx [])
buildCfg-output bs₁ = (zero , refl)
buildCfg-output (s₁ then s₂)
with (idx , p) buildCfg-output s₂ rewrite p = (_ , refl)
buildCfg-output (if _ then s₁ else s₂) = (_ , refl)
buildCfg-output (while _ repeat s)
with (idx , p) buildCfg-output s rewrite p = (_ , refl)
Trace-∙ˡ : {g₁ g₂ : Graph} {idx₁ idx₂ : Graph.Index g₁} {ρ₁ ρ₂ : Env}
Trace {g₁} idx₁ idx₂ ρ₁ ρ₂
@ -213,10 +224,6 @@ EndToEndTrace-singleton ρ₁⇒ρ₂ = record
EndToEndTrace-singleton[] : (ρ : Env) EndToEndTrace {singleton []} ρ ρ
EndToEndTrace-singleton[] env = EndToEndTrace-singleton []
EndToEndTrace-wrap : {g : Graph} {ρ₁ ρ₂ : Env}
EndToEndTrace {g} ρ₁ ρ₂ EndToEndTrace {wrap g} ρ₁ ρ₂
EndToEndTrace-wrap {g} {ρ₁} {ρ₂} etr = EndToEndTrace-singleton[] ρ₁ ++ etr ++ EndToEndTrace-singleton[] ρ₂
buildCfg-sufficient : {s : Stmt} {ρ₁ ρ₂ : Env} ρ₁ , s ⇒ˢ ρ₂
EndToEndTrace {buildCfg s} ρ₁ ρ₂
buildCfg-sufficient (⇒ˢ-⟨⟩ ρ₁ ρ₂ bs ρ₁,bs⇒ρ) =

View File

@ -355,12 +355,7 @@ module Plain (x : A) where
rewrite [x]≺y⇒y≡ _ _ [x]≺y with ≈-- y≈z = ⊥-elim (¬-Chain- c)
fixedHeight : IsLattice.FixedHeight isLattice 2
fixedHeight = record
{ =
; =
; longestChain = longestChain
; bounded = isLongest
}
fixedHeight = ((( , ) , longestChain) , isLongest)
isFiniteHeightLattice : IsFiniteHeightLattice AboveBelow 2 _≈_ _⊔_ _⊓_
isFiniteHeightLattice = record

View File

@ -30,9 +30,7 @@ open import Lattice.Map ≡-dec-A lB as Map
; absorb-⊓-⊔ to absorb-⊓ᵐ-⊔ᵐ
; ≈-dec to ≈ᵐ-dec
; _[_] to _[_]ᵐ
; []-∈ to []ᵐ-∈
; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ
; m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ to m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ᵐ
; locate to locateᵐ
; keys to keysᵐ
; _updating_via_ to _updatingᵐ_via_
@ -106,10 +104,6 @@ module WithKeys (ks : List A) where
_[_] : FiniteMap List A List B
_[_] (m₁ , _) ks = m₁ [ ks ]ᵐ
[]-∈ : {k : A} {v : B} {ks' : List A} (fm : FiniteMap)
k ∈ˡ ks' (k , v) fm v ∈ˡ (fm [ ks' ])
[]-∈ {k} {v} {ks'} (m , _) k∈ks' k,v∈fm = []ᵐ-∈ m k,v∈fm k∈ks'
≈-equiv : IsEquivalence FiniteMap _≈_
≈-equiv = record
{ ≈-refl =
@ -165,11 +159,6 @@ module WithKeys (ks : List A) where
fm₁ fm₂ (k , v₁) fm₁ (k , v₂) fm₂ v₁ ≼₂ v₂
m₁≼m₂⇒m₁[k]≼m₂[k] (m₁ , _) (m₂ , _) m₁≼m₂ k,v₁∈m₁ k,v₂∈m₂ = m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ m₁ m₂ m₁≼m₂ k,v₁∈m₁ k,v₂∈m₂
m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ : (fm₁ fm₂ : FiniteMap) {k : A}
fm₁ fm₂ (k∈kfm₁ : k ∈k fm₁) (k∈kfm₂ : k ∈k fm₂)
proj₁ (locate {fm = fm₁} k∈kfm₁) ≈₂ proj₁ (locate {fm = fm₂} k∈kfm₂)
m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ (m₁ , _) (m₂ , _) = m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ᵐ m₁ m₂
module GeneralizedUpdate
{l} {L : Set l}
{_≈ˡ_ : L L Set l} {_⊔ˡ_ : L L L} {_⊓ˡ_ : L L L}

View File

@ -28,7 +28,6 @@ open import Data.List.Relation.Unary.All using (All)
open import Data.List.Relation.Unary.Any using (Any; here; there)
open import Relation.Nullary using (¬_)
open import Isomorphism using (IsInverseˡ; IsInverseʳ)
open import Chain using (Height)
open import Lattice.Map ≡-dec-A lB
using
@ -105,14 +104,6 @@ module IterProdIsomorphism where
_∈ᵐ_ : {ks : List A} A × B FiniteMap ks Set
_∈ᵐ_ {ks} = _∈_ ks
to-build : {b : B} {ks : List A} (uks : Unique ks)
let fm = to uks (IP.build b tt (length ks))
in (k : A) (v : B) (k , v) ∈ᵐ fm v b
to-build {b} {k ks'} (push _ uks') k v (here refl) = refl
to-build {b} {k ks'} (push _ uks') k' v (there k',v∈m') =
to-build {ks = ks'} uks' k' v k',v∈m'
-- The left inverse is: from (to x) = x
from-to-inverseˡ : {ks : List A} (uks : Unique ks)
IsInverseˡ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {length ks})
@ -162,26 +153,6 @@ module IterProdIsomorphism where
fm'₂⊆fm'₁ k' v' k',v'∈fm'₂
in (v'' , (v'≈v'' , there k',v''∈fm'₁))
FromBothMaps : (k : A) (v : B) {ks : List A} (fm₁ fm₂ : FiniteMap ks) Set
FromBothMaps k v fm₁ fm₂ =
Σ (B × B)
(λ (v₁ , v₂) ( (v v₁ ⊔₂ v₂) × ((k , v₁) ∈ᵐ fm₁ × (k , v₂) ∈ᵐ fm₂)))
Provenance-union : {ks : List A} (fm₁ fm₂ : FiniteMap ks) {k : A} {v : B}
(k , v) ∈ᵐ (fm₁ ⊔ᵐ fm₂) FromBothMaps k v fm₁ fm₂
Provenance-union fm₁@(m₁ , ks₁≡ks) fm₂@(m₂ , ks₂≡ks) {k} {v} k,v∈fm₁fm₂
with Expr-Provenance-≡ ((` m₁) (` m₂)) k,v∈fm₁fm₂
... | in (single k,v∈m₁) k∉km₂
with k∈km₁ (forget k,v∈m₁)
rewrite trans ks₁≡ks (sym ks₂≡ks) =
⊥-elim (k∉km₂ k∈km₁)
... | in k∉km₁ (single k,v∈m₂)
with k∈km₂ (forget k,v∈m₂)
rewrite trans ks₁≡ks (sym ks₂≡ks) =
⊥-elim (k∉km₁ k∈km₂)
... | bothᵘ {v₁} {v₂} (single k,v₁∈m₁) (single k,v₂∈m₂) =
((v₁ , v₂) , (refl , (k,v₁∈m₁ , k,v₂∈m₂)))
private
first-key-in-map : {k : A} {ks : List A} (fm : FiniteMap (k ks))
Σ B (λ v (k , v) ∈ᵐ fm)
@ -233,6 +204,26 @@ module IterProdIsomorphism where
k,v∈⇒k,v∈pop (m@(_ _ , push k≢ks _) , refl) k≢k' (here refl) = ⊥-elim (k≢k' refl)
k,v∈⇒k,v∈pop (m@(_ _ , push k≢ks _) , refl) k≢k' (there k,v'∈fm') = k,v'∈fm'
FromBothMaps : (k : A) (v : B) {ks : List A} (fm₁ fm₂ : FiniteMap ks) Set
FromBothMaps k v fm₁ fm₂ =
Σ (B × B)
(λ (v₁ , v₂) ( (v v₁ ⊔₂ v₂) × ((k , v₁) ∈ᵐ fm₁ × (k , v₂) ∈ᵐ fm₂)))
Provenance-union : {ks : List A} (fm₁ fm₂ : FiniteMap ks) {k : A} {v : B}
(k , v) ∈ᵐ (fm₁ ⊔ᵐ fm₂) FromBothMaps k v fm₁ fm₂
Provenance-union fm₁@(m₁ , ks₁≡ks) fm₂@(m₂ , ks₂≡ks) {k} {v} k,v∈fm₁fm₂
with Expr-Provenance-≡ ((` m₁) (` m₂)) k,v∈fm₁fm₂
... | in (single k,v∈m₁) k∉km₂
with k∈km₁ (forget k,v∈m₁)
rewrite trans ks₁≡ks (sym ks₂≡ks) =
⊥-elim (k∉km₂ k∈km₁)
... | in k∉km₁ (single k,v∈m₂)
with k∈km₂ (forget k,v∈m₂)
rewrite trans ks₁≡ks (sym ks₂≡ks) =
⊥-elim (k∉km₁ k∈km₂)
... | bothᵘ {v₁} {v₂} (single k,v₁∈m₁) (single k,v₂∈m₂) =
((v₁ , v₂) , (refl , (k,v₁∈m₁ , k,v₂∈m₂)))
pop-⊔-distr : {k : A} {ks : List A} (fm₁ fm₂ : FiniteMap (k ks))
pop (fm₁ ⊔ᵐ fm₂) ≈ᵐ (pop fm₁ ⊔ᵐ pop fm₂)
pop-⊔-distr {k} {ks} fm₁@(m₁ , _) fm₂@(m₂ , _) =
@ -416,12 +407,3 @@ module IterProdIsomorphism where
(to-⊔-distr uks) (from-⊔-distr {ks})
(from-to-inverseʳ uks) (from-to-inverseˡ uks)
using (isFiniteHeightLattice; finiteHeightLattice) public
-- Helpful lemma: all entries of the 'bottom' map are assigned to bottom.
open Height (IsFiniteHeightLattice.fixedHeight isFiniteHeightLattice) using ()
⊥-contains-bottoms : {k : A} {v : B} (k , v) ∈ᵐ v (Height.⊥ fhB)
⊥-contains-bottoms {k} {v} k,v∈⊥
rewrite IP.⊥-built (length ks) ≈₂-dec ≈ᵘ-dec h₂ 0 fhB fixedHeightᵘ =
to-build uks k v k,v∈⊥

View File

@ -11,11 +11,9 @@ module Lattice.IterProd {a} {A B : Set a}
(lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
open import Agda.Primitive using (lsuc)
open import Data.Nat using (; zero; suc; _+_)
open import Data.Product using (_×_; _,_; proj₁; proj₂)
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; cong)
open import Data.Nat using (; suc; _+_)
open import Data.Product using (_×_)
open import Utils using (iterate)
open import Chain using (Height)
open IsLattice lA renaming (FixedHeight to FixedHeight₁)
open IsLattice lB renaming (FixedHeight to FixedHeight₂)
@ -32,10 +30,6 @@ IterProd k = iterate k (λ t → A × t) B
-- that are built up by the two iterations. So, do everything in one iteration.
-- This requires some odd code.
build : A B (k : ) IterProd k
build _ b zero = b
build a b (suc s) = (a , build a b s)
private
record RequiredForFixedHeight : Set (lsuc a) where
field
@ -45,37 +39,22 @@ private
fhA : FixedHeight₁ h₁
fhB : FixedHeight₂ h₂
⊥₁ : A
⊥₁ = Height.⊥ fhA
⊥₂ : B
⊥₂ = Height.⊥ fhB
⊥k : (k : ) IterProd k
⊥k = build ⊥₁ ⊥₂
record IsFiniteHeightWithBotAndDecEq {A : Set a} {_≈_ : A A Set a} {_⊔_ : A A A} {_⊓_ : A A A} (isLattice : IsLattice A _≈_ _⊔_ _⊓_) ( : A) : Set (lsuc a) where
record IsFiniteHeightAndDecEq {A : Set a} {_≈_ : A A Set a} {_⊔_ : A A A} {_⊓_ : A A A} (isLattice : IsLattice A _≈_ _⊔_ _⊓_) : Set (lsuc a) where
field
height :
fixedHeight : IsLattice.FixedHeight isLattice height
≈-dec : IsDecidable _≈_
⊥-correct : Height.⊥ fixedHeight
record Everything (k : ) : Set (lsuc a) where
T = IterProd k
record Everything (A : Set a) : Set (lsuc a) where
field
_≈_ : T T Set a
_⊔_ : T T T
_⊓_ : T T T
_≈_ : A A Set a
_⊔_ : A A A
_⊓_ : A A A
isLattice : IsLattice T _≈_ _⊔_ _⊓_
isFiniteHeightIfSupported :
(req : RequiredForFixedHeight)
IsFiniteHeightWithBotAndDecEq isLattice (RequiredForFixedHeight.⊥k req k)
isLattice : IsLattice A _≈_ _⊔_ _⊓_
isFiniteHeightIfSupported : RequiredForFixedHeight IsFiniteHeightAndDecEq isLattice
everything : (k : ) Everything k
everything : (k : ) Everything (IterProd k)
everything 0 = record
{ _≈_ = _≈₂_
; _⊔_ = _⊔₂_
@ -85,7 +64,6 @@ private
{ height = RequiredForFixedHeight.h₂ req
; fixedHeight = RequiredForFixedHeight.fhB req
; ≈-dec = RequiredForFixedHeight.≈₂-dec req
; ⊥-correct = refl
}
}
everything (suc k') = record
@ -98,16 +76,13 @@ private
fhlRest = Everything.isFiniteHeightIfSupported everythingRest req
in
record
{ height = (RequiredForFixedHeight.h₁ req) + IsFiniteHeightWithBotAndDecEq.height fhlRest
{ height = (RequiredForFixedHeight.h₁ req) + IsFiniteHeightAndDecEq.height fhlRest
; fixedHeight =
P.fixedHeight
(RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightWithBotAndDecEq.≈-dec fhlRest)
(RequiredForFixedHeight.h₁ req) (IsFiniteHeightWithBotAndDecEq.height fhlRest)
(RequiredForFixedHeight.fhA req) (IsFiniteHeightWithBotAndDecEq.fixedHeight fhlRest)
; ≈-dec = P.≈-dec (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightWithBotAndDecEq.≈-dec fhlRest)
; ⊥-correct =
cong ((Height.⊥ (RequiredForFixedHeight.fhA req)) ,_)
(IsFiniteHeightWithBotAndDecEq.⊥-correct fhlRest)
(RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightAndDecEq.≈-dec fhlRest)
(RequiredForFixedHeight.h₁ req) (IsFiniteHeightAndDecEq.height fhlRest)
(RequiredForFixedHeight.fhA req) (IsFiniteHeightAndDecEq.fixedHeight fhlRest)
; ≈-dec = P.≈-dec (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightAndDecEq.≈-dec fhlRest)
}
}
where
@ -146,22 +121,16 @@ module _ (k : ) where
; fhB = fhB
}
fixedHeight = IsFiniteHeightWithBotAndDecEq.fixedHeight (Everything.isFiniteHeightIfSupported (everything k) required)
isFiniteHeightLattice = record
{ isLattice = isLattice
; fixedHeight = fixedHeight
; fixedHeight = IsFiniteHeightAndDecEq.fixedHeight (Everything.isFiniteHeightIfSupported (everything k) required)
}
finiteHeightLattice : FiniteHeightLattice (IterProd k)
finiteHeightLattice = record
{ height = IsFiniteHeightWithBotAndDecEq.height (Everything.isFiniteHeightIfSupported (everything k) required)
{ height = IsFiniteHeightAndDecEq.height (Everything.isFiniteHeightIfSupported (everything k) required)
; _≈_ = _≈_
; _⊔_ = _⊔_
; _⊓_ = _⊓_
; isFiniteHeightLattice = isFiniteHeightLattice
}
⊥-built : Height.⊥ fixedHeight (build (Height.⊥ fhA) (Height.⊥ fhB) k)
⊥-built = IsFiniteHeightWithBotAndDecEq.⊥-correct (Everything.isFiniteHeightIfSupported (everything k) required)

View File

@ -1112,19 +1112,6 @@ _[_] m (k ∷ ks)
... | yes k∈km = proj₁ (locate {m = m} k∈km) (m [ ks ])
... | no _ = m [ ks ]
[]-∈ : {k : A} {v : B} {ks : List A} (m : Map)
(k , v) m k ∈ˡ ks v ∈ˡ (m [ ks ])
[]-∈ {k} {v} {ks} m k,v∈m (here refl)
with ∈k-dec k (proj₁ m)
... | no k∉km = ⊥-elim (k∉km (forget k,v∈m))
... | yes k∈km
with (v' , k,v'∈m) locate {m = m} k∈km
rewrite Map-functional {m = m} k,v'∈m k,v∈m = here refl
[]-∈ {k} {v} {k' ks'} m k,v∈m (there k∈ks')
with ∈k-dec k' (proj₁ m)
... | no _ = []-∈ m k,v∈m k∈ks'
... | yes _ = there ([]-∈ m k,v∈m k∈ks')
m₁≼m₂⇒m₁[k]≼m₂[k] : (m₁ m₂ : Map) {k : A} {v₁ v₂ : B}
m₁ m₂ (k , v₁) m₁ (k , v₂) m₂ v₁ ≼₂ v₂
m₁≼m₂⇒m₁[k]≼m₂[k] m₁ m₂ m₁≼m₂ k,v₁∈m₁ k,v₂∈m₂
@ -1142,12 +1129,3 @@ m₁≼m₂⇒k∈km₁⇒k∈km₂ m₁ m₂ m₁≼m₂ k∈km₁ =
(v' , (v≈v' , k,v'∈m₂)) = (proj₁ m₁≼m₂) _ _ k,v∈m₁m₂
in
forget k,v'∈m₂
m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ : (m₁ m₂ : Map) {k : A}
m₁ m₂ (k∈km₁ : k ∈k m₁) (k∈km₂ : k ∈k m₂)
proj₁ (locate {m = m₁} k∈km₁) ≈₂ proj₁ (locate {m = m₂} k∈km₂)
m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂ m₁ m₂ {k} (m₁⊆m₂ , m₂⊆m₁) k∈km₁ k∈km₂
with (v₁ , k,v₁∈m₁) locate {m = m₁} k∈km₁
with (v₂ , k,v₂∈m₂) locate {m = m₂} k∈km₂
with (v₂' , (v₁≈v₂' , k,v₂'∈m₂)) m₁⊆m₂ k v₁ k,v₁∈m₁
rewrite Map-functional {m = m₂} k,v₂∈m₂ k,v₂'∈m₂ = v₁≈v₂'

View File

@ -143,8 +143,17 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
∙,b-Preserves-≈₁ : (b : B) (λ a (a , b)) Preserves _≈₁_ _≈_
∙,b-Preserves-≈₁ b {a₁} {a₂} a₁≈a₂ = (a₁≈a₂ , ≈₂-refl)
open ChainA.Height fhA using () renaming ( to ⊥₁; to ⊤₁; longestChain to longestChain₁; bounded to bounded₁)
open ChainB.Height fhB using () renaming ( to ⊥₂; to ⊤₂; longestChain to longestChain₂; bounded to bounded₂)
amin : A
amin = proj₁ (proj₁ (proj₁ fhA))
amax : A
amax = proj₂ (proj₁ (proj₁ fhA))
bmin : B
bmin = proj₁ (proj₁ (proj₁ fhB))
bmax : B
bmax = proj₂ (proj₁ (proj₁ fhB))
unzip : {a₁ a₂ : A} {b₁ b₂ : B} {n : } Chain (a₁ , b₁) (a₂ , b₂) n Σ ( × ) (λ (n₁ , n₂) ((Chain₁ a₁ a₂ n₁ × Chain₂ b₁ b₂ n₂) × (n n₁ + n₂)))
unzip (done (a₁≈a₂ , b₁≈b₂)) = ((0 , 0) , ((done₁ a₁≈a₂ , done₂ b₁≈b₂) , ≤-refl))
@ -163,16 +172,15 @@ module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
))
fixedHeight : IsLattice.FixedHeight isLattice (h₁ + h₂)
fixedHeight = record
{ = (⊥₁ , ⊥₂)
; = (⊤₁ , ⊤₂)
; longestChain = concat
(ChainMapping₁.Chain-map (λ a (a , ⊥₂)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) longestChain₁)
(ChainMapping₂.Chain-map (λ b (⊤₁ , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) longestChain₂)
; bounded = λ a₁b₁a₂b₂
let ((n₁ , n₂) , ((a₁a₂ , b₁b₂) , n≤n₁+n₂)) = unzip a₁b₁a₂b₂
in ≤-trans n≤n₁+n₂ (+-mono-≤ (bounded₁ a₁a₂) (bounded₂ b₁b₂))
}
fixedHeight =
( ( ((amin , bmin) , (amax , bmax))
, concat
(ChainMapping₁.Chain-map (λ a (a , bmin)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) (proj₂ (proj₁ fhA)))
(ChainMapping₂.Chain-map (λ b (amax , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) (proj₂ (proj₁ fhB)))
)
, λ a₁b₁a₂b₂ let ((n₁ , n₂) , ((a₁a₂ , b₁b₂) , n≤n₁+n₂)) = unzip a₁b₁a₂b₂
in ≤-trans n≤n₁+n₂ (+-mono-≤ (proj₂ fhA a₁a₂) (proj₂ fhB b₁b₂))
)
isFiniteHeightLattice : IsFiniteHeightLattice (A × B) (h₁ + h₂) _≈_ _⊔_ _⊓_
isFiniteHeightLattice = record

View File

@ -108,12 +108,7 @@ private
isLongest (done _) = z≤n
fixedHeight : IsLattice.FixedHeight isLattice 0
fixedHeight = record
{ = tt
; = tt
; longestChain = longestChain
; bounded = isLongest
}
fixedHeight = (((tt , tt) , longestChain) , isLongest)
isFiniteHeightLattice : IsFiniteHeightLattice 0 _≈_ _⊔_ _⊓_
isFiniteHeightLattice = record