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

Compare commits

base: DanilaFe:4da9b6d3cd6d55373f2920c8494b0f5d2682774e
Branches Tags
DanilaFe:main
...
compare: DanilaFe:cf824dc7443ce9ff78127200d4886838114e310c
Branches Tags
DanilaFe:main

6 Commits
4da9b6d3cd ... cf824dc744

Author SHA1 Message Date
Danila Fedorin
cf824dc744 Switch product to using instances 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2025-01-04 21:33:59 -08:00
Danila Fedorin
70847d51db Swich AboveBelow to using instances 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2025-01-04 21:23:07 -08:00
Danila Fedorin
d96eb97b69 Switch maps (and consequently most of the code) to using instances 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2025-01-04 21:16:22 -08:00
Danila Fedorin
d90b544436 Use binary operator for decidable equality consistently 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2025-01-04 19:08:28 -08:00
Danila Fedorin
b0488c9cc6 Make 'IsDecidable' into a record to aid instance search 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2025-01-04 18:58:56 -08:00
Danila Fedorin
8abf6f8670 Make 'isLattice' for simple types be an instance 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
 2025-01-04 17:27:38 -08:00
19 changed files with 538 additions and 482 deletions
Show Stats Expand all files Collapse all files

14
Analysis/Forward.agda
View File

@ -2,10 +2,10 @@ open import Language hiding (_[_])
open import Lattice open import Lattice
module Analysis.Forward module Analysis.Forward
{L : Set} {h} (L : Set) {h}
{_≈ˡ_ : L → L → Set} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L} {_≈ˡ_ : L → L → Set} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
(isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_) {{isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_}}
(≈ˡ-dec : IsDecidable _≈ˡ_) where {{≈ˡ-dec : IsDecidable _≈ˡ_}} where
open import Data.Empty using (⊥-elim) open import Data.Empty using (⊥-elim)
open import Data.String using (String) open import Data.String using (String)
@ -20,8 +20,8 @@ open IsFiniteHeightLattice isFiniteHeightLatticeˡ
using () renaming (isLattice to isLatticeˡ) using () renaming (isLattice to isLatticeˡ)
module WithProg (prog : Program) where module WithProg (prog : Program) where
open import Analysis.Forward.Lattices isFiniteHeightLatticeˡ ≈ˡ-dec prog open import Analysis.Forward.Lattices L prog hiding (≈ᵛ-Decidable) -- to disambiguate instance resolution
open import Analysis.Forward.Evaluation isFiniteHeightLatticeˡ ≈ˡ-dec prog open import Analysis.Forward.Evaluation L prog
open Program prog open Program prog
private module WithStmtEvaluator {{evaluator : StmtEvaluator}} where private module WithStmtEvaluator {{evaluator : StmtEvaluator}} where
@ -43,7 +43,7 @@ module WithProg (prog : Program) where
(flip (eval s)) (eval-Monoʳ s) (flip (eval s)) (eval-Monoʳ s)
vs₁≼vs₂ vs₁≼vs₂
open StateVariablesFiniteMap.GeneralizedUpdate isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) updateVariablesForState updateVariablesForState-Monoʳ states open StateVariablesFiniteMap.GeneralizedUpdate {{isLatticeᵐ}} (λ x → x) (λ a₁≼a₂ → a₁≼a₂) updateVariablesForState updateVariablesForState-Monoʳ states
using () using ()
renaming renaming
( f' to updateAll ( f' to updateAll
@ -65,7 +65,7 @@ module WithProg (prog : Program) where
(joinAll-Mono {sv₁} {sv₂} sv₁≼sv₂) (joinAll-Mono {sv₁} {sv₂} sv₁≼sv₂)
-- The fixed point of the 'analyze' function is our final goal. -- The fixed point of the 'analyze' function is our final goal.
open import Fixedpoint ≈ᵐ-dec isFiniteHeightLatticeᵐ analyze (λ {m₁} {m₂} m₁≼m₂ → analyze-Mono {m₁} {m₂} m₁≼m₂) open import Fixedpoint ≈ᵐ-Decidable isFiniteHeightLatticeᵐ analyze (λ {m₁} {m₂} m₁≼m₂ → analyze-Mono {m₁} {m₂} m₁≼m₂)
using () using ()
renaming (aᶠ to result; aᶠ≈faᶠ to result≈analyze-result) renaming (aᶠ to result; aᶠ≈faᶠ to result≈analyze-result)
public public

12
Analysis/Forward/Adapters.agda
View File

@ -2,14 +2,14 @@ open import Language hiding (_[_])
open import Lattice open import Lattice
module Analysis.Forward.Adapters module Analysis.Forward.Adapters
{L : Set} {h} (L : Set) {h}
{_≈ˡ_ : L → L → Set} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L} {_≈ˡ_ : L → L → Set} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
(isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_) {{isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_}}
(≈ˡ-dec : IsDecidable _≈ˡ_) {{≈ˡ-dec : IsDecidable _≈ˡ_}}
(prog : Program) where (prog : Program) where
open import Analysis.Forward.Lattices isFiniteHeightLatticeˡ ≈ˡ-dec prog open import Analysis.Forward.Lattices L prog
open import Analysis.Forward.Evaluation isFiniteHeightLatticeˡ ≈ˡ-dec prog open import Analysis.Forward.Evaluation L prog
open import Data.Empty using (⊥-elim) open import Data.Empty using (⊥-elim)
open import Data.String using (String) renaming (_≟_ to _≟ˢ_) open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
@ -41,7 +41,7 @@ module ExprToStmtAdapter {{ exprEvaluator : ExprEvaluator }} where
-- for an assignment, and update the corresponding key. Use Exercise 4.26's -- for an assignment, and update the corresponding key. Use Exercise 4.26's
-- generalized update to set the single key's value. -- generalized update to set the single key's value.
private module _ (k : String) (e : Expr) where private module _ (k : String) (e : Expr) where
open VariableValuesFiniteMap.GeneralizedUpdate isLatticeᵛ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) (λ _ → evalᵉ e) (λ _ {vs₁} {vs₂} vs₁≼vs₂ → evalᵉ-Monoʳ e {vs₁} {vs₂} vs₁≼vs₂) (k ∷ []) open VariableValuesFiniteMap.GeneralizedUpdate {{isLatticeᵛ}} (λ x → x) (λ a₁≼a₂ → a₁≼a₂) (λ _ → evalᵉ e) (λ _ {vs₁} {vs₂} vs₁≼vs₂ → evalᵉ-Monoʳ e {vs₁} {vs₂} vs₁≼vs₂) (k ∷ [])
using () using ()
renaming renaming
( f' to updateVariablesFromExpression ( f' to updateVariablesFromExpression

8
Analysis/Forward/Evaluation.agda
View File

@ -2,13 +2,13 @@ open import Language hiding (_[_])
open import Lattice open import Lattice
module Analysis.Forward.Evaluation module Analysis.Forward.Evaluation
{L : Set} {h} (L : Set) {h}
{_≈ˡ_ : L → L → Set} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L} {_≈ˡ_ : L → L → Set} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
(isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_) {{isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_}}
(≈ˡ-dec : IsDecidable _≈ˡ_) {{≈ˡ-dec : IsDecidable _≈ˡ_}}
(prog : Program) where (prog : Program) where
open import Analysis.Forward.Lattices isFiniteHeightLatticeˡ ≈ˡ-dec prog open import Analysis.Forward.Lattices L prog
open import Data.Product using (_,_) open import Data.Product using (_,_)
open IsFiniteHeightLattice isFiniteHeightLatticeˡ open IsFiniteHeightLattice isFiniteHeightLatticeˡ

40
Analysis/Forward/Lattices.agda
View File

@ -2,20 +2,21 @@ open import Language hiding (_[_])
open import Lattice open import Lattice
module Analysis.Forward.Lattices module Analysis.Forward.Lattices
{L : Set} {h} (L : Set) {h}
{_≈ˡ_ : L → L → Set} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L} {_≈ˡ_ : L → L → Set} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
(isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_) {{isFiniteHeightLatticeˡ : IsFiniteHeightLattice L h _≈ˡ_ _⊔ˡ_ _⊓ˡ_}}
(≈ˡ-dec : IsDecidable _≈ˡ_) {{≈ˡ-Decidable : IsDecidable _≈ˡ_}}
(prog : Program) where (prog : Program) where
open import Data.String using () renaming (_≟_ to _≟ˢ_) open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
open import Data.Product using (proj₁; proj₂; _,_) open import Data.Product using (proj₁; proj₂; _,_)
open import Data.Unit using (tt)
open import Data.Sum using (inj₁; inj₂) open import Data.Sum using (inj₁; inj₂)
open import Data.List using (List; _∷_; []; foldr) open import Data.List using (List; _∷_; []; foldr)
open import Data.List.Membership.Propositional using () renaming (_∈_ to _∈ˡ_) open import Data.List.Membership.Propositional using () renaming (_∈_ to _∈ˡ_)
open import Data.List.Relation.Unary.Any as Any using () open import Data.List.Relation.Unary.Any as Any using ()
open import Relation.Binary.PropositionalEquality using (_≡_; refl) open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Utils using (Pairwise; _⇒_; _∨_) open import Utils using (Pairwise; _⇒_; _∨_; it)
open IsFiniteHeightLattice isFiniteHeightLatticeˡ open IsFiniteHeightLattice isFiniteHeightLatticeˡ
using () using ()
@ -29,11 +30,15 @@ open Program prog
import Lattice.FiniteMap import Lattice.FiniteMap
import Chain import Chain
instance
≡-Decidable-String = record { R-dec = _≟ˢ_ }
≡-Decidable-State = record { R-dec = _≟_ }
-- The variable -> abstract value (e.g. sign) map is a finite value-map -- The variable -> abstract value (e.g. sign) map is a finite value-map
-- with keys strings. Use a bundle to avoid explicitly specifying operators. -- with keys strings. Use a bundle to avoid explicitly specifying operators.
-- It's helpful to export these via 'public' since consumers tend to -- It's helpful to export these via 'public' since consumers tend to
-- use various variable lattice operations. -- use various variable lattice operations.
module VariableValuesFiniteMap = Lattice.FiniteMap.WithKeys _≟ˢ_ isLatticeˡ vars module VariableValuesFiniteMap = Lattice.FiniteMap.WithKeys String L tt vars
open VariableValuesFiniteMap open VariableValuesFiniteMap
using () using ()
renaming renaming
@ -42,7 +47,7 @@ open VariableValuesFiniteMap
; _≈_ to _≈ᵛ_ ; _≈_ to _≈ᵛ_
; _⊔_ to _⊔ᵛ_ ; _⊔_ to _⊔ᵛ_
; _≼_ to _≼ᵛ_ ; _≼_ to _≼ᵛ_
; ≈₂-dec⇒≈-dec to ≈ˡ-dec⇒≈ᵛ-dec ; ≈-Decidable to ≈ᵛ-Decidable
; _∈_ to _∈ᵛ_ ; _∈_ to _∈ᵛ_
; _∈k_ to _∈kᵛ_ ; _∈k_ to _∈kᵛ_
; _updating_via_ to _updatingᵛ_via_ ; _updating_via_ to _updatingᵛ_via_
@ -60,27 +65,25 @@ open IsLattice isLatticeᵛ
; ⊔-idemp to ⊔ᵛ-idemp ; ⊔-idemp to ⊔ᵛ-idemp
) )
public public
open Lattice.FiniteMap.IterProdIsomorphism _≟ˢ_ isLatticeˡ open Lattice.FiniteMap.IterProdIsomorphism String L _
using () using ()
renaming renaming
( Provenance-union to Provenance-unionᵐ ( Provenance-union to Provenance-unionᵐ
) )
public public
open Lattice.FiniteMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟ˢ_ isLatticeˡ vars-Unique ≈ˡ-dec _ fixedHeightˡ open Lattice.FiniteMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight String L _ vars-Unique
using () using ()
renaming renaming
( isFiniteHeightLattice to isFiniteHeightLatticeᵛ ( isFiniteHeightLattice to isFiniteHeightLatticeᵛ
; fixedHeight to fixedHeightᵛ
; ⊥-contains-bottoms to ⊥ᵛ-contains-bottoms ; ⊥-contains-bottoms to ⊥ᵛ-contains-bottoms
) )
public public
≈ᵛ-dec = ≈ˡ-dec⇒≈ᵛ-dec ≈ˡ-dec
joinSemilatticeᵛ = IsFiniteHeightLattice.joinSemilattice isFiniteHeightLatticeᵛ
fixedHeightᵛ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵛ
⊥ᵛ = Chain.Height.⊥ fixedHeightᵛ ⊥ᵛ = Chain.Height.⊥ fixedHeightᵛ
-- Finally, the map we care about is (state -> (variables -> value)). Bring that in. -- Finally, the map we care about is (state -> (variables -> value)). Bring that in.
module StateVariablesFiniteMap = Lattice.FiniteMap.WithKeys _≟_ isLatticeᵛ states module StateVariablesFiniteMap = Lattice.FiniteMap.WithKeys State VariableValues tt states
open StateVariablesFiniteMap open StateVariablesFiniteMap
using (_[_]; []-∈; m₁≼m₂⇒m₁[ks]≼m₂[ks]; m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂) using (_[_]; []-∈; m₁≼m₂⇒m₁[ks]≼m₂[ks]; m₁≈m₂⇒k∈m₁⇒k∈km₂⇒v₁≈v₂)
renaming renaming
@ -91,11 +94,11 @@ open StateVariablesFiniteMap
; _∈k_ to _∈kᵐ_ ; _∈k_ to _∈kᵐ_
; locate to locateᵐ ; locate to locateᵐ
; _≼_ to _≼ᵐ_ ; _≼_ to _≼ᵐ_
; ≈₂-dec⇒≈-dec to ≈ᵛ-dec⇒≈ᵐ-dec ; ≈-Decidable to ≈ᵐ-Decidable
; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ
) )
public public
open Lattice.FiniteMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight _≟_ isLatticeᵛ states-Unique ≈ᵛ-dec _ fixedHeightᵛ open Lattice.FiniteMap.IterProdIsomorphism.WithUniqueKeysAndFixedHeight State VariableValues _ states-Unique
using () using ()
renaming renaming
( isFiniteHeightLattice to isFiniteHeightLatticeᵐ ( isFiniteHeightLattice to isFiniteHeightLatticeᵐ
@ -108,9 +111,6 @@ open IsFiniteHeightLattice isFiniteHeightLatticeᵐ
) )
public public
≈ᵐ-dec = ≈ᵛ-dec⇒≈ᵐ-dec ≈ᵛ-dec
fixedHeightᵐ = IsFiniteHeightLattice.fixedHeight isFiniteHeightLatticeᵐ
-- We now have our (state -> (variables -> value)) map. -- We now have our (state -> (variables -> value)) map.
-- Define a couple of helpers to retrieve values from it. Specifically, -- Define a couple of helpers to retrieve values from it. Specifically,
-- since the State type is as specific as possible, it's always possible to -- since the State type is as specific as possible, it's always possible to
@ -144,12 +144,12 @@ joinForKey k states = foldr _⊔ᵛ_ ⊥ᵛ (states [ incoming k ])
joinForKey-Mono : ∀ (k : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (joinForKey k) joinForKey-Mono : ∀ (k : State) → Monotonic _≼ᵐ_ _≼ᵛ_ (joinForKey k)
joinForKey-Mono k {fm₁} {fm₂} fm₁≼fm₂ = joinForKey-Mono k {fm₁} {fm₂} fm₁≼fm₂ =
foldr-Mono joinSemilatticeᵛ joinSemilatticeᵛ (fm₁ [ incoming k ]) (fm₂ [ incoming k ]) _⊔ᵛ_ ⊥ᵛ ⊥ᵛ foldr-Mono it it (fm₁ [ incoming k ]) (fm₂ [ incoming k ]) _⊔ᵛ_ ⊥ᵛ ⊥ᵛ
(m₁≼m₂⇒m₁[ks]≼m₂[ks] fm₁ fm₂ (incoming k) fm₁≼fm₂) (m₁≼m₂⇒m₁[ks]≼m₂[ks] fm₁ fm₂ (incoming k) fm₁≼fm₂)
(⊔ᵛ-idemp ⊥ᵛ) ⊔ᵛ-Monotonicʳ ⊔ᵛ-Monotonicˡ (⊔ᵛ-idemp ⊥ᵛ) ⊔ᵛ-Monotonicʳ ⊔ᵛ-Monotonicˡ
-- The name f' comes from the formulation of Exercise 4.26. -- The name f' comes from the formulation of Exercise 4.26.
open StateVariablesFiniteMap.GeneralizedUpdate isLatticeᵐ (λ x → x) (λ a₁≼a₂ → a₁≼a₂) joinForKey joinForKey-Mono states open StateVariablesFiniteMap.GeneralizedUpdate {{isLatticeᵐ}} (λ x → x) (λ a₁≼a₂ → a₁≼a₂) joinForKey joinForKey-Mono states
using () using ()
renaming renaming
( f' to joinAll ( f' to joinAll

31
Analysis/Sign.agda
View File

@ -7,11 +7,13 @@ open import Data.Sum using (inj₁; inj₂)
open import Data.Empty using (⊥; ⊥-elim) open import Data.Empty using (⊥; ⊥-elim)
open import Data.Unit using (⊤; tt) open import Data.Unit using (⊤; tt)
open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_) open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_)
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst) open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans; subst)
open import Relation.Nullary using (¬_; yes; no) open import Relation.Nullary using (¬_; yes; no)
open import Language open import Language
open import Lattice open import Lattice
open import Equivalence
open import Showable using (Showable; show) open import Showable using (Showable; show)
open import Utils using (_⇒_; _∧_; _∨_) open import Utils using (_⇒_; _∧_; _∨_)
import Analysis.Forward import Analysis.Forward
@ -32,7 +34,7 @@ instance
} }
-- g for siGn; s is used for strings and i is not very descriptive. -- g for siGn; s is used for strings and i is not very descriptive.
_≟ᵍ_ : IsDecidable (_≡_ {_} {Sign}) _≟ᵍ_ : Decidable (_≡_ {_} {Sign})
_≟ᵍ_ + + = yes refl _≟ᵍ_ + + = yes refl
_≟ᵍ_ + - = no (λ ()) _≟ᵍ_ + - = no (λ ())
_≟ᵍ_ + 0ˢ = no (λ ()) _≟ᵍ_ + 0ˢ = no (λ ())
@ -43,12 +45,22 @@ _≟ᵍ_ 0ˢ + = no (λ ())
_≟ᵍ_ 0ˢ - = no (λ ()) _≟ᵍ_ 0ˢ - = no (λ ())
_≟ᵍ_ 0ˢ 0ˢ = yes refl _≟ᵍ_ 0ˢ 0ˢ = yes refl
instance
≡-equiv : IsEquivalence Sign _≡_
≡-equiv = record
{ ≈-refl = refl
; ≈-sym = sym
; ≈-trans = trans
}
≡-Decidable-Sign : IsDecidable {_} {Sign} _≡_
≡-Decidable-Sign = record { R-dec = _≟ᵍ_ }
-- embelish 'sign' with a top and bottom element. -- embelish 'sign' with a top and bottom element.
open import Lattice.AboveBelow Sign _≡_ (record { ≈-refl = refl; ≈-sym = sym; ≈-trans = trans }) _≟ᵍ_ as AB open import Lattice.AboveBelow Sign _ as AB
using () using ()
renaming renaming
( AboveBelow to SignLattice ( AboveBelow to SignLattice
; ≈-dec to ≈ᵍ-dec
; ⊥ to ⊥ᵍ ; ⊥ to ⊥ᵍ
; ⊤ to ⊤ᵍ ; ⊤ to ⊤ᵍ
; [_] to [_]ᵍ ; [_] to [_]ᵍ
@ -68,10 +80,7 @@ open AB.Plain 0ˢ using ()
; _⊓_ to _⊓ᵍ_ ; _⊓_ to _⊓ᵍ_
) )
open IsLattice isLatticeᵍ using () open IsLattice isLatticeᵍ using () renaming (≼-trans to ≼ᵍ-trans)
renaming
( ≼-trans to ≼ᵍ-trans
)
plus : SignLattice → SignLattice → SignLattice plus : SignLattice → SignLattice → SignLattice
plus ⊥ᵍ _ = ⊥ᵍ plus ⊥ᵍ _ = ⊥ᵍ
@ -171,9 +180,9 @@ instance
module WithProg (prog : Program) where module WithProg (prog : Program) where
open Program prog open Program prog
open import Analysis.Forward.Lattices isFiniteHeightLatticeᵍ ≈ᵍ-dec prog open import Analysis.Forward.Lattices SignLattice prog
open import Analysis.Forward.Evaluation isFiniteHeightLatticeᵍ ≈ᵍ-dec prog open import Analysis.Forward.Evaluation SignLattice prog
open import Analysis.Forward.Adapters isFiniteHeightLatticeᵍ ≈ᵍ-dec prog open import Analysis.Forward.Adapters SignLattice prog
eval : ∀ (e : Expr) → VariableValues → SignLattice eval : ∀ (e : Expr) → VariableValues → SignLattice
eval (e₁ + e₂) vs = plus (eval e₁ vs) (eval e₂ vs) eval (e₁ + e₂) vs = plus (eval e₁ vs) (eval e₂ vs)
@ -229,7 +238,7 @@ module WithProg (prog : Program) where
SignEval = record { eval = eval; eval-Monoʳ = eval-Monoʳ } SignEval = record { eval = eval; eval-Monoʳ = eval-Monoʳ }
-- For debugging purposes, print out the result. -- For debugging purposes, print out the result.
output = show (Analysis.Forward.WithProg.result isFiniteHeightLatticeᵍ ≈ᵍ-dec prog) output = show (Analysis.Forward.WithProg.result SignLattice prog)
-- This should have fewer cases -- the same number as the actual 'plus' above. -- This should have fewer cases -- the same number as the actual 'plus' above.
-- But agda only simplifies on first argument, apparently, so we are stuck -- But agda only simplifies on first argument, apparently, so we are stuck

3
Fixedpoint.agda
View File

@ -5,7 +5,7 @@ module Fixedpoint {a} {A : Set a}
{h : ℕ} {h : ℕ}
{_≈_ : A → A → Set a} {_≈_ : A → A → Set a}
{_⊔_ : A → A → A} {_⊓_ : A → A → A} {_⊔_ : A → A → A} {_⊓_ : A → A → A}
(≈-dec : IsDecidable _≈_) (≈-Decidable : IsDecidable _≈_)
(flA : IsFiniteHeightLattice A h _≈_ _⊔_ _⊓_) (flA : IsFiniteHeightLattice A h _≈_ _⊔_ _⊓_)
(f : A → A) (f : A → A)
(Monotonicᶠ : Monotonic (IsFiniteHeightLattice._≼_ flA) (Monotonicᶠ : Monotonic (IsFiniteHeightLattice._≼_ flA)
@ -17,6 +17,7 @@ open import Data.Empty using (⊥-elim)
open import Relation.Binary.PropositionalEquality using (_≡_; sym) open import Relation.Binary.PropositionalEquality using (_≡_; sym)
open import Relation.Nullary using (Dec; ¬_; yes; no) open import Relation.Nullary using (Dec; ¬_; yes; no)
open IsDecidable ≈-Decidable using () renaming (R-dec to ≈-dec)
open IsFiniteHeightLattice flA open IsFiniteHeightLattice flA
import Chain import Chain

46
Isomorphism.agda
View File

@ -63,27 +63,29 @@ module TransportFiniteHeight
portChain₂ (done₂ a₂≈a₁) = done₁ (g-preserves-≈₂ a₂≈a₁) portChain₂ (done₂ a₂≈a₁) = done₁ (g-preserves-≈₂ a₂≈a₁)
portChain₂ (step₂ {b₁} {b₂} (b₁≼b₂ , b₁̷≈b₂) b₂≈b₂' c) = step₁ (≈₁-trans (≈₁-sym (g-⊔-distr b₁ b₂)) (g-preserves-≈₂ b₁≼b₂) , g-preserves-̷≈ b₁̷≈b₂) (g-preserves-≈₂ b₂≈b₂') (portChain₂ c) portChain₂ (step₂ {b₁} {b₂} (b₁≼b₂ , b₁̷≈b₂) b₂≈b₂' c) = step₁ (≈₁-trans (≈₁-sym (g-⊔-distr b₁ b₂)) (g-preserves-≈₂ b₁≼b₂) , g-preserves-̷≈ b₁̷≈b₂) (g-preserves-≈₂ b₂≈b₂') (portChain₂ c)
isFiniteHeightLattice : IsFiniteHeightLattice B height _≈₂_ _⊔₂_ _⊓₂_ open Chain.Height (IsFiniteHeightLattice.fixedHeight fhlA)
isFiniteHeightLattice = using ()
let renaming (⊥ to ⊥₁; ⊤ to ⊤₁; bounded to bounded₁; longestChain to c)
open Chain.Height (IsFiniteHeightLattice.fixedHeight fhlA)
using () instance
renaming (⊥ to ⊥₁; ⊤ to ⊤₁; bounded to bounded₁; longestChain to c) fixedHeight = record
in record { ⊥ = f ⊥₁
{ isLattice = lB ; ⊤ = f ⊤₁
; fixedHeight = record ; longestChain = portChain₁ c
{ ⊥ = f ⊥₁ ; bounded = λ c' → bounded₁ (portChain₂ c')
; ⊤ = f ⊤₁
; longestChain = portChain₁ c
; bounded = λ c' → bounded₁ (portChain₂ c')
}
} }
finiteHeightLattice : FiniteHeightLattice B isFiniteHeightLattice : IsFiniteHeightLattice B height _≈₂_ _⊔₂_ _⊓₂_
finiteHeightLattice = record isFiniteHeightLattice = record
{ height = height { isLattice = lB
; _≈_ = _≈₂_ ; fixedHeight = fixedHeight
; _⊔_ = _⊔₂_ }
; _⊓_ = _⊓₂_
; isFiniteHeightLattice = isFiniteHeightLattice finiteHeightLattice : FiniteHeightLattice B
} finiteHeightLattice = record
{ height = height
; _≈_ = _≈₂_
; _⊔_ = _⊔₂_
; _⊓_ = _⊓₂_
; isFiniteHeightLattice = isFiniteHeightLattice
}

7
Language.agda
View File

@ -16,12 +16,13 @@ open import Data.Nat using (ℕ; suc)
open import Data.Product using (_,_; Σ; proj₁; proj₂) open import Data.Product using (_,_; Σ; proj₁; proj₂)
open import Data.Product.Properties as ProdProp using () open import Data.Product.Properties as ProdProp using ()
open import Data.String using (String) renaming (_≟_ to _≟ˢ_) open import Data.String using (String) renaming (_≟_ to _≟ˢ_)
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Binary.PropositionalEquality using (_≡_; refl) open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Relation.Nullary using (¬_) open import Relation.Nullary using (¬_)
open import Lattice open import Lattice
open import Utils using (Unique; push; Unique-map; x∈xs⇒fx∈fxs) open import Utils using (Unique; push; Unique-map; x∈xs⇒fx∈fxs)
open import Lattice.MapSet _≟ˢ_ using () open import Lattice.MapSet String {{record { R-dec = _≟ˢ_ }}} _ using ()
renaming renaming
( MapSet to StringSet ( MapSet to StringSet
; to-List to to-Listˢ ; to-List to to-Listˢ
@ -73,10 +74,10 @@ record Program : Set where
-- vars-complete : ∀ {k : String} (s : State) → k ∈ᵇ (code s) → k ListMem.∈ vars -- vars-complete : ∀ {k : String} (s : State) → k ∈ᵇ (code s) → k ListMem.∈ vars
-- vars-complete {k} s = ∈⇒∈-Stmts-vars {length} {k} {stmts} {s} -- vars-complete {k} s = ∈⇒∈-Stmts-vars {length} {k} {stmts} {s}
_≟_ : IsDecidable (_≡_ {_} {State}) _≟_ : Decidable (_≡_ {_} {State})
_≟_ = FinProp._≟_ _≟_ = FinProp._≟_
_≟ᵉ_ : IsDecidable (_≡_ {_} {Graph.Edge graph}) _≟ᵉ_ : Decidable (_≡_ {_} {Graph.Edge graph})
_≟ᵉ_ = ProdProp.≡-dec _≟_ _≟_ _≟ᵉ_ = ProdProp.≡-dec _≟_ _≟_
open import Data.List.Membership.DecPropositional _≟ᵉ_ using (_∈?_) open import Data.List.Membership.DecPropositional _≟ᵉ_ using (_∈?_)

2
Language/Base.agda
View File

@ -39,7 +39,7 @@ data _∈ᵇ_ : String → BasicStmt → Set where
in←₁ : ∀ {k : String} {e : Expr} → k ∈ᵇ (k ← e) in←₁ : ∀ {k : String} {e : Expr} → k ∈ᵇ (k ← e)
in←₂ : ∀ {k k' : String} {e : Expr} → k ∈ᵉ e → k ∈ᵇ (k' ← e) in←₂ : ∀ {k k' : String} {e : Expr} → k ∈ᵉ e → k ∈ᵇ (k' ← e)
open import Lattice.MapSet (String._≟_) open import Lattice.MapSet String {{record { R-dec = String._≟_ }}} _
renaming renaming
( MapSet to StringSet ( MapSet to StringSet
; insert to insertˢ ; insert to insertˢ

19
Lattice.agda
View File

@ -11,8 +11,9 @@ open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔ℓ_) open import Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔ℓ_)
open import Function.Definitions using (Injective) open import Function.Definitions using (Injective)
IsDecidable : ∀ {a} {A : Set a} (R : A → A → Set a) → Set a record IsDecidable {a} {A : Set a} (R : A → A → Set a) : Set a where
IsDecidable {a} {A} R = ∀ (a₁ a₂ : A) → Dec (R a₁ a₂) field
R-dec : ∀ (a₁ a₂ : A) → Dec (R a₁ a₂)
module _ {a b} {A : Set a} {B : Set b} module _ {a b} {A : Set a} {B : Set b}
(_≼₁_ : A → A → Set a) (_≼₂_ : B → B → Set b) where (_≼₁_ : A → A → Set a) (_≼₂_ : B → B → Set b) where
@ -186,8 +187,8 @@ record IsLattice {a} (A : Set a)
(_⊓_ : A → A → A) : Set a where (_⊓_ : A → A → A) : Set a where
field field
joinSemilattice : IsSemilattice A _≈_ _⊔_ {{joinSemilattice}} : IsSemilattice A _≈_ _⊔_
meetSemilattice : IsSemilattice A _≈_ _⊓_ {{meetSemilattice}} : IsSemilattice A _≈_ _⊓_
absorb-⊔-⊓ : (x y : A) → (x ⊔ (x ⊓ y)) ≈ x absorb-⊔-⊓ : (x y : A) → (x ⊔ (x ⊓ y)) ≈ x
absorb-⊓-⊔ : (x y : A) → (x ⊓ (x ⊔ y)) ≈ x absorb-⊓-⊔ : (x y : A) → (x ⊓ (x ⊔ y)) ≈ x
@ -216,12 +217,12 @@ record IsFiniteHeightLattice {a} (A : Set a)
(_⊓_ : A → A → A) : Set (lsuc a) where (_⊓_ : A → A → A) : Set (lsuc a) where
field field
isLattice : IsLattice A _≈_ _⊔_ _⊓_ {{isLattice}} : IsLattice A _≈_ _⊔_ _⊓_
open IsLattice isLattice public open IsLattice isLattice public
field field
fixedHeight : FixedHeight h {{fixedHeight}} : FixedHeight h
module ChainMapping {a b} {A : Set a} {B : Set b} module ChainMapping {a b} {A : Set a} {B : Set b}
{_≈₁_ : A → A → Set a} {_≈₂_ : B → B → Set b} {_≈₁_ : A → A → Set a} {_≈₂_ : B → B → Set b}
@ -251,7 +252,7 @@ record Semilattice {a} (A : Set a) : Set (lsuc a) where
_≈_ : A → A → Set a _≈_ : A → A → Set a
_⊔_ : A → A → A _⊔_ : A → A → A
isSemilattice : IsSemilattice A _≈_ _⊔_ {{isSemilattice}} : IsSemilattice A _≈_ _⊔_
open IsSemilattice isSemilattice public open IsSemilattice isSemilattice public
@ -262,7 +263,7 @@ record Lattice {a} (A : Set a) : Set (lsuc a) where
_⊔_ : A → A → A _⊔_ : A → A → A
_⊓_ : A → A → A _⊓_ : A → A → A
isLattice : IsLattice A _≈_ _⊔_ _⊓_ {{isLattice}} : IsLattice A _≈_ _⊔_ _⊓_
open IsLattice isLattice public open IsLattice isLattice public
@ -273,6 +274,6 @@ record FiniteHeightLattice {a} (A : Set a) : Set (lsuc a) where
_⊔_ : A → A → A _⊔_ : A → A → A
_⊓_ : A → A → A _⊓_ : A → A → A
isFiniteHeightLattice : IsFiniteHeightLattice A height _≈_ _⊔_ _⊓_ {{isFiniteHeightLattice}} : IsFiniteHeightLattice A height _≈_ _⊔_ _⊓_
open IsFiniteHeightLattice isFiniteHeightLattice public open IsFiniteHeightLattice isFiniteHeightLattice public

120
Lattice/AboveBelow.agda
View File

@ -1,17 +1,19 @@
open import Lattice open import Lattice
open import Equivalence open import Equivalence
open import Relation.Nullary using (Dec; ¬_; yes; no) open import Relation.Nullary using (Dec; ¬_; yes; no)
open import Data.Unit using () renaming (⊤ to ⊤ᵘ)
module Lattice.AboveBelow {a} (A : Set a) module Lattice.AboveBelow {a} (A : Set a)
(_≈₁_ : A → A → Set a) {_≈₁_ : A → A → Set a}
(≈₁-equiv : IsEquivalence A _≈₁_) {{≈₁-equiv : IsEquivalence A _≈₁_}}
(≈₁-dec : IsDecidable _≈₁_) where {{≈₁-Decidable : IsDecidable _≈₁_}} (dummy : ⊤ᵘ) where
open import Data.Empty using (⊥-elim) open import Data.Empty using (⊥-elim)
open import Data.Product using (_,_) open import Data.Product using (_,_)
open import Data.Nat using (_≤_; ℕ; z≤n; s≤s; suc) open import Data.Nat using (_≤_; ℕ; z≤n; s≤s; suc)
open import Function using (_∘_) open import Function using (_∘_)
open import Showable using (Showable; show) open import Showable using (Showable; show)
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Binary.PropositionalEquality as Eq open import Relation.Binary.PropositionalEquality as Eq
using (_≡_; sym; subst; refl) using (_≡_; sym; subst; refl)
@ -20,6 +22,8 @@ import Chain
open IsEquivalence ≈₁-equiv using () open IsEquivalence ≈₁-equiv using ()
renaming (≈-refl to ≈₁-refl; ≈-sym to ≈₁-sym; ≈-trans to ≈₁-trans) renaming (≈-refl to ≈₁-refl; ≈-sym to ≈₁-sym; ≈-trans to ≈₁-trans)
open IsDecidable ≈₁-Decidable using () renaming (R-dec to ≈₁-dec)
data AboveBelow : Set a where data AboveBelow : Set a where
⊥ : AboveBelow ⊥ : AboveBelow
⊤ : AboveBelow ⊤ : AboveBelow
@ -62,7 +66,7 @@ data _≈_ : AboveBelow → AboveBelow → Set a where
; ≈-trans = ≈-trans ; ≈-trans = ≈-trans
} }
≈-dec : IsDecidable _≈_ ≈-dec : Decidable _≈_
≈-dec ⊥ ⊥ = yes ≈-⊥-⊥ ≈-dec ⊥ ⊥ = yes ≈-⊥-⊥
≈-dec ⊤ ⊤ = yes ≈-⊤-⊤ ≈-dec ⊤ ⊤ = yes ≈-⊤-⊤
≈-dec [ x ] [ y ] ≈-dec [ x ] [ y ]
@ -76,6 +80,10 @@ data _≈_ : AboveBelow → AboveBelow → Set a where
≈-dec [ x ] ⊥ = no λ () ≈-dec [ x ] ⊥ = no λ ()
≈-dec [ x ] ⊤ = no λ () ≈-dec [ x ] ⊤ = no λ ()
instance
≈-Decidable : IsDecidable _≈_
≈-Decidable = record { R-dec = ≈-dec }
-- Any object can be wrapped in an 'above below' to make it a lattice, -- Any object can be wrapped in an 'above below' to make it a lattice,
-- since ⊤ and ⊥ are the largest and least elements, and the rest are left -- since ⊤ and ⊥ are the largest and least elements, and the rest are left
-- unordered. That's what this module does. -- unordered. That's what this module does.
@ -169,14 +177,15 @@ module Plain (x : A) where
⊔-idemp ⊥ = ≈-⊥-⊥ ⊔-idemp ⊥ = ≈-⊥-⊥
⊔-idemp [ x ] rewrite x≈y⇒[x]⊔[y]≡[x] (≈₁-refl {x}) = ≈-refl ⊔-idemp [ x ] rewrite x≈y⇒[x]⊔[y]≡[x] (≈₁-refl {x}) = ≈-refl
isJoinSemilattice : IsSemilattice AboveBelow _≈_ _⊔_ instance
isJoinSemilattice = record isJoinSemilattice : IsSemilattice AboveBelow _≈_ _⊔_
{ ≈-equiv = ≈-equiv isJoinSemilattice = record
; ≈-⊔-cong = ≈-⊔-cong { ≈-equiv = ≈-equiv
; ⊔-assoc = ⊔-assoc ; ≈-⊔-cong = ≈-⊔-cong
; ⊔-comm = ⊔-comm ; ⊔-assoc = ⊔-assoc
; ⊔-idemp = ⊔-idemp ; ⊔-comm = ⊔-comm
} ; ⊔-idemp = ⊔-idemp
}
_⊓_ : AboveBelow → AboveBelow → AboveBelow _⊓_ : AboveBelow → AboveBelow → AboveBelow
⊥ ⊓ x = ⊥ ⊥ ⊓ x = ⊥
@ -262,14 +271,15 @@ module Plain (x : A) where
⊓-idemp ⊤ = ≈-⊤-⊤ ⊓-idemp ⊤ = ≈-⊤-⊤
⊓-idemp [ x ] rewrite x≈y⇒[x]⊓[y]≡[x] (≈₁-refl {x}) = ≈-refl ⊓-idemp [ x ] rewrite x≈y⇒[x]⊓[y]≡[x] (≈₁-refl {x}) = ≈-refl
isMeetSemilattice : IsSemilattice AboveBelow _≈_ _⊓_ instance
isMeetSemilattice = record isMeetSemilattice : IsSemilattice AboveBelow _≈_ _⊓_
{ ≈-equiv = ≈-equiv isMeetSemilattice = record
; ≈-⊔-cong = ≈-⊓-cong { ≈-equiv = ≈-equiv
; ⊔-assoc = ⊓-assoc ; ≈-⊔-cong = ≈-⊓-cong
; ⊔-comm = ⊓-comm ; ⊔-assoc = ⊓-assoc
; ⊔-idemp = ⊓-idemp ; ⊔-comm = ⊓-comm
} ; ⊔-idemp = ⊓-idemp
}
absorb-⊔-⊓ : ∀ (ab₁ ab₂ : AboveBelow) → (ab₁ ⊔ (ab₁ ⊓ ab₂)) ≈ ab₁ absorb-⊔-⊓ : ∀ (ab₁ ab₂ : AboveBelow) → (ab₁ ⊔ (ab₁ ⊓ ab₂)) ≈ ab₁
absorb-⊔-⊓ ⊥ ab₂ rewrite ⊥⊓x≡⊥ ab₂ = ≈-⊥-⊥ absorb-⊔-⊓ ⊥ ab₂ rewrite ⊥⊓x≡⊥ ab₂ = ≈-⊥-⊥
@ -294,21 +304,22 @@ module Plain (x : A) where
... | no x̷≈y rewrite x̷≈y⇒[x]⊔[y]≡⊤ x̷≈y rewrite x⊓⊤≡x [ x ] = ≈-refl ... | no x̷≈y rewrite x̷≈y⇒[x]⊔[y]≡⊤ x̷≈y rewrite x⊓⊤≡x [ x ] = ≈-refl
isLattice : IsLattice AboveBelow _≈_ _⊔_ _⊓_ instance
isLattice = record isLattice : IsLattice AboveBelow _≈_ _⊔_ _⊓_
{ joinSemilattice = isJoinSemilattice isLattice = record
; meetSemilattice = isMeetSemilattice { joinSemilattice = isJoinSemilattice
; absorb-⊔-⊓ = absorb-⊔-⊓ ; meetSemilattice = isMeetSemilattice
; absorb-⊓-⊔ = absorb-⊓-⊔ ; absorb-⊔-⊓ = absorb-⊔-⊓
} ; absorb-⊓-⊔ = absorb-⊓-⊔
}
lattice : Lattice AboveBelow lattice : Lattice AboveBelow
lattice = record lattice = record
{ _≈_ = _≈_ { _≈_ = _≈_
; _⊔_ = _⊔_ ; _⊔_ = _⊔_
; _⊓_ = _⊓_ ; _⊓_ = _⊓_
; isLattice = isLattice ; isLattice = isLattice
} }
open IsLattice isLattice using (_≼_; _≺_; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public open IsLattice isLattice using (_≼_; _≺_; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public
@ -354,25 +365,26 @@ module Plain (x : A) where
isLongest {⊥} (step {_} {[ x ]} _ (≈-lift _) (step [x]≺y y≈z c@(step _ _ _))) isLongest {⊥} (step {_} {[ x ]} _ (≈-lift _) (step [x]≺y y≈z c@(step _ _ _)))
rewrite [x]≺y⇒y≡⊤ _ _ [x]≺y with ≈-⊤-⊤ ← y≈z = ⊥-elim (¬-Chain-⊤ c) rewrite [x]≺y⇒y≡⊤ _ _ [x]≺y with ≈-⊤-⊤ ← y≈z = ⊥-elim (¬-Chain-⊤ c)
fixedHeight : IsLattice.FixedHeight isLattice 2 instance
fixedHeight = record fixedHeight : IsLattice.FixedHeight isLattice 2
{ ⊥ = ⊥ fixedHeight = record
; ⊤ = ⊤ { ⊥ = ⊥
; longestChain = longestChain ; ⊤ = ⊤
; bounded = isLongest ; longestChain = longestChain
} ; bounded = isLongest
}
isFiniteHeightLattice : IsFiniteHeightLattice AboveBelow 2 _≈_ _⊔_ _⊓_ isFiniteHeightLattice : IsFiniteHeightLattice AboveBelow 2 _≈_ _⊔_ _⊓_
isFiniteHeightLattice = record isFiniteHeightLattice = record
{ isLattice = isLattice { isLattice = isLattice
; fixedHeight = fixedHeight ; fixedHeight = fixedHeight
} }
finiteHeightLattice : FiniteHeightLattice AboveBelow finiteHeightLattice : FiniteHeightLattice AboveBelow
finiteHeightLattice = record finiteHeightLattice = record
{ height = 2 { height = 2
; _≈_ = _≈_ ; _≈_ = _≈_
; _⊔_ = _⊔_ ; _⊔_ = _⊔_
; _⊓_ = _⊓_ ; _⊓_ = _⊓_
; isFiniteHeightLattice = isFiniteHeightLattice ; isFiniteHeightLattice = isFiniteHeightLattice
} }

119
Lattice/FiniteMap.agda
View File

@ -3,15 +3,16 @@ open import Relation.Binary.PropositionalEquality as Eq
using (_≡_;refl; sym; trans; cong; subst) using (_≡_;refl; sym; trans; cong; subst)
open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_) open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
open import Data.List using (List; _∷_; []) open import Data.List using (List; _∷_; [])
open import Data.Unit using (⊤)
module Lattice.FiniteMap {A : Set} {B : Set} module Lattice.FiniteMap (A : Set) (B : Set)
{_≈₂_ : B → B → Set} {_≈₂_ : B → B → Set}
{_⊔₂_ : B → B → B} {_⊓₂_ : B → B → B} {_⊔₂_ : B → B → B} {_⊓₂_ : B → B → B}
(≡-dec-A : IsDecidable (_≡_ {_} {A})) {{≡-Decidable-A : IsDecidable {_} {A} _≡_}}
(lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where {{lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_}} (dummy : ⊤) where
open IsLattice lB using () renaming (_≼_ to _≼₂_) open IsLattice lB using () renaming (_≼_ to _≼₂_)
open import Lattice.Map ≡-dec-A lB as Map open import Lattice.Map A B dummy as Map
using using
( Map ( Map
; ⊔-equal-keys ; ⊔-equal-keys
@ -39,7 +40,7 @@ open import Lattice.Map ≡-dec-A lB as Map
; ⊓-idemp to ⊓ᵐ-idemp ; ⊓-idemp to ⊓ᵐ-idemp
; absorb-⊔-⊓ to absorb-⊔ᵐ-⊓ᵐ ; absorb-⊔-⊓ to absorb-⊔ᵐ-⊓ᵐ
; absorb-⊓-⊔ to absorb-⊓ᵐ-⊔ᵐ ; absorb-⊓-⊔ to absorb-⊓ᵐ-⊔ᵐ
; ≈-dec to ≈ᵐ-dec ; ≈-Decidable to ≈ᵐ-Decidable
; _[_] to _[_]ᵐ ; _[_] to _[_]ᵐ
; []-∈ to []ᵐ-∈ ; []-∈ to []ᵐ-∈
; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ ; m₁≼m₂⇒m₁[k]≼m₂[k] to m₁≼m₂⇒m₁[k]ᵐ≼m₂[k]ᵐ
@ -67,7 +68,6 @@ open import Data.Nat using (ℕ)
open import Data.Product using (_×_; _,_; Σ; proj₁; proj₂) open import Data.Product using (_×_; _,_; Σ; proj₁; proj₂)
open import Equivalence open import Equivalence
open import Function using (_∘_) open import Function using (_∘_)
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Nullary using (¬_; Dec; yes; no) open import Relation.Nullary using (¬_; Dec; yes; no)
open import Utils using (Pairwise; _∷_; []; Unique; push; empty; All¬-¬Any) open import Utils using (Pairwise; _∷_; []; Unique; push; empty; All¬-¬Any)
open import Showable using (Showable; show) open import Showable using (Showable; show)
@ -86,8 +86,12 @@ module WithKeys (ks : List A) where
_≈_ : FiniteMap → FiniteMap → Set _≈_ : FiniteMap → FiniteMap → Set
_≈_ (m₁ , _) (m₂ , _) = m₁ ≈ᵐ m₂ _≈_ (m₁ , _) (m₂ , _) = m₁ ≈ᵐ m₂
≈₂-dec⇒≈-dec : IsDecidable _≈₂_ → IsDecidable _≈_ instance
≈₂-dec⇒≈-dec ≈₂-dec fm₁ fm₂ = ≈ᵐ-dec ≈₂-dec (proj₁ fm₁) (proj₁ fm₂) ≈-Decidable : {{ IsDecidable _≈₂_ }} → IsDecidable _≈_
≈-Decidable {{≈₂-Decidable}} = record
{ R-dec = λ fm₁ fm₂ → IsDecidable.R-dec (≈ᵐ-Decidable {{≈₂-Decidable}})
(proj₁ fm₁) (proj₁ fm₂)
}
_⊔_ : FiniteMap → FiniteMap → FiniteMap _⊔_ : FiniteMap → FiniteMap → FiniteMap
_⊔_ (m₁ , km₁≡ks) (m₂ , km₂≡ks) = _⊔_ (m₁ , km₁≡ks) (m₂ , km₂≡ks) =
@ -140,46 +144,47 @@ module WithKeys (ks : List A) where
IsEquivalence.≈-trans ≈ᵐ-equiv {m₁} {m₂} {m₃} IsEquivalence.≈-trans ≈ᵐ-equiv {m₁} {m₂} {m₃}
} }
isUnionSemilattice : IsSemilattice FiniteMap _≈_ _⊔_ instance
isUnionSemilattice = record isUnionSemilattice : IsSemilattice FiniteMap _≈_ _⊔_
{ ≈-equiv = ≈-equiv isUnionSemilattice = record
; ≈-⊔-cong = { ≈-equiv = ≈-equiv
λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} {(m₄ , _)} m₁≈m₂ m₃≈m₄ → ; ≈-⊔-cong =
≈ᵐ-⊔ᵐ-cong {m₁} {m₂} {m₃} {m₄} m₁≈m₂ m₃≈m₄ λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} {(m₄ , _)} m₁≈m₂ m₃≈m₄ →
; ⊔-assoc = λ (m₁ , _) (m₂ , _) (m₃ , _) → ⊔ᵐ-assoc m₁ m₂ m₃ ≈ᵐ-⊔ᵐ-cong {m₁} {m₂} {m₃} {m₄} m₁≈m₂ m₃≈m₄
; ⊔-comm = λ (m₁ , _) (m₂ , _) → ⊔ᵐ-comm m₁ m₂ ; ⊔-assoc = λ (m₁ , _) (m₂ , _) (m₃ , _) → ⊔ᵐ-assoc m₁ m₂ m₃
; ⊔-idemp = λ (m , _) → ⊔ᵐ-idemp m ; ⊔-comm = λ (m₁ , _) (m₂ , _) → ⊔ᵐ-comm m₁ m₂
} ; ⊔-idemp = λ (m , _) → ⊔ᵐ-idemp m
}
isIntersectSemilattice : IsSemilattice FiniteMap _≈_ _⊓_ isIntersectSemilattice : IsSemilattice FiniteMap _≈_ _⊓_
isIntersectSemilattice = record isIntersectSemilattice = record
{ ≈-equiv = ≈-equiv { ≈-equiv = ≈-equiv
; ≈-⊔-cong = ; ≈-⊔-cong =
λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} {(m₄ , _)} m₁≈m₂ m₃≈m₄ → λ {(m₁ , _)} {(m₂ , _)} {(m₃ , _)} {(m₄ , _)} m₁≈m₂ m₃≈m₄ →
≈ᵐ-⊓ᵐ-cong {m₁} {m₂} {m₃} {m₄} m₁≈m₂ m₃≈m₄ ≈ᵐ-⊓ᵐ-cong {m₁} {m₂} {m₃} {m₄} m₁≈m₂ m₃≈m₄
; ⊔-assoc = λ (m₁ , _) (m₂ , _) (m₃ , _) → ⊓ᵐ-assoc m₁ m₂ m₃ ; ⊔-assoc = λ (m₁ , _) (m₂ , _) (m₃ , _) → ⊓ᵐ-assoc m₁ m₂ m₃
; ⊔-comm = λ (m₁ , _) (m₂ , _) → ⊓ᵐ-comm m₁ m₂ ; ⊔-comm = λ (m₁ , _) (m₂ , _) → ⊓ᵐ-comm m₁ m₂
; ⊔-idemp = λ (m , _) → ⊓ᵐ-idemp m ; ⊔-idemp = λ (m , _) → ⊓ᵐ-idemp m
} }
isLattice : IsLattice FiniteMap _≈_ _⊔_ _⊓_ isLattice : IsLattice FiniteMap _≈_ _⊔_ _⊓_
isLattice = record isLattice = record
{ joinSemilattice = isUnionSemilattice { joinSemilattice = isUnionSemilattice
; meetSemilattice = isIntersectSemilattice ; meetSemilattice = isIntersectSemilattice
; absorb-⊔-⊓ = λ (m₁ , _) (m₂ , _) → absorb-⊔ᵐ-⊓ᵐ m₁ m₂ ; absorb-⊔-⊓ = λ (m₁ , _) (m₂ , _) → absorb-⊔ᵐ-⊓ᵐ m₁ m₂
; absorb-⊓-⊔ = λ (m₁ , _) (m₂ , _) → absorb-⊓ᵐ-⊔ᵐ m₁ m₂ ; absorb-⊓-⊔ = λ (m₁ , _) (m₂ , _) → absorb-⊓ᵐ-⊔ᵐ m₁ m₂
} }
lattice : Lattice FiniteMap
lattice = record
{ _≈_ = _≈_
; _⊔_ = _⊔_
; _⊓_ = _⊓_
; isLattice = isLattice
}
open IsLattice isLattice using (_≼_; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public open IsLattice isLattice using (_≼_; ⊔-Monotonicˡ; ⊔-Monotonicʳ) public
lattice : Lattice FiniteMap
lattice = record
{ _≈_ = _≈_
; _⊔_ = _⊔_
; _⊓_ = _⊓_
; isLattice = isLattice
}
m₁≼m₂⇒m₁[k]≼m₂[k] : ∀ (fm₁ fm₂ : FiniteMap) {k : A} {v₁ v₂ : B} → m₁≼m₂⇒m₁[k]≼m₂[k] : ∀ (fm₁ fm₂ : FiniteMap) {k : A} {v₁ v₂ : B} →
fm₁ ≼ fm₂ → (k , v₁) ∈ fm₁ → (k , v₂) ∈ fm₂ → v₁ ≼₂ v₂ 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₂⇒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₂
@ -192,7 +197,7 @@ module WithKeys (ks : List A) where
module GeneralizedUpdate module GeneralizedUpdate
{l} {L : Set l} {l} {L : Set l}
{_≈ˡ_ : L → L → Set l} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L} {_≈ˡ_ : L → L → Set l} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
(lL : IsLattice L _≈ˡ_ _⊔ˡ_ _⊓ˡ_) {{lL : IsLattice L _≈ˡ_ _⊔ˡ_ _⊓ˡ_}}
(f : L → FiniteMap) (f-Monotonic : Monotonic (IsLattice._≼_ lL) _≼_ f) (f : L → FiniteMap) (f-Monotonic : Monotonic (IsLattice._≼_ lL) _≼_ f)
(g : A → L → B) (g-Monotonicʳ : ∀ k → Monotonic (IsLattice._≼_ lL) _≼₂_ (g k)) (g : A → L → B) (g-Monotonicʳ : ∀ k → Monotonic (IsLattice._≼_ lL) _≼₂_ (g k))
(ks : List A) where (ks : List A) where
@ -206,7 +211,7 @@ module WithKeys (ks : List A) where
f' l = (f l) updating ks via (updater l) f' l = (f l) updating ks via (updater l)
f'-Monotonic : Monotonic _≼ˡ_ _≼_ f' f'-Monotonic : Monotonic _≼ˡ_ _≼_ f'
f'-Monotonic {l₁} {l₂} l₁≼l₂ = f'-Monotonicᵐ lL (proj₁ ∘ f) f-Monotonic g g-Monotonicʳ ks l₁≼l₂ f'-Monotonic {l₁} {l₂} l₁≼l₂ = f'-Monotonicᵐ (proj₁ ∘ f) f-Monotonic g g-Monotonicʳ ks l₁≼l₂
f'-∈k-forward : ∀ {k l} → k ∈k (f l) → k ∈k (f' l) f'-∈k-forward : ∀ {k l} → k ∈k (f l) → k ∈k (f' l)
f'-∈k-forward {k} {l} = updatingᵐ-via-∈k-forward (proj₁ (f l)) ks (updater l) f'-∈k-forward {k} {l} = updatingᵐ-via-∈k-forward (proj₁ (f l)) ks (updater l)
@ -251,18 +256,18 @@ module WithKeys (ks : List A) where
open WithKeys public open WithKeys public
module IterProdIsomorphism where module IterProdIsomorphism where
open import Data.Unit using (⊤; tt) open import Data.Unit using (tt)
open import Lattice.Unit using () open import Lattice.Unit using ()
renaming renaming
( _≈_ to _≈ᵘ_ ( _≈_ to _≈ᵘ_
; _⊔_ to _⊔ᵘ_ ; _⊔_ to _⊔ᵘ_
; _⊓_ to _⊓ᵘ_ ; _⊓_ to _⊓ᵘ_
; ≈-dec to ≈ᵘ-dec ; ≈-Decidable to ≈ᵘ-Decidable
; isLattice to isLatticeᵘ ; isLattice to isLatticeᵘ
; ≈-equiv to ≈ᵘ-equiv ; ≈-equiv to ≈ᵘ-equiv
; fixedHeight to fixedHeightᵘ ; fixedHeight to fixedHeightᵘ
) )
open import Lattice.IterProd _≈₂_ _≈ᵘ_ _⊔₂_ _⊔ᵘ_ _⊓₂_ _⊓ᵘ_ lB isLatticeᵘ open import Lattice.IterProd B ⊤ dummy
as IP as IP
using (IterProd) using (IterProd)
open IsLattice lB using () open IsLattice lB using ()
@ -297,11 +302,11 @@ module IterProdIsomorphism where
_⊆ᵐ_ fm₁ fm₂ = subset-impl (proj₁ (proj₁ fm₁)) (proj₁ (proj₁ fm₂)) _⊆ᵐ_ fm₁ fm₂ = subset-impl (proj₁ (proj₁ fm₁)) (proj₁ (proj₁ fm₂))
_≈ⁱᵖ_ : ∀ {n : ℕ} → IterProd n → IterProd n → Set _≈ⁱᵖ_ : ∀ {n : ℕ} → IterProd n → IterProd n → Set
_≈ⁱᵖ_ {n} = IP._≈_ n _≈ⁱᵖ_ {n} = IP._≈_ {n}
_⊔ⁱᵖ_ : ∀ {ks : List A} → _⊔ⁱᵖ_ : ∀ {ks : List A} →
IterProd (length ks) → IterProd (length ks) → IterProd (length ks) IterProd (length ks) → IterProd (length ks) → IterProd (length ks)
_⊔ⁱᵖ_ {ks} = IP._⊔_ (length ks) _⊔ⁱᵖ_ {ks} = IP._⊔_ {length ks}
_∈ᵐ_ : ∀ {ks : List A} → A × B → FiniteMap ks → Set _∈ᵐ_ : ∀ {ks : List A} → A × B → FiniteMap ks → Set
_∈ᵐ_ {ks} = _∈_ ks _∈ᵐ_ {ks} = _∈_ ks
@ -318,7 +323,7 @@ module IterProdIsomorphism where
from-to-inverseˡ : ∀ {ks : List A} (uks : Unique ks) → from-to-inverseˡ : ∀ {ks : List A} (uks : Unique ks) →
IsInverseˡ (_≈_ ks) (_≈ⁱᵖ_ {length ks}) IsInverseˡ (_≈_ ks) (_≈ⁱᵖ_ {length ks})
(from {ks}) (to {ks} uks) (from {ks}) (to {ks} uks)
from-to-inverseˡ {[]} _ _ = IsEquivalence.≈-refl (IP.≈-equiv 0) from-to-inverseˡ {[]} _ _ = IsEquivalence.≈-refl (IP.≈-equiv {0})
from-to-inverseˡ {k ∷ ks'} (push k≢ks' uks') (v , rest) from-to-inverseˡ {k ∷ ks'} (push k≢ks' uks') (v , rest)
with ((fm' , ufm') , refl) ← to uks' rest in p rewrite sym p = with ((fm' , ufm') , refl) ← to uks' rest in p rewrite sym p =
(IsLattice.≈-refl lB , from-to-inverseˡ {ks'} uks' rest) (IsLattice.≈-refl lB , from-to-inverseˡ {ks'} uks' rest)
@ -520,7 +525,7 @@ module IterProdIsomorphism where
fm₂⊆fm₁ : to uks ip₂ ⊆ᵐ to uks ip₁ fm₂⊆fm₁ : to uks ip₂ ⊆ᵐ to uks ip₁
fm₂⊆fm₁ = inductive-step (≈₂-sym v₁≈v₂) fm₂⊆fm₁ = inductive-step (≈₂-sym v₁≈v₂)
(IP.≈-sym (length ks') rest₁≈rest₂) (IP.≈-sym {length ks'} rest₁≈rest₂)
from-⊔-distr : ∀ {ks : List A} → (fm₁ fm₂ : FiniteMap ks) → from-⊔-distr : ∀ {ks : List A} → (fm₁ fm₂ : FiniteMap ks) →
_≈ⁱᵖ_ {length ks} (from (_⊔_ _ fm₁ fm₂)) _≈ⁱᵖ_ {length ks} (from (_⊔_ _ fm₁ fm₂))
@ -543,7 +548,7 @@ module IterProdIsomorphism where
rewrite from-rest (_⊔_ _ fm₁ fm₂) rewrite from-rest fm₁ rewrite from-rest fm₂ rewrite from-rest (_⊔_ _ fm₁ fm₂) rewrite from-rest fm₁ rewrite from-rest fm₂
= ( IsLattice.≈-refl lB = ( IsLattice.≈-refl lB
, IsEquivalence.≈-trans , IsEquivalence.≈-trans
(IP.≈-equiv (length ks)) (IP.≈-equiv {length ks})
(from-preserves-≈ {_} {pop (_⊔_ _ fm₁ fm₂)} (from-preserves-≈ {_} {pop (_⊔_ _ fm₁ fm₂)}
{_⊔_ _ (pop fm₁) (pop fm₂)} {_⊔_ _ (pop fm₁) (pop fm₂)}
(pop-⊔-distr fm₁ fm₂)) (pop-⊔-distr fm₁ fm₂))
@ -608,15 +613,15 @@ module IterProdIsomorphism where
in in
(v' , (v₁⊔v₂≈v' , there v'∈fm')) (v' , (v₁⊔v₂≈v' , there v'∈fm'))
module WithUniqueKeysAndFixedHeight {ks : List A} (uks : Unique ks) (≈₂-dec : Decidable _≈₂_) (h₂ : ℕ) (fhB : FixedHeight₂ h₂) where module WithUniqueKeysAndFixedHeight {ks : List A} (uks : Unique ks) {{≈₂-Decidable : IsDecidable _≈₂_}} {h₂ : ℕ} {{fhB : FixedHeight₂ h₂}} where
import Isomorphism import Isomorphism
open Isomorphism.TransportFiniteHeight open Isomorphism.TransportFiniteHeight
(IP.isFiniteHeightLattice (length ks) ≈₂-dec ≈ᵘ-dec h₂ 0 fhB fixedHeightᵘ) (isLattice ks) (IP.isFiniteHeightLattice {k = length ks} {{fhB = fixedHeightᵘ}}) (isLattice ks)
{f = to uks} {g = from {ks}} {f = to uks} {g = from {ks}}
(to-preserves-≈ uks) (from-preserves-≈ {ks}) (to-preserves-≈ uks) (from-preserves-≈ {ks})
(to-⊔-distr uks) (from-⊔-distr {ks}) (to-⊔-distr uks) (from-⊔-distr {ks})
(from-to-inverseʳ uks) (from-to-inverseˡ uks) (from-to-inverseʳ uks) (from-to-inverseˡ uks)
using (isFiniteHeightLattice; finiteHeightLattice) public using (isFiniteHeightLattice; finiteHeightLattice; fixedHeight) public
-- Helpful lemma: all entries of the 'bottom' map are assigned to bottom. -- Helpful lemma: all entries of the 'bottom' map are assigned to bottom.
@ -624,5 +629,5 @@ module IterProdIsomorphism where
⊥-contains-bottoms : ∀ {k : A} {v : B} → (k , v) ∈ᵐ ⊥ → v ≡ (Height.⊥ fhB) ⊥-contains-bottoms : ∀ {k : A} {v : B} → (k , v) ∈ᵐ ⊥ → v ≡ (Height.⊥ fhB)
⊥-contains-bottoms {k} {v} k,v∈⊥ ⊥-contains-bottoms {k} {v} k,v∈⊥
rewrite IP.⊥-built (length ks) ≈₂-dec ≈ᵘ-dec h₂ 0 fhB fixedHeightᵘ = rewrite IP.⊥-built {length ks} {{fhB = fixedHeightᵘ}} =
to-build uks k v k,v∈⊥ to-build uks k v k,v∈⊥

121
Lattice/IterProd.agda
View File

@ -1,14 +1,15 @@
open import Lattice open import Lattice
open import Data.Unit using (⊤)
-- Due to universe levels, it becomes relatively annoying to handle the case -- Due to universe levels, it becomes relatively annoying to handle the case
-- where the levels of A and B are not the same. For the time being, constrain -- where the levels of A and B are not the same. For the time being, constrain
-- them to be the same. -- them to be the same.
module Lattice.IterProd {a} {A B : Set a} module Lattice.IterProd {a} (A B : Set a)
(_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a) {_≈₁_ : A → A → Set a} {_≈₂_ : B → B → Set a}
(_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B) {_⊔₁_ : A → A → A} {_⊔₂_ : B → B → B}
(_⊓₁_ : A → A → A) (_⊓₂_ : B → B → B) {_⊓₁_ : A → A → A} {_⊓₂_ : B → B → B}
(lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where {{lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_}} {{lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_}} (dummy : ⊤) where
open import Agda.Primitive using (lsuc) open import Agda.Primitive using (lsuc)
open import Data.Nat using (ℕ; zero; suc; _+_) open import Data.Nat using (ℕ; zero; suc; _+_)
@ -39,11 +40,11 @@ build a b (suc s) = (a , build a b s)
private private
record RequiredForFixedHeight : Set (lsuc a) where record RequiredForFixedHeight : Set (lsuc a) where
field field
≈₁-dec : IsDecidable _≈₁_ {{≈₁-Decidable}} : IsDecidable _≈₁_
≈₂-dec : IsDecidable _≈₂_ {{≈₂-Decidable}} : IsDecidable _≈₂_
h₁ h₂ : ℕ h₁ h₂ : ℕ
fhA : FixedHeight₁ h₁ {{fhA}} : FixedHeight₁ h₁
fhB : FixedHeight₂ h₂ {{fhB}} : FixedHeight₂ h₂
⊥₁ : A ⊥₁ : A
⊥₁ = Height.⊥ fhA ⊥₁ = Height.⊥ fhA
@ -58,7 +59,7 @@ private
field field
height : ℕ height : ℕ
fixedHeight : IsLattice.FixedHeight isLattice height fixedHeight : IsLattice.FixedHeight isLattice height
≈-dec : IsDecidable _≈_ ≈-Decidable : IsDecidable _≈_
⊥-correct : Height.⊥ fixedHeight ≡ ⊥ ⊥-correct : Height.⊥ fixedHeight ≡ ⊥
@ -84,7 +85,7 @@ private
; isFiniteHeightIfSupported = λ req → record ; isFiniteHeightIfSupported = λ req → record
{ height = RequiredForFixedHeight.h₂ req { height = RequiredForFixedHeight.h₂ req
; fixedHeight = RequiredForFixedHeight.fhB req ; fixedHeight = RequiredForFixedHeight.fhB req
; ≈-dec = RequiredForFixedHeight.≈₂-dec req ; ≈-Decidable = RequiredForFixedHeight.≈₂-Decidable req
; ⊥-correct = refl ; ⊥-correct = refl
} }
} }
@ -101,10 +102,9 @@ private
{ height = (RequiredForFixedHeight.h₁ req) + IsFiniteHeightWithBotAndDecEq.height fhlRest { height = (RequiredForFixedHeight.h₁ req) + IsFiniteHeightWithBotAndDecEq.height fhlRest
; fixedHeight = ; fixedHeight =
P.fixedHeight P.fixedHeight
(RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightWithBotAndDecEq.≈-dec fhlRest) {{≈₂-Decidable = IsFiniteHeightWithBotAndDecEq.≈-Decidable fhlRest}}
(RequiredForFixedHeight.h₁ req) (IsFiniteHeightWithBotAndDecEq.height fhlRest) {{fhB = IsFiniteHeightWithBotAndDecEq.fixedHeight fhlRest}}
(RequiredForFixedHeight.fhA req) (IsFiniteHeightWithBotAndDecEq.fixedHeight fhlRest) ; ≈-Decidable = P.≈-Decidable {{≈₂-Decidable = IsFiniteHeightWithBotAndDecEq.≈-Decidable fhlRest}}
; ≈-dec = P.≈-dec (RequiredForFixedHeight.≈₁-dec req) (IsFiniteHeightWithBotAndDecEq.≈-dec fhlRest)
; ⊥-correct = ; ⊥-correct =
cong ((Height.⊥ (RequiredForFixedHeight.fhA req)) ,_) cong ((Height.⊥ (RequiredForFixedHeight.fhA req)) ,_)
(IsFiniteHeightWithBotAndDecEq.⊥-correct fhlRest) (IsFiniteHeightWithBotAndDecEq.⊥-correct fhlRest)
@ -112,56 +112,57 @@ private
} }
where where
everythingRest = everything k' everythingRest = everything k'
import Lattice.Prod A (IterProd k') {{lB = Everything.isLattice everythingRest}} as P
import Lattice.Prod module _ {k : ℕ} where
_≈₁_ (Everything._≈_ everythingRest) open Everything (everything k) using (_≈_; _⊔_; _⊓_) public
_⊔₁_ (Everything._⊔_ everythingRest) open Lattice.IsLattice (Everything.isLattice (everything k)) public
_⊓₁_ (Everything._⊓_ everythingRest)
lA (Everything.isLattice everythingRest) as P
module _ (k : ℕ) where instance
open Everything (everything k) using (_≈_; _⊔_; _⊓_; isLattice) public isLattice = Everything.isLattice (everything k)
open Lattice.IsLattice isLattice public
lattice : Lattice (IterProd k) lattice : Lattice (IterProd k)
lattice = record lattice = record
{ _≈_ = _≈_ { _≈_ = _≈_
; _⊔_ = _⊔_
; _⊓_ = _⊓_
; isLattice = isLattice
}
module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
(h₁ h₂ : ℕ)
(fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where
private
required : RequiredForFixedHeight
required = record
{ ≈₁-dec = ≈₁-dec
; ≈₂-dec = ≈₂-dec
; h₁ = h₁
; h₂ = h₂
; fhA = fhA
; fhB = fhB
}
fixedHeight = IsFiniteHeightWithBotAndDecEq.fixedHeight (Everything.isFiniteHeightIfSupported (everything k) required)
isFiniteHeightLattice = record
{ isLattice = isLattice
; fixedHeight = fixedHeight
}
finiteHeightLattice : FiniteHeightLattice (IterProd k)
finiteHeightLattice = record
{ height = IsFiniteHeightWithBotAndDecEq.height (Everything.isFiniteHeightIfSupported (everything k) required)
; _≈_ = _≈_
; _⊔_ = _⊔_ ; _⊔_ = _⊔_
; _⊓_ = _⊓_ ; _⊓_ = _⊓_
; isFiniteHeightLattice = isFiniteHeightLattice ; isLattice = isLattice
} }
⊥-built : Height.⊥ fixedHeight ≡ (build (Height.⊥ fhA) (Height.⊥ fhB) k) module _ {{≈₁-Decidable : IsDecidable _≈₁_}} {{≈₂-Decidable : IsDecidable _≈₂_}}
⊥-built = IsFiniteHeightWithBotAndDecEq.⊥-correct (Everything.isFiniteHeightIfSupported (everything k) required) {h₁ h₂ : ℕ}
{{fhA : FixedHeight₁ h₁}} {{fhB : FixedHeight₂ h₂}} where
private
isFiniteHeightWithBotAndDecEq =
Everything.isFiniteHeightIfSupported (everything k)
record
{ ≈₁-Decidable = ≈₁-Decidable
; ≈₂-Decidable = ≈₂-Decidable
; h₁ = h₁
; h₂ = h₂
; fhA = fhA
; fhB = fhB
}
open IsFiniteHeightWithBotAndDecEq isFiniteHeightWithBotAndDecEq using (height; ⊥-correct)
instance
fixedHeight = IsFiniteHeightWithBotAndDecEq.fixedHeight isFiniteHeightWithBotAndDecEq
isFiniteHeightLattice = record
{ isLattice = isLattice
; fixedHeight = fixedHeight
}
finiteHeightLattice : FiniteHeightLattice (IterProd k)
finiteHeightLattice = record
{ height = height
; _≈_ = _≈_
; _⊔_ = _⊔_
; _⊓_ = _⊓_
; isFiniteHeightLattice = isFiniteHeightLattice
}
⊥-built : Height.⊥ fixedHeight ≡ (build (Height.⊥ fhA) (Height.⊥ fhB) k)
⊥-built = ⊥-correct

69
Lattice/Map.agda
View File

@ -1,13 +1,14 @@
open import Lattice open import Lattice
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
open import Relation.Binary.Definitions using (Decidable)
open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_) open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
open import Data.Unit using (⊤)
module Lattice.Map {a b : Level} {A : Set a} {B : Set b} module Lattice.Map {a b : Level} (A : Set a) (B : Set b)
{_≈₂_ : B → B → Set b} {_≈₂_ : B → B → Set b}
{_⊔₂_ : B → B → B} {_⊓₂_ : B → B → B} {_⊔₂_ : B → B → B} {_⊓₂_ : B → B → B}
(≡-dec-A : Decidable (_≡_ {a} {A})) {{≡-Decidable-A : IsDecidable {a} {A} _≡_}}
(lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where {{lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_}}
(dummy : ⊤) where
open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_) open import Data.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_)
@ -23,6 +24,8 @@ open import Utils using (Unique; push; Unique-append; All¬-¬Any; All-x∈xs)
open import Data.String using () renaming (_++_ to _++ˢ_) open import Data.String using () renaming (_++_ to _++ˢ_)
open import Showable using (Showable; show) open import Showable using (Showable; show)
open IsDecidable ≡-Decidable-A using () renaming (R-dec to _≟ᴬ_)
open IsLattice lB using () renaming open IsLattice lB using () renaming
( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym; ≈-trans to ≈₂-trans ( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym; ≈-trans to ≈₂-trans
; ≈-⊔-cong to ≈₂-⊔₂-cong; ≈-⊓-cong to ≈₂-⊓₂-cong ; ≈-⊔-cong to ≈₂-⊔₂-cong; ≈-⊓-cong to ≈₂-⊓₂-cong
@ -41,7 +44,7 @@ private module ImplKeys where
∈k-dec : ∀ (k : A) (l : List (A × B)) → Dec (k ∈ˡ (ImplKeys.keys l)) ∈k-dec : ∀ (k : A) (l : List (A × B)) → Dec (k ∈ˡ (ImplKeys.keys l))
∈k-dec k [] = no (λ ()) ∈k-dec k [] = no (λ ())
∈k-dec k ((k' , v) ∷ xs) ∈k-dec k ((k' , v) ∷ xs)
with (≡-dec-A k k') with (k ≟ᴬ k')
... | yes k≡k' = yes (here k≡k') ... | yes k≡k' = yes (here k≡k')
... | no k≢k' with (∈k-dec k xs) ... | no k≢k' with (∈k-dec k xs)
... | yes k∈kxs = yes (there k∈kxs) ... | yes k∈kxs = yes (there k∈kxs)
@ -76,7 +79,7 @@ private module _ where
k∈-dec : ∀ (k : A) (l : List A) → Dec (k ∈ l) k∈-dec : ∀ (k : A) (l : List A) → Dec (k ∈ l)
k∈-dec k [] = no (λ ()) k∈-dec k [] = no (λ ())
k∈-dec k (x ∷ xs) k∈-dec k (x ∷ xs)
with (≡-dec-A k x) with (k ≟ᴬ x)
... | yes refl = yes (here refl) ... | yes refl = yes (here refl)
... | no k≢x with (k∈-dec k xs) ... | no k≢x with (k∈-dec k xs)
... | yes k∈xs = yes (there k∈xs) ... | yes k∈xs = yes (there k∈xs)
@ -113,7 +116,7 @@ private module ImplInsert (f : B → B → B) where
insert : A → B → List (A × B) → List (A × B) insert : A → B → List (A × B) → List (A × B)
insert k v [] = (k , v) ∷ [] insert k v [] = (k , v) ∷ []
insert k v (x@(k' , v') ∷ xs) with ≡-dec-A k k' insert k v (x@(k' , v') ∷ xs) with k ≟ᴬ k'
... | yes _ = (k' , f v v') ∷ xs ... | yes _ = (k' , f v v') ∷ xs
... | no _ = x ∷ insert k v xs ... | no _ = x ∷ insert k v xs
@ -123,11 +126,11 @@ private module ImplInsert (f : B → B → B) where
insert-keys-∈ : ∀ {k : A} {v : B} {l : List (A × B)} → insert-keys-∈ : ∀ {k : A} {v : B} {l : List (A × B)} →
k ∈k l → keys l ≡ keys (insert k v l) k ∈k l → keys l ≡ keys (insert k v l)
insert-keys-∈ {k} {v} {(k' , v') ∷ xs} (here k≡k') insert-keys-∈ {k} {v} {(k' , v') ∷ xs} (here k≡k')
with (≡-dec-A k k') with (k ≟ᴬ k')
... | yes _ = refl ... | yes _ = refl
... | no k≢k' = ⊥-elim (k≢k' k≡k') ... | no k≢k' = ⊥-elim (k≢k' k≡k')
insert-keys-∈ {k} {v} {(k' , _) ∷ xs} (there k∈kxs) insert-keys-∈ {k} {v} {(k' , _) ∷ xs} (there k∈kxs)
with (≡-dec-A k k') with (k ≟ᴬ k')
... | yes _ = refl ... | yes _ = refl
... | no _ = cong (λ xs' → k' ∷ xs') (insert-keys-∈ k∈kxs) ... | no _ = cong (λ xs' → k' ∷ xs') (insert-keys-∈ k∈kxs)
@ -135,7 +138,7 @@ private module ImplInsert (f : B → B → B) where
¬ (k ∈k l) → (keys l ++ (k ∷ [])) ≡ keys (insert k v l) ¬ (k ∈k l) → (keys l ++ (k ∷ [])) ≡ keys (insert k v l)
insert-keys-∉ {k} {v} {[]} _ = refl insert-keys-∉ {k} {v} {[]} _ = refl
insert-keys-∉ {k} {v} {(k' , v') ∷ xs} k∉kl insert-keys-∉ {k} {v} {(k' , v') ∷ xs} k∉kl
with (≡-dec-A k k') with (k ≟ᴬ k')
... | yes k≡k' = ⊥-elim (k∉kl (here k≡k')) ... | yes k≡k' = ⊥-elim (k∉kl (here k≡k'))
... | no _ = cong (λ xs' → k' ∷ xs') ... | no _ = cong (λ xs' → k' ∷ xs')
(insert-keys-∉ (λ k∈kxs → k∉kl (there k∈kxs))) (insert-keys-∉ (λ k∈kxs → k∉kl (there k∈kxs)))
@ -171,7 +174,7 @@ private module ImplInsert (f : B → B → B) where
¬ k ∈k l → (k , v) ∈ insert k v l ¬ k ∈k l → (k , v) ∈ insert k v l
insert-fresh {l = []} k∉kl = here refl insert-fresh {l = []} k∉kl = here refl
insert-fresh {k} {l = (k' , v') ∷ xs} k∉kl insert-fresh {k} {l = (k' , v') ∷ xs} k∉kl
with ≡-dec-A k k' with k ≟ᴬ k'
... | yes k≡k' = ⊥-elim (k∉kl (here k≡k')) ... | yes k≡k' = ⊥-elim (k∉kl (here k≡k'))
... | no _ = there (insert-fresh (λ k∈kxs → k∉kl (there k∈kxs))) ... | no _ = there (insert-fresh (λ k∈kxs → k∉kl (there k∈kxs)))
@ -180,9 +183,9 @@ private module ImplInsert (f : B → B → B) where
insert-preserves-∉k {l = []} k≢k' k∉kl (here k≡k') = k≢k' k≡k' insert-preserves-∉k {l = []} k≢k' k∉kl (here k≡k') = k≢k' k≡k'
insert-preserves-∉k {l = []} k≢k' k∉kl (there ()) insert-preserves-∉k {l = []} k≢k' k∉kl (there ())
insert-preserves-∉k {k} {k'} {v'} {(k'' , v'') ∷ xs} k≢k' k∉kl k∈kil insert-preserves-∉k {k} {k'} {v'} {(k'' , v'') ∷ xs} k≢k' k∉kl k∈kil
with ≡-dec-A k k'' with k ≟ᴬ k''
... | yes k≡k'' = k∉kl (here k≡k'') ... | yes k≡k'' = k∉kl (here k≡k'')
... | no k≢k'' with ≡-dec-A k' k'' | k∈kil ... | no k≢k'' with k' ≟ᴬ k'' | k∈kil
... | yes k'≡k'' | here k≡k'' = k≢k'' k≡k'' ... | yes k'≡k'' | here k≡k'' = k≢k'' k≡k''
... | yes k'≡k'' | there k∈kxs = k∉kl (there k∈kxs) ... | yes k'≡k'' | there k∈kxs = k∉kl (there k∈kxs)
... | no k'≢k'' | here k≡k'' = k∉kl (here k≡k'') ... | no k'≢k'' | here k≡k'' = k∉kl (here k≡k'')
@ -193,18 +196,18 @@ private module ImplInsert (f : B → B → B) where
¬ k ∈k l₁ → ¬ k ∈k l₂ → ¬ k ∈k union l₁ l₂ ¬ k ∈k l₁ → ¬ k ∈k l₂ → ¬ k ∈k union l₁ l₂
union-preserves-∉ {l₁ = []} _ k∉kl₂ = k∉kl₂ union-preserves-∉ {l₁ = []} _ k∉kl₂ = k∉kl₂
union-preserves-∉ {k} {(k' , v') ∷ xs₁} k∉kl₁ k∉kl₂ union-preserves-∉ {k} {(k' , v') ∷ xs₁} k∉kl₁ k∉kl₂
with ≡-dec-A k k' with k ≟ᴬ k'
... | yes k≡k' = ⊥-elim (k∉kl₁ (here k≡k')) ... | yes k≡k' = ⊥-elim (k∉kl₁ (here k≡k'))
... | no k≢k' = insert-preserves-∉k k≢k' (union-preserves-∉ (λ k∈kxs₁ → k∉kl₁ (there k∈kxs₁)) k∉kl₂) ... | no k≢k' = insert-preserves-∉k k≢k' (union-preserves-∉ (λ k∈kxs₁ → k∉kl₁ (there k∈kxs₁)) k∉kl₂)
insert-preserves-∈k : ∀ {k k' : A} {v' : B} {l : List (A × B)} → insert-preserves-∈k : ∀ {k k' : A} {v' : B} {l : List (A × B)} →
k ∈k l → k ∈k insert k' v' l k ∈k l → k ∈k insert k' v' l
insert-preserves-∈k {k} {k'} {v'} {(k'' , v'') ∷ xs} (here k≡k'') insert-preserves-∈k {k} {k'} {v'} {(k'' , v'') ∷ xs} (here k≡k'')
with (≡-dec-A k' k'') with k' ≟ᴬ k''
... | yes _ = here k≡k'' ... | yes _ = here k≡k''
... | no _ = here k≡k'' ... | no _ = here k≡k''
insert-preserves-∈k {k} {k'} {v'} {(k'' , v'') ∷ xs} (there k∈kxs) insert-preserves-∈k {k} {k'} {v'} {(k'' , v'') ∷ xs} (there k∈kxs)
with (≡-dec-A k' k'') with k' ≟ᴬ k''
... | yes _ = there k∈kxs ... | yes _ = there k∈kxs
... | no _ = there (insert-preserves-∈k k∈kxs) ... | no _ = there (insert-preserves-∈k k∈kxs)
@ -236,11 +239,11 @@ private module ImplInsert (f : B → B → B) where
insert-preserves-∈ : ∀ {k k' : A} {v v' : B} {l : List (A × B)} → insert-preserves-∈ : ∀ {k k' : A} {v v' : B} {l : List (A × B)} →
¬ k ≡ k' → (k , v) ∈ l → (k , v) ∈ insert k' v' l ¬ k ≡ k' → (k , v) ∈ l → (k , v) ∈ insert k' v' l
insert-preserves-∈ {k} {k'} {l = x ∷ xs} k≢k' (here k,v=x) insert-preserves-∈ {k} {k'} {l = x ∷ xs} k≢k' (here k,v=x)
rewrite sym k,v=x with ≡-dec-A k' k rewrite sym k,v=x with k' ≟ᴬ k
... | yes k'≡k = ⊥-elim (k≢k' (sym k'≡k)) ... | yes k'≡k = ⊥-elim (k≢k' (sym k'≡k))
... | no _ = here refl ... | no _ = here refl
insert-preserves-∈ {k} {k'} {l = (k'' , _) ∷ xs} k≢k' (there k,v∈xs) insert-preserves-∈ {k} {k'} {l = (k'' , _) ∷ xs} k≢k' (there k,v∈xs)
with ≡-dec-A k' k'' with k' ≟ᴬ k''
... | yes _ = there k,v∈xs ... | yes _ = there k,v∈xs
... | no _ = there (insert-preserves-∈ k≢k' k,v∈xs) ... | no _ = there (insert-preserves-∈ k≢k' k,v∈xs)
@ -259,7 +262,7 @@ private module ImplInsert (f : B → B → B) where
k,v∈mxs₁l = union-preserves-∈₁ uxs₁ k,v∈xs₁ k∉kl₂ k,v∈mxs₁l = union-preserves-∈₁ uxs₁ k,v∈xs₁ k∉kl₂
k≢k' : ¬ k ≡ k' k≢k' : ¬ k ≡ k'
k≢k' with ≡-dec-A k k' k≢k' with k ≟ᴬ k'
... | yes k≡k' rewrite k≡k' = ⊥-elim (All¬-¬Any k'≢xs₁ (∈-cong proj₁ k,v∈xs₁)) ... | yes k≡k' rewrite k≡k' = ⊥-elim (All¬-¬Any k'≢xs₁ (∈-cong proj₁ k,v∈xs₁))
... | no k≢k' = k≢k' ... | no k≢k' = k≢k'
union-preserves-∈₁ {l₁ = (k' , v') ∷ xs₁} (push k'≢xs₁ uxs₁) (here k,v≡k',v') k∉kl₂ union-preserves-∈₁ {l₁ = (k' , v') ∷ xs₁} (push k'≢xs₁ uxs₁) (here k,v≡k',v') k∉kl₂
@ -270,11 +273,11 @@ private module ImplInsert (f : B → B → B) where
Unique (keys l) → (k , v') ∈ l → (k , f v v') ∈ (insert k v l) Unique (keys l) → (k , v') ∈ l → (k , f v v') ∈ (insert k v l)
insert-combines {l = (k' , v'') ∷ xs} _ (here k,v'≡k',v'') insert-combines {l = (k' , v'') ∷ xs} _ (here k,v'≡k',v'')
rewrite cong proj₁ k,v'≡k',v'' rewrite cong proj₂ k,v'≡k',v'' rewrite cong proj₁ k,v'≡k',v'' rewrite cong proj₂ k,v'≡k',v''
with ≡-dec-A k' k' with k' ≟ᴬ k'
... | yes _ = here refl ... | yes _ = here refl
... | no k≢k' = ⊥-elim (k≢k' refl) ... | no k≢k' = ⊥-elim (k≢k' refl)
insert-combines {k} {l = (k' , v'') ∷ xs} (push k'≢xs uxs) (there k,v'∈xs) insert-combines {k} {l = (k' , v'') ∷ xs} (push k'≢xs uxs) (there k,v'∈xs)
with ≡-dec-A k k' with k ≟ᴬ k'
... | yes k≡k' rewrite k≡k' = ⊥-elim (All¬-¬Any k'≢xs (∈-cong proj₁ k,v'∈xs)) ... | yes k≡k' rewrite k≡k' = ⊥-elim (All¬-¬Any k'≢xs (∈-cong proj₁ k,v'∈xs))
... | no k≢k' = there (insert-combines uxs k,v'∈xs) ... | no k≢k' = there (insert-combines uxs k,v'∈xs)
@ -288,13 +291,13 @@ private module ImplInsert (f : B → B → B) where
insert-preserves-∈ k≢k' (union-combines uxs₁ ul₂ k,v₁∈xs₁ k,v₂∈l₂) insert-preserves-∈ k≢k' (union-combines uxs₁ ul₂ k,v₁∈xs₁ k,v₂∈l₂)
where where
k≢k' : ¬ k ≡ k' k≢k' : ¬ k ≡ k'
k≢k' with ≡-dec-A k k' k≢k' with k ≟ᴬ k'
... | yes k≡k' rewrite k≡k' = ⊥-elim (All¬-¬Any k'≢xs₁ (∈-cong proj₁ k,v₁∈xs₁)) ... | yes k≡k' rewrite k≡k' = ⊥-elim (All¬-¬Any k'≢xs₁ (∈-cong proj₁ k,v₁∈xs₁))
... | no k≢k' = k≢k' ... | no k≢k' = k≢k'
update : A → B → List (A × B) → List (A × B) update : A → B → List (A × B) → List (A × B)
update k v [] = [] update k v [] = []
update k v ((k' , v') ∷ xs) with ≡-dec-A k k' update k v ((k' , v') ∷ xs) with k ≟ᴬ k'
... | yes _ = (k' , f v v') ∷ xs ... | yes _ = (k' , f v v') ∷ xs
... | no _ = (k' , v') ∷ update k v xs ... | no _ = (k' , v') ∷ update k v xs
@ -314,7 +317,7 @@ private module ImplInsert (f : B → B → B) where
keys l ≡ keys (update k v l) keys l ≡ keys (update k v l)
update-keys {l = []} = refl update-keys {l = []} = refl
update-keys {k} {v} {l = (k' , v') ∷ xs} update-keys {k} {v} {l = (k' , v') ∷ xs}
with ≡-dec-A k k' with k ≟ᴬ k'
... | yes _ = refl ... | yes _ = refl
... | no _ rewrite update-keys {k} {v} {xs} = refl ... | no _ rewrite update-keys {k} {v} {xs} = refl
@ -431,11 +434,11 @@ private module ImplInsert (f : B → B → B) where
¬ k ≡ k' → (k , v) ∈ l → (k , v) ∈ update k' v' l ¬ k ≡ k' → (k , v) ∈ l → (k , v) ∈ update k' v' l
update-preserves-∈ {k} {k'} {v} {v'} {(k'' , v'') ∷ xs} k≢k' (here k,v≡k'',v'') update-preserves-∈ {k} {k'} {v} {v'} {(k'' , v'') ∷ xs} k≢k' (here k,v≡k'',v'')
rewrite cong proj₁ k,v≡k'',v'' rewrite cong proj₂ k,v≡k'',v'' rewrite cong proj₁ k,v≡k'',v'' rewrite cong proj₂ k,v≡k'',v''
with ≡-dec-A k' k'' with k' ≟ᴬ k''
... | yes k'≡k'' = ⊥-elim (k≢k' (sym k'≡k'')) ... | yes k'≡k'' = ⊥-elim (k≢k' (sym k'≡k''))
... | no _ = here refl ... | no _ = here refl
update-preserves-∈ {k} {k'} {v} {v'} {(k'' , v'') ∷ xs} k≢k' (there k,v∈xs) update-preserves-∈ {k} {k'} {v} {v'} {(k'' , v'') ∷ xs} k≢k' (there k,v∈xs)
with ≡-dec-A k' k'' with k' ≟ᴬ k''
... | yes _ = there k,v∈xs ... | yes _ = there k,v∈xs
... | no _ = there (update-preserves-∈ k≢k' k,v∈xs) ... | no _ = there (update-preserves-∈ k≢k' k,v∈xs)
@ -449,11 +452,11 @@ private module ImplInsert (f : B → B → B) where
Unique (keys l) → (k , v) ∈ l → (k , f v' v) ∈ update k v' l Unique (keys l) → (k , v) ∈ l → (k , f v' v) ∈ update k v' l
update-combines {k} {v} {v'} {(k' , v'') ∷ xs} _ (here k,v=k',v'') update-combines {k} {v} {v'} {(k' , v'') ∷ xs} _ (here k,v=k',v'')
rewrite cong proj₁ k,v=k',v'' rewrite cong proj₂ k,v=k',v'' rewrite cong proj₁ k,v=k',v'' rewrite cong proj₂ k,v=k',v''
with ≡-dec-A k' k' with k' ≟ᴬ k'
... | yes _ = here refl ... | yes _ = here refl
... | no k'≢k' = ⊥-elim (k'≢k' refl) ... | no k'≢k' = ⊥-elim (k'≢k' refl)
update-combines {k} {v} {v'} {(k' , v'') ∷ xs} (push k'≢xs uxs) (there k,v∈xs) update-combines {k} {v} {v'} {(k' , v'') ∷ xs} (push k'≢xs uxs) (there k,v∈xs)
with ≡-dec-A k k' with k ≟ᴬ k'
... | yes k≡k' rewrite k≡k' = ⊥-elim (All¬-¬Any k'≢xs (∈-cong proj₁ k,v∈xs)) ... | yes k≡k' rewrite k≡k' = ⊥-elim (All¬-¬Any k'≢xs (∈-cong proj₁ k,v∈xs))
... | no _ = there (update-combines uxs k,v∈xs) ... | no _ = there (update-combines uxs k,v∈xs)
@ -467,7 +470,7 @@ private module ImplInsert (f : B → B → B) where
update-preserves-∈ k≢k' (updates-combine uxs₁ u₂ k,v₁∈xs k,v₂∈l₂) update-preserves-∈ k≢k' (updates-combine uxs₁ u₂ k,v₁∈xs k,v₂∈l₂)
where where
k≢k' : ¬ k ≡ k' k≢k' : ¬ k ≡ k'
k≢k' with ≡-dec-A k k' k≢k' with k ≟ᴬ k'
... | yes k≡k' rewrite k≡k' = ⊥-elim (All¬-¬Any k'≢xs (∈-cong proj₁ k,v₁∈xs)) ... | yes k≡k' rewrite k≡k' = ⊥-elim (All¬-¬Any k'≢xs (∈-cong proj₁ k,v₁∈xs))
... | no k≢k' = k≢k' ... | no k≢k' = k≢k'
@ -625,7 +628,8 @@ Expr-Provenance-≡ {k} {v} e k,v∈e
with (v' , (p , k,v'∈e)) ← Expr-Provenance k e (forget k,v∈e) with (v' , (p , k,v'∈e)) ← Expr-Provenance k e (forget k,v∈e)
rewrite Map-functional {m = ⟦ e ⟧} k,v∈e k,v'∈e = p rewrite Map-functional {m = ⟦ e ⟧} k,v∈e k,v'∈e = p
module _ (≈₂-dec : IsDecidable _≈₂_) where module _ {{≈₂-Decidable : IsDecidable _≈₂_}} where
open IsDecidable ≈₂-Decidable using () renaming (R-dec to ≈₂-dec)
private module _ where private module _ where
data SubsetInfo (m₁ m₂ : Map) : Set (a ⊔ℓ b) where data SubsetInfo (m₁ m₂ : Map) : Set (a ⊔ℓ b) where
extra : (k : A) → k ∈k m₁ → ¬ k ∈k m₂ → SubsetInfo m₁ m₂ extra : (k : A) → k ∈k m₁ → ¬ k ∈k m₂ → SubsetInfo m₁ m₂
@ -676,6 +680,9 @@ module _ (≈₂-dec : IsDecidable _≈₂_) where
... | _ | no m₂̷⊆m₁ = no (λ (_ , m₂⊆m₁) → m₂̷⊆m₁ m₂⊆m₁) ... | _ | no m₂̷⊆m₁ = no (λ (_ , m₂⊆m₁) → m₂̷⊆m₁ m₂⊆m₁)
... | no m₁̷⊆m₂ | _ = no (λ (m₁⊆m₂ , _) → m₁̷⊆m₂ m₁⊆m₂) ... | no m₁̷⊆m₂ | _ = no (λ (m₁⊆m₂ , _) → m₁̷⊆m₂ m₁⊆m₂)
≈-Decidable : IsDecidable _≈_
≈-Decidable = record { R-dec = ≈-dec }
private module I⊔ = ImplInsert _⊔₂_ private module I⊔ = ImplInsert _⊔₂_
private module I⊓ = ImplInsert _⊓₂_ private module I⊓ = ImplInsert _⊓₂_
@ -1026,7 +1033,7 @@ updating-via-k∉ks-backward m = transform-k∉ks-backward
module _ {l} {L : Set l} module _ {l} {L : Set l}
{_≈ˡ_ : L → L → Set l} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L} {_≈ˡ_ : L → L → Set l} {_⊔ˡ_ : L → L → L} {_⊓ˡ_ : L → L → L}
(lL : IsLattice L _≈ˡ_ _⊔ˡ_ _⊓ˡ_) where {{lL : IsLattice L _≈ˡ_ _⊔ˡ_ _⊓ˡ_}} where
open IsLattice lL using () renaming (_≼_ to _≼ˡ_) open IsLattice lL using () renaming (_≼_ to _≼ˡ_)
module _ (f : L → Map) (f-Monotonic : Monotonic _≼ˡ_ _≼_ f) module _ (f : L → Map) (f-Monotonic : Monotonic _≼ˡ_ _≼_ f)

6
Lattice/MapSet.agda
View File

@ -1,9 +1,9 @@
open import Lattice open import Lattice
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
open import Relation.Binary.Definitions using (Decidable)
open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_) open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
open import Data.Unit using (⊤)
module Lattice.MapSet {a : Level} {A : Set a} (≡-dec-A : Decidable (_≡_ {a} {A})) where module Lattice.MapSet {a : Level} (A : Set a) {{≡-Decidable-A : IsDecidable (_≡_ {a} {A})}} (dummy : ⊤) where
open import Data.List using (List; map) open import Data.List using (List; map)
open import Data.Product using (_,_; proj₁) open import Data.Product using (_,_; proj₁)
@ -12,7 +12,7 @@ open import Function using (_∘_)
open import Lattice.Unit using (⊤; tt) renaming (_≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_; isLattice to ⊤-isLattice) open import Lattice.Unit using (⊤; tt) renaming (_≈_ to _≈₂_; _⊔_ to _⊔₂_; _⊓_ to _⊓₂_; isLattice to ⊤-isLattice)
import Lattice.Map import Lattice.Map
private module UnitMap = Lattice.Map ≡-dec-A ⊤-isLattice private module UnitMap = Lattice.Map A ⊤ dummy
open UnitMap open UnitMap
using (Map; Expr; ⟦_⟧) using (Map; Expr; ⟦_⟧)
renaming renaming

74
Lattice/Nat.agda
View File

@ -18,31 +18,32 @@ private
≡-⊓-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≡ a₂ → a₃ ≡ a₄ → (a₁ ⊓ a₃) ≡ (a₂ ⊓ a₄) ≡-⊓-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≡ a₂ → a₃ ≡ a₄ → (a₁ ⊓ a₃) ≡ (a₂ ⊓ a₄)
≡-⊓-cong a₁≡a₂ a₃≡a₄ rewrite a₁≡a₂ rewrite a₃≡a₄ = refl ≡-⊓-cong a₁≡a₂ a₃≡a₄ rewrite a₁≡a₂ rewrite a₃≡a₄ = refl
isMaxSemilattice : IsSemilattice ℕ _≡_ _⊔_ instance
isMaxSemilattice = record isMaxSemilattice : IsSemilattice ℕ _≡_ _⊔_
{ ≈-equiv = record isMaxSemilattice = record
{ ≈-refl = refl { ≈-equiv = record
; ≈-sym = sym { ≈-refl = refl
; ≈-trans = trans ; ≈-sym = sym
; ≈-trans = trans
}
; ≈-⊔-cong = ≡-⊔-cong
; ⊔-assoc = ⊔-assoc
; ⊔-comm = ⊔-comm
; ⊔-idemp = ⊔-idem
} }
; ≈-⊔-cong = ≡-⊔-cong
; ⊔-assoc = ⊔-assoc
; ⊔-comm = ⊔-comm
; ⊔-idemp = ⊔-idem
}
isMinSemilattice : IsSemilattice ℕ _≡_ _⊓_ isMinSemilattice : IsSemilattice ℕ _≡_ _⊓_
isMinSemilattice = record isMinSemilattice = record
{ ≈-equiv = record { ≈-equiv = record
{ ≈-refl = refl { ≈-refl = refl
; ≈-sym = sym ; ≈-sym = sym
; ≈-trans = trans ; ≈-trans = trans
}
; ≈-⊔-cong = ≡-⊓-cong
; ⊔-assoc = ⊓-assoc
; ⊔-comm = ⊓-comm
; ⊔-idemp = ⊓-idem
} }
; ≈-⊔-cong = ≡-⊓-cong
; ⊔-assoc = ⊓-assoc
; ⊔-comm = ⊓-comm
; ⊔-idemp = ⊓-idem
}
private private
max-bound₁ : {x y z : ℕ} → x ⊔ y ≡ z → x ≤ z max-bound₁ : {x y z : ℕ} → x ⊔ y ≡ z → x ≤ z
@ -74,18 +75,19 @@ private
helper : x ⊔ (x ⊓ y) ≤ x ⊔ x → x ⊔ x ≡ x → x ⊔ (x ⊓ y) ≤ x helper : x ⊔ (x ⊓ y) ≤ x ⊔ x → x ⊔ x ≡ x → x ⊔ (x ⊓ y) ≤ x
helper x⊔x⊓y≤x⊔x x⊔x≡x rewrite x⊔x≡x = x⊔x⊓y≤x⊔x helper x⊔x⊓y≤x⊔x x⊔x≡x rewrite x⊔x≡x = x⊔x⊓y≤x⊔x
isLattice : IsLattice ℕ _≡_ _⊔_ _⊓_ instance
isLattice = record isLattice : IsLattice ℕ _≡_ _⊔_ _⊓_
{ joinSemilattice = isMaxSemilattice isLattice = record
; meetSemilattice = isMinSemilattice { joinSemilattice = isMaxSemilattice
; absorb-⊔-⊓ = λ x y → maxmin-absorb {x} {y} ; meetSemilattice = isMinSemilattice
; absorb-⊓-⊔ = λ x y → minmax-absorb {x} {y} ; absorb-⊔-⊓ = λ x y → maxmin-absorb {x} {y}
} ; absorb-⊓-⊔ = λ x y → minmax-absorb {x} {y}
}
lattice : Lattice ℕ lattice : Lattice ℕ
lattice = record lattice = record
{ _≈_ = _≡_ { _≈_ = _≡_
; _⊔_ = _⊔_ ; _⊔_ = _⊔_
; _⊓_ = _⊓_ ; _⊓_ = _⊓_
; isLattice = isLattice ; isLattice = isLattice
} }

209
Lattice/Prod.agda
View File

@ -1,10 +1,10 @@
open import Lattice open import Lattice
module Lattice.Prod {a b} {A : Set a} {B : Set b} module Lattice.Prod {a b} (A : Set a) (B : Set b)
(_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set b) {_≈₁_ : A → A → Set a} {_≈₂_ : B → B → Set b}
(_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B) {_⊔₁_ : A → A → A} {_⊔₂_ : B → B → B}
(_⊓₁_ : A → A → A) (_⊓₂_ : B → B → B) {_⊓₁_ : A → A → A} {_⊓₂_ : B → B → B}
(lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where {{lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_}} {{lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_}} where
open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_) open import Agda.Primitive using (Level) renaming (_⊔_ to _⊔ℓ_)
open import Data.Nat using (ℕ; _≤_; _+_; suc) open import Data.Nat using (ℕ; _≤_; _+_; suc)
@ -12,6 +12,7 @@ open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
open import Data.Empty using (⊥-elim) open import Data.Empty using (⊥-elim)
open import Relation.Binary.Core using (_Preserves_⟶_ ) open import Relation.Binary.Core using (_Preserves_⟶_ )
open import Relation.Binary.PropositionalEquality using (sym; subst) open import Relation.Binary.PropositionalEquality using (sym; subst)
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Nullary using (¬_; yes; no) open import Relation.Nullary using (¬_; yes; no)
open import Equivalence open import Equivalence
import Chain import Chain
@ -39,13 +40,14 @@ open IsLattice lB using () renaming
_≈_ : A × B → A × B → Set (a ⊔ℓ b) _≈_ : A × B → A × B → Set (a ⊔ℓ b)
(a₁ , b₁) ≈ (a₂ , b₂) = (a₁ ≈₁ a₂) × (b₁ ≈₂ b₂) (a₁ , b₁) ≈ (a₂ , b₂) = (a₁ ≈₁ a₂) × (b₁ ≈₂ b₂)
≈-equiv : IsEquivalence (A × B) _≈_ instance
≈-equiv = record ≈-equiv : IsEquivalence (A × B) _≈_
{ ≈-refl = λ {p} → (≈₁-refl , ≈₂-refl) ≈-equiv = record
; ≈-sym = λ {p₁} {p₂} (a₁≈a₂ , b₁≈b₂) → (≈₁-sym a₁≈a₂ , ≈₂-sym b₁≈b₂) { ≈-refl = λ {p} → (≈₁-refl , ≈₂-refl)
; ≈-trans = λ {p₁} {p₂} {p₃} (a₁≈a₂ , b₁≈b₂) (a₂≈a₃ , b₂≈b₃) → ; ≈-sym = λ {p₁} {p₂} (a₁≈a₂ , b₁≈b₂) → (≈₁-sym a₁≈a₂ , ≈₂-sym b₁≈b₂)
( ≈₁-trans a₁≈a₂ a₂≈a₃ , ≈₂-trans b₁≈b₂ b₂≈b₃ ) ; ≈-trans = λ {p₁} {p₂} {p₃} (a₁≈a₂ , b₁≈b₂) (a₂≈a₃ , b₂≈b₃) →
} ( ≈₁-trans a₁≈a₂ a₂≈a₃ , ≈₂-trans b₁≈b₂ b₂≈b₃ )
}
_⊔_ : A × B → A × B → A × B _⊔_ : A × B → A × B → A × B
(a₁ , b₁) ⊔ (a₂ , b₂) = (a₁ ⊔₁ a₂ , b₁ ⊔₂ b₂) (a₁ , b₁) ⊔ (a₂ , b₂) = (a₁ ⊔₁ a₂ , b₁ ⊔₂ b₂)
@ -75,116 +77,123 @@ private module ProdIsSemilattice (f₁ : A → A → A) (f₂ : B → B → B) (
) )
} }
isJoinSemilattice : IsSemilattice (A × B) _≈_ _⊔_ instance
isJoinSemilattice = ProdIsSemilattice.isSemilattice _⊔₁_ _⊔₂_ joinSemilattice₁ joinSemilattice₂ isJoinSemilattice : IsSemilattice (A × B) _≈_ _⊔_
isJoinSemilattice = ProdIsSemilattice.isSemilattice _⊔₁_ _⊔₂_ joinSemilattice₁ joinSemilattice₂
isMeetSemilattice : IsSemilattice (A × B) _≈_ _⊓_ isMeetSemilattice : IsSemilattice (A × B) _≈_ _⊓_
isMeetSemilattice = ProdIsSemilattice.isSemilattice _⊓₁_ _⊓₂_ meetSemilattice₁ meetSemilattice₂ isMeetSemilattice = ProdIsSemilattice.isSemilattice _⊓₁_ _⊓₂_ meetSemilattice₁ meetSemilattice₂
isLattice : IsLattice (A × B) _≈_ _⊔_ _⊓_ isLattice : IsLattice (A × B) _≈_ _⊔_ _⊓_
isLattice = record isLattice = record
{ joinSemilattice = isJoinSemilattice { joinSemilattice = isJoinSemilattice
; meetSemilattice = isMeetSemilattice ; meetSemilattice = isMeetSemilattice
; absorb-⊔-⊓ = λ (a₁ , b₁) (a₂ , b₂) → ; absorb-⊔-⊓ = λ (a₁ , b₁) (a₂ , b₂) →
( IsLattice.absorb-⊔-⊓ lA a₁ a₂ ( IsLattice.absorb-⊔-⊓ lA a₁ a₂
, IsLattice.absorb-⊔-⊓ lB b₁ b₂ , IsLattice.absorb-⊔-⊓ lB b₁ b₂
) )
; absorb-⊓-⊔ = λ (a₁ , b₁) (a₂ , b₂) → ; absorb-⊓-⊔ = λ (a₁ , b₁) (a₂ , b₂) →
( IsLattice.absorb-⊓-⊔ lA a₁ a₂ ( IsLattice.absorb-⊓-⊔ lA a₁ a₂
, IsLattice.absorb-⊓-⊔ lB b₁ b₂ , IsLattice.absorb-⊓-⊔ lB b₁ b₂
) )
} }
lattice : Lattice (A × B) lattice : Lattice (A × B)
lattice = record lattice = record
{ _≈_ = _≈_ { _≈_ = _≈_
; _⊔_ = _⊔_ ; _⊔_ = _⊔_
; _⊓_ = _⊓_ ; _⊓_ = _⊓_
; isLattice = isLattice ; isLattice = isLattice
} }
module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) where module _ {{≈₁-Decidable : IsDecidable _≈₁_}} {{≈₂-Decidable : IsDecidable _≈₂_}} where
≈-dec : IsDecidable _≈_ open IsDecidable ≈₁-Decidable using () renaming (R-dec to ≈₁-dec)
open IsDecidable ≈₂-Decidable using () renaming (R-dec to ≈₂-dec)
≈-dec : Decidable _≈_
≈-dec (a₁ , b₁) (a₂ , b₂) ≈-dec (a₁ , b₁) (a₂ , b₂)
with ≈₁-dec a₁ a₂ | ≈₂-dec b₁ b₂ with ≈₁-dec a₁ a₂ | ≈₂-dec b₁ b₂
... | yes a₁≈a₂ | yes b₁≈b₂ = yes (a₁≈a₂ , b₁≈b₂) ... | yes a₁≈a₂ | yes b₁≈b₂ = yes (a₁≈a₂ , b₁≈b₂)
... | no a₁̷≈a₂ | _ = no (λ (a₁≈a₂ , _) → a₁̷≈a₂ a₁≈a₂) ... | no a₁̷≈a₂ | _ = no (λ (a₁≈a₂ , _) → a₁̷≈a₂ a₁≈a₂)
... | _ | no b₁̷≈b₂ = no (λ (_ , b₁≈b₂) → b₁̷≈b₂ b₁≈b₂) ... | _ | no b₁̷≈b₂ = no (λ (_ , b₁≈b₂) → b₁̷≈b₂ b₁≈b₂)
instance
≈-Decidable : IsDecidable _≈_
≈-Decidable = record { R-dec = ≈-dec }
module _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_) module _ {h₁ h₂ : ℕ}
(h₁ h₂ : ℕ) {{fhA : FixedHeight₁ h₁}} {{fhB : FixedHeight₂ h₂}} where
(fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where
open import Data.Nat.Properties open import Data.Nat.Properties
open IsLattice isLattice using (_≼_; _≺_; ≺-cong) open IsLattice isLattice using (_≼_; _≺_; ≺-cong)
module ChainMapping₁ = ChainMapping joinSemilattice₁ isJoinSemilattice module ChainMapping₁ = ChainMapping joinSemilattice₁ isJoinSemilattice
module ChainMapping₂ = ChainMapping joinSemilattice₂ isJoinSemilattice module ChainMapping₂ = ChainMapping joinSemilattice₂ isJoinSemilattice
module ChainA = Chain _≈₁_ ≈₁-equiv _≺₁_ ≺₁-cong module ChainA = Chain _≈₁_ ≈₁-equiv _≺₁_ ≺₁-cong
module ChainB = Chain _≈₂_ ≈₂-equiv _≺₂_ ≺₂-cong module ChainB = Chain _≈₂_ ≈₂-equiv _≺₂_ ≺₂-cong
module ProdChain = Chain _≈_ ≈-equiv _≺_ ≺-cong module ProdChain = Chain _≈_ ≈-equiv _≺_ ≺-cong
open ChainA using () renaming (Chain to Chain₁; done to done₁; step to step₁; Chain-≈-cong₁ to Chain₁-≈-cong₁) open ChainA using () renaming (Chain to Chain₁; done to done₁; step to step₁; Chain-≈-cong₁ to Chain₁-≈-cong₁)
open ChainB using () renaming (Chain to Chain₂; done to done₂; step to step₂; Chain-≈-cong₁ to Chain₂-≈-cong₁) open ChainB using () renaming (Chain to Chain₂; done to done₂; step to step₂; Chain-≈-cong₁ to Chain₂-≈-cong₁)
open ProdChain using (Chain; concat; done; step) open ProdChain using (Chain; concat; done; step)
private private
a,∙-Monotonic : ∀ (a : A) → Monotonic _≼₂_ _≼_ (λ b → (a , b)) a,∙-Monotonic : ∀ (a : A) → Monotonic _≼₂_ _≼_ (λ b → (a , b))
a,∙-Monotonic a {b₁} {b₂} b₁⊔b₂≈b₂ = (⊔₁-idemp a , b₁⊔b₂≈b₂) a,∙-Monotonic a {b₁} {b₂} b₁⊔b₂≈b₂ = (⊔₁-idemp a , b₁⊔b₂≈b₂)
a,∙-Preserves-≈₂ : ∀ (a : A) → (λ b → (a , b)) Preserves _≈₂_ ⟶ _≈_ a,∙-Preserves-≈₂ : ∀ (a : A) → (λ b → (a , b)) Preserves _≈₂_ ⟶ _≈_
a,∙-Preserves-≈₂ a {b₁} {b₂} b₁≈b₂ = (≈₁-refl , b₁≈b₂) a,∙-Preserves-≈₂ a {b₁} {b₂} b₁≈b₂ = (≈₁-refl , b₁≈b₂)
∙,b-Monotonic : ∀ (b : B) → Monotonic _≼₁_ _≼_ (λ a → (a , b)) ∙,b-Monotonic : ∀ (b : B) → Monotonic _≼₁_ _≼_ (λ a → (a , b))
∙,b-Monotonic b {a₁} {a₂} a₁⊔a₂≈a₂ = (a₁⊔a₂≈a₂ , ⊔₂-idemp b) ∙,b-Monotonic b {a₁} {a₂} a₁⊔a₂≈a₂ = (a₁⊔a₂≈a₂ , ⊔₂-idemp b)
∙,b-Preserves-≈₁ : ∀ (b : B) → (λ a → (a , b)) Preserves _≈₁_ ⟶ _≈_ ∙,b-Preserves-≈₁ : ∀ (b : B) → (λ a → (a , b)) Preserves _≈₁_ ⟶ _≈_
∙,b-Preserves-≈₁ b {a₁} {a₂} a₁≈a₂ = (a₁≈a₂ , ≈₂-refl) ∙,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 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₂) open ChainB.Height fhB using () renaming (⊥ to ⊥₂; ⊤ to ⊤₂; longestChain to longestChain₂; bounded to bounded₂)
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 : ∀ {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)) unzip (done (a₁≈a₂ , b₁≈b₂)) = ((0 , 0) , ((done₁ a₁≈a₂ , done₂ b₁≈b₂) , ≤-refl))
unzip {a₁} {a₂} {b₁} {b₂} {n} (step {(a₁ , b₁)} {(a , b)} ((a₁≼a , b₁≼b) , a₁b₁̷≈ab) (a≈a' , b≈b') a'b'a₂b₂) unzip {a₁} {a₂} {b₁} {b₂} {n} (step {(a₁ , b₁)} {(a , b)} ((a₁≼a , b₁≼b) , a₁b₁̷≈ab) (a≈a' , b≈b') a'b'a₂b₂)
with ≈₁-dec a₁ a | ≈₂-dec b₁ b | unzip a'b'a₂b₂ with ≈₁-dec a₁ a | ≈₂-dec b₁ b | unzip a'b'a₂b₂
... | yes a₁≈a | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = ⊥-elim (a₁b₁̷≈ab (a₁≈a , b₁≈b)) ... | yes a₁≈a | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = ⊥-elim (a₁b₁̷≈ab (a₁≈a , b₁≈b))
... | no a₁̷≈a | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = ... | no a₁̷≈a | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) =
((suc n₁ , n₂) , ((step₁ (a₁≼a , a₁̷≈a) a≈a' c₁ , Chain₂-≈-cong₁ (≈₂-sym (≈₂-trans b₁≈b b≈b')) c₂), +-monoʳ-≤ 1 (n≤n₁+n₂))) ((suc n₁ , n₂) , ((step₁ (a₁≼a , a₁̷≈a) a≈a' c₁ , Chain₂-≈-cong₁ (≈₂-sym (≈₂-trans b₁≈b b≈b')) c₂), +-monoʳ-≤ 1 (n≤n₁+n₂)))
... | yes a₁≈a | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = ... | yes a₁≈a | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) =
((n₁ , suc n₂) , ( (Chain₁-≈-cong₁ (≈₁-sym (≈₁-trans a₁≈a a≈a')) c₁ , step₂ (b₁≼b , b₁̷≈b) b≈b' c₂) ((n₁ , suc n₂) , ( (Chain₁-≈-cong₁ (≈₁-sym (≈₁-trans a₁≈a a≈a')) c₁ , step₂ (b₁≼b , b₁̷≈b) b≈b' c₂)
, subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂) , subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂)
))
... | no a₁̷≈a | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) =
((suc n₁ , suc n₂) , ( (step₁ (a₁≼a , a₁̷≈a) a≈a' c₁ , step₂ (b₁≼b , b₁̷≈b) b≈b' c₂)
, m≤n⇒m≤o+n 1 (subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂))
)) ))
... | no a₁̷≈a | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) =
((suc n₁ , suc n₂) , ( (step₁ (a₁≼a , a₁̷≈a) a≈a' c₁ , step₂ (b₁≼b , b₁̷≈b) b≈b' c₂)
, m≤n⇒m≤o+n 1 (subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂))
))
fixedHeight : IsLattice.FixedHeight isLattice (h₁ + h₂) instance
fixedHeight = record fixedHeight : IsLattice.FixedHeight isLattice (h₁ + h₂)
{ ⊥ = (⊥₁ , ⊥₂) fixedHeight = record
; ⊤ = (⊤₁ , ⊤₂) { ⊥ = (⊥₁ , ⊥₂)
; longestChain = concat ; ⊤ = (⊤₁ , ⊤₂)
(ChainMapping₁.Chain-map (λ a → (a , ⊥₂)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) longestChain₁) ; longestChain = concat
(ChainMapping₂.Chain-map (λ b → (⊤₁ , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) longestChain₂) (ChainMapping₁.Chain-map (λ a → (a , ⊥₂)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) longestChain₁)
; bounded = λ a₁b₁a₂b₂ → (ChainMapping₂.Chain-map (λ b → (⊤₁ , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) longestChain₂)
let ((n₁ , n₂) , ((a₁a₂ , b₁b₂) , n≤n₁+n₂)) = unzip a₁b₁a₂b₂ ; bounded = λ a₁b₁a₂b₂ →
in ≤-trans n≤n₁+n₂ (+-mono-≤ (bounded₁ a₁a₂) (bounded₂ b₁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₂))
}
isFiniteHeightLattice : IsFiniteHeightLattice (A × B) (h₁ + h₂) _≈_ _⊔_ _⊓_ isFiniteHeightLattice : IsFiniteHeightLattice (A × B) (h₁ + h₂) _≈_ _⊔_ _⊓_
isFiniteHeightLattice = record isFiniteHeightLattice = record
{ isLattice = isLattice { isLattice = isLattice
; fixedHeight = fixedHeight ; fixedHeight = fixedHeight
} }
finiteHeightLattice : FiniteHeightLattice (A × B) finiteHeightLattice : FiniteHeightLattice (A × B)
finiteHeightLattice = record finiteHeightLattice = record
{ height = h₁ + h₂ { height = h₁ + h₂
; _≈_ = _≈_ ; _≈_ = _≈_
; _⊔_ = _⊔_ ; _⊔_ = _⊔_
; _⊓_ = _⊓_ ; _⊓_ = _⊓_
; isFiniteHeightLattice = isFiniteHeightLattice ; isFiniteHeightLattice = isFiniteHeightLattice
} }

117
Lattice/Unit.agda
View File

@ -7,6 +7,7 @@ open import Data.Unit using (⊤; tt) public
open import Data.Unit.Properties using (_≟_; ≡-setoid) open import Data.Unit.Properties using (_≟_; ≡-setoid)
open import Relation.Binary using (Setoid) open import Relation.Binary using (Setoid)
open import Relation.Binary.PropositionalEquality as Eq using (_≡_) open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Nullary using (Dec; ¬_; yes; no) open import Relation.Nullary using (Dec; ¬_; yes; no)
open import Equivalence open import Equivalence
open import Lattice open import Lattice
@ -24,9 +25,13 @@ _≈_ = _≡_
; ≈-trans = trans ; ≈-trans = trans
} }
≈-dec : IsDecidable _≈_ ≈-dec : Decidable _≈_
≈-dec = _≟_ ≈-dec = _≟_
instance
≈-Decidable : IsDecidable _≈_
≈-Decidable = record { R-dec = ≈-dec }
_⊔_ : ⊤ → ⊤ → ⊤ _⊔_ : ⊤ → ⊤ → ⊤
tt ⊔ tt = tt tt ⊔ tt = tt
@ -45,14 +50,15 @@ tt ⊓ tt = tt
⊔-idemp : (x : ⊤) → (x ⊔ x) ≈ x ⊔-idemp : (x : ⊤) → (x ⊔ x) ≈ x
⊔-idemp tt = Eq.refl ⊔-idemp tt = Eq.refl
isJoinSemilattice : IsSemilattice ⊤ _≈_ _⊔_ instance
isJoinSemilattice = record isJoinSemilattice : IsSemilattice ⊤ _≈_ _⊔_
{ ≈-equiv = ≈-equiv isJoinSemilattice = record
; ≈-⊔-cong = ≈-⊔-cong { ≈-equiv = ≈-equiv
; ⊔-assoc = ⊔-assoc ; ≈-⊔-cong = ≈-⊔-cong
; ⊔-comm = ⊔-comm ; ⊔-assoc = ⊔-assoc
; ⊔-idemp = ⊔-idemp ; ⊔-comm = ⊔-comm
} ; ⊔-idemp = ⊔-idemp
}
≈-⊓-cong : ∀ {ab₁ ab₂ ab₃ ab₄} → ab₁ ≈ ab₂ → ab₃ ≈ ab₄ → (ab₁ ⊓ ab₃) ≈ (ab₂ ⊓ ab₄) ≈-⊓-cong : ∀ {ab₁ ab₂ ab₃ ab₄} → ab₁ ≈ ab₂ → ab₃ ≈ ab₄ → (ab₁ ⊓ ab₃) ≈ (ab₂ ⊓ ab₄)
≈-⊓-cong {tt} {tt} {tt} {tt} _ _ = Eq.refl ≈-⊓-cong {tt} {tt} {tt} {tt} _ _ = Eq.refl
@ -66,36 +72,32 @@ isJoinSemilattice = record
⊓-idemp : (x : ⊤) → (x ⊓ x) ≈ x ⊓-idemp : (x : ⊤) → (x ⊓ x) ≈ x
⊓-idemp tt = Eq.refl ⊓-idemp tt = Eq.refl
isMeetSemilattice : IsSemilattice ⊤ _≈_ _⊓_ instance
isMeetSemilattice = record isMeetSemilattice : IsSemilattice ⊤ _≈_ _⊓_
{ ≈-equiv = ≈-equiv isMeetSemilattice = record
; ≈-⊔-cong = ≈-⊓-cong { ≈-equiv = ≈-equiv
; ⊔-assoc = ⊓-assoc ; ≈-⊔-cong = ≈-⊓-cong
; ⊔-comm = ⊓-comm ; ⊔-assoc = ⊓-assoc
; ⊔-idemp = ⊓-idemp ; ⊔-comm = ⊓-comm
} ; ⊔-idemp = ⊓-idemp
}
absorb-⊔-⊓ : (x y : ⊤) → (x ⊔ (x ⊓ y)) ≈ x instance
absorb-⊔-⊓ tt tt = Eq.refl isLattice : IsLattice ⊤ _≈_ _⊔_ _⊓_
isLattice = record
{ joinSemilattice = isJoinSemilattice
; meetSemilattice = isMeetSemilattice
; absorb-⊔-⊓ = λ { tt tt → Eq.refl }
; absorb-⊓-⊔ = λ { tt tt → Eq.refl }
}
absorb-⊓-⊔ : (x y : ⊤) → (x ⊓ (x ⊔ y)) ≈ x lattice : Lattice ⊤
absorb-⊓-⊔ tt tt = Eq.refl lattice = record
{ _≈_ = _≈_
isLattice : IsLattice ⊤ _≈_ _⊔_ _⊓_ ; _⊔_ = _⊔_
isLattice = record ; _⊓_ = _⊓_
{ joinSemilattice = isJoinSemilattice ; isLattice = isLattice
; meetSemilattice = isMeetSemilattice }
; absorb-⊔-⊓ = absorb-⊔-⊓
; absorb-⊓-⊔ = absorb-⊓-⊔
}
lattice : Lattice ⊤
lattice = record
{ _≈_ = _≈_
; _⊔_ = _⊔_
; _⊓_ = _⊓_
; isLattice = isLattice
}
open Chain _≈_ ≈-equiv (IsLattice._≺_ isLattice) (IsLattice.≺-cong isLattice) open Chain _≈_ ≈-equiv (IsLattice._≺_ isLattice) (IsLattice.≺-cong isLattice)
@ -107,25 +109,26 @@ private
isLongest {tt} {tt} (step (tt⊔tt≈tt , tt̷≈tt) _ _) = ⊥-elim (tt̷≈tt refl) isLongest {tt} {tt} (step (tt⊔tt≈tt , tt̷≈tt) _ _) = ⊥-elim (tt̷≈tt refl)
isLongest (done _) = z≤n isLongest (done _) = z≤n
fixedHeight : IsLattice.FixedHeight isLattice 0 instance
fixedHeight = record fixedHeight : IsLattice.FixedHeight isLattice 0
{ ⊥ = tt fixedHeight = record
; ⊤ = tt { ⊥ = tt
; longestChain = longestChain ; ⊤ = tt
; bounded = isLongest ; longestChain = longestChain
} ; bounded = isLongest
}
isFiniteHeightLattice : IsFiniteHeightLattice ⊤ 0 _≈_ _⊔_ _⊓_ isFiniteHeightLattice : IsFiniteHeightLattice ⊤ 0 _≈_ _⊔_ _⊓_
isFiniteHeightLattice = record isFiniteHeightLattice = record
{ isLattice = isLattice { isLattice = isLattice
; fixedHeight = fixedHeight ; fixedHeight = fixedHeight
} }
finiteHeightLattice : FiniteHeightLattice ⊤ finiteHeightLattice : FiniteHeightLattice ⊤
finiteHeightLattice = record finiteHeightLattice = record
{ height = 0 { height = 0
; _≈_ = _≈_ ; _≈_ = _≈_
; _⊔_ = _⊔_ ; _⊔_ = _⊔_
; _⊓_ = _⊓_ ; _⊓_ = _⊓_
; isFiniteHeightLattice = isFiniteHeightLattice ; isFiniteHeightLattice = isFiniteHeightLattice
} }

3
Utils.agda
View File

@ -103,3 +103,6 @@ _∨_ P Q a = P a ⊎ Q a
_∧_ : ∀ {a p₁ p₂} {A : Set a} (P : A → Set p₁) (Q : A → Set p₂) → _∧_ : ∀ {a p₁ p₂} {A : Set a} (P : A → Set p₁) (Q : A → Set p₂) →
A → Set (p₁ ⊔ℓ p₂) A → Set (p₁ ⊔ℓ p₂)
_∧_ P Q a = P a × Q a _∧_ P Q a = P a × Q a
it : ∀ {a} {A : Set a} {{_ : A}} → A
it {{x}} = x