Compare commits

...

2 Commits

Author SHA1 Message Date
671ffc82df Define to-and-from functions from finite maps to tuples and prove one inverse direction
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-19 14:50:29 -08:00
486b552b59 Try to generalize universe levels where possible
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-19 12:36:46 -08:00
3 changed files with 65 additions and 3 deletions

View File

@ -0,0 +1,57 @@
-- Because iterated products currently require both A and B to be of the same
-- universe, and the FiniteMap is written in a universe-polymorphic way,
-- specialize the FiniteMap module with Set-typed types only.
open import Lattice
open import Equivalence
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 Function.Definitions using (Inverseˡ; Inverseʳ)
module Lattice.FiniteValueMap (A : Set) (B : Set)
(_≈₂_ : B B Set)
(_⊔₂_ : B B B) (_⊓₂_ : B B B)
(≈-dec-A : Decidable (_≡_ {_} {A}))
(lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where
open import Data.List using (List; length; []; _∷_)
open import Utils using (Unique; push; empty)
open import Data.Product using (_,_)
open import Data.List.Properties using (∷-injectiveʳ)
open import Lattice.FiniteMap A B _≈₂_ _⊔₂_ _⊓₂_ ≈-dec-A lB public
module IterProdIsomorphism where
open import Data.Unit using (; tt)
open import Lattice.Unit using () renaming (_≈_ to _≈ᵘ_; _⊔_ to _⊔ᵘ_; _⊓_ to _⊓ᵘ_; ≈-dec to ≈ᵘ-dec; isLattice to isLatticeᵘ)
open import Lattice.IterProd _≈₂_ _≈ᵘ_ _⊔₂_ _⊔ᵘ_ _⊓₂_ _⊓ᵘ_ lB isLatticeᵘ as IP using (IterProd)
from : {ks : List A} FiniteMap ks IterProd (length ks)
from {[]} (([] , _) , _) = tt
from {k ks'} (((k' , v) kvs' , push _ uks') , refl) = (v , from ((kvs' , uks'), refl))
to : {ks : List A} Unique ks IterProd (length ks) FiniteMap ks
to {[]} _ = (([] , empty) , refl)
to {k ks'} (push k≢ks' uks') (v , rest)
with to uks' rest
... | ((kvs' , ukvs') , refl) = (((k , v) kvs' , push k≢ks' ukvs') , refl)
private
_≈ᵐ_ : {ks : List A} FiniteMap ks FiniteMap ks Set
_≈ᵐ_ {ks} = _≈_ ks
_≈ⁱᵖ_ : {ks : List A} IterProd (length ks) IterProd (length ks) Set
_≈ⁱᵖ_ {ks} = IP._≈_ (length ks)
from-to-inverseˡ : {ks : List A} (uks : Unique ks)
Inverseˡ (_≈ᵐ_ {ks}) (_≈ⁱᵖ_ {ks}) (from {ks}) (to {ks} uks) -- from (to x) = x
from-to-inverseˡ {[]} _ _ = IsEquivalence.≈-refl (IP.≈-equiv 0)
from-to-inverseˡ {k ks'} (push k≢ks' uks') (v , rest)
with ((kvs' , ukvs') , refl) to uks' rest in p rewrite sym p =
(IsLattice.≈-refl lB , from-to-inverseˡ {ks'} uks' rest)
-- the rewrite here is needed because the IH is in terms of `to uks' rest`,
-- but we end up with the 'unpacked' form (kvs', ...). So, put it back
-- in the 'packed' form after we've performed enough inspection
-- to know we take the cons branch of `to`.

View File

@ -1,5 +1,9 @@
open import Lattice open import Lattice
-- 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
-- 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)

View File

@ -1,11 +1,12 @@
open import Lattice open import Lattice
module Lattice.Prod {a} {A B : Set a} module Lattice.Prod {a b} {A : Set a} {B : Set b}
(_≈₁_ : A A Set a) (_≈₂_ : B B Set a) (_≈₁_ : 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 Data.Nat using (; _≤_; _+_; suc) open import Data.Nat using (; _≤_; _+_; suc)
open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂) open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
open import Data.Empty using (⊥-elim) open import Data.Empty using (⊥-elim)
@ -35,7 +36,7 @@ open IsLattice lB using () renaming
; ≺-cong to ≺₂-cong ; ≺-cong to ≺₂-cong
) )
_≈_ : A × B A × B Set a _≈_ : 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) _≈_ ≈-equiv : IsEquivalence (A × B) _≈_