@ -4,7 +4,8 @@
open import Lattice
open import Equivalence
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 Function.Definitions using ( Inverseˡ; Inverseʳ)
@ -27,18 +28,45 @@ 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 Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB using ( subset-impl; locate; forget; _∈_; Map-functional; Expr-Provenance; _∩_; _∪ `_; in ₁; in ₂; bothᵘ; single; ⊔-combines)
open import Lattice.Map A B _≈₂_ _⊔₂_ _⊓₂_ ≡-dec-A lB
using
( subset-impl
; locate; forget
; _∈_
; Map-functional
; Expr-Provenance
; _∩_; _∪ `_
; in ₁; in ₂; bothᵘ; single
; ⊔-combines
)
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ᵘ; ≈-equiv to ≈ᵘ-equiv; fixedHeight to fixedHeightᵘ)
open import Lattice.IterProd _≈₂_ _≈ᵘ_ _⊔₂_ _⊔ᵘ_ _⊓₂_ _⊓ᵘ_ lB isLatticeᵘ as IP using ( IterProd)
open IsLattice lB using ( ) renaming ( ≈-trans to ≈₂-trans; ≈-sym to ≈₂-sym; FixedHeight to FixedHeight₂)
open import Lattice.Unit using ( )
renaming
( _≈_ to _≈ᵘ_
; _⊔_ to _⊔ᵘ_
; _⊓_ to _⊓ᵘ_
; ≈-dec to ≈ᵘ-dec
; isLattice to isLatticeᵘ
; ≈-equiv to ≈ᵘ-equiv
; fixedHeight to fixedHeightᵘ
)
open import Lattice.IterProd _≈₂_ _≈ᵘ_ _⊔₂_ _⊔ᵘ_ _⊓₂_ _⊓ᵘ_ lB isLatticeᵘ
as IP
using ( IterProd)
open IsLattice lB using ( )
renaming
( ≈-trans to ≈₂-trans
; ≈-sym to ≈₂-sym
; FixedHeight to FixedHeight₂
)
from : ∀ { ks : List A} → FiniteMap ks → IterProd ( length ks)
from { []} ( ( [] , _) , _) = tt
from { k ∷ ks'} ( ( ( k' , v) ∷ fm' , push _ uks') , refl) = ( v , from ( ( fm' , uks') , refl) )
from { k ∷ ks'} ( ( ( k' , v) ∷ fm' , push _ uks') , refl) =
( v , from ( ( fm' , uks') , refl) )
to : ∀ { ks : List A} → Unique ks → IterProd ( length ks) → FiniteMap ks
to { []} _ ⊤ = ( ( [] , empty) , refl)
@ -65,17 +93,20 @@ module IterProdIsomorphism where
_⊆ᵐ_ : ∀ { ks₁ ks₂ : List A} → FiniteMap ks₁ → FiniteMap ks₂ → Set
_⊆ᵐ_ fm₁ fm₂ = subset-impl ( proj₁ ( proj₁ fm₁) ) ( proj₁ ( proj₁ fm₂) )
_≈ⁱᵖ_ : ∀ { ks : List A } → IterProd ( legth ks) → IterProd ( legth ks) → Set
_≈ⁱᵖ_ { ks } = IP._≈_ ( legth ks)
_≈ⁱᵖ_ : ∀ { n : ℕ } → IterProd n → IterProd n → Set
_≈ⁱᵖ_ { n } = IP._≈_ n
_⊔ⁱᵖ_ : ∀ { ks : List A} → IterProd ( length ks) → IterProd ( length ks) → IterProd ( length ks)
_⊔ⁱᵖ_ : ∀ { ks : List A} →
IterProd ( length ks) → IterProd ( length ks) → IterProd ( length ks)
_⊔ⁱᵖ_ { ks} = IP._⊔_ ( length ks)
_∈ᵐ_ : ∀ { ks : List A} → A × B → FiniteMap ks → Set
_∈ᵐ_ { ks} k,v fm = k,v ∈ proj₁ fm
-- The left inverse is: from (to x) = x
from-to-inverseˡ : ∀ { ks : List A} ( uks : Unique ks) →
Inverseˡ ( _≈ᵐ_ { ks} ) ( _≈ⁱᵖ_ { ks} ) ( from { ks} ) ( to { ks} uks) -- from (to x) = x
Inverseˡ ( _≈ᵐ_ { ks} ) ( _≈ⁱᵖ_ { length ks} )
( from { ks} ) ( to { ks} uks)
from-to-inverseˡ { []} _ _ = IsEquivalence.≈-refl ( IP.≈-equiv 0 )
from-to-inverseˡ { k ∷ ks'} ( push k≢ks' uks') ( v , rest)
with ( ( fm' , ufm') , refl) ← to uks' rest in p rewrite sym p =
@ -87,33 +118,47 @@ module IterProdIsomorphism where
-- The map has its own uniqueness proof, but the call to 'to' needs a standalone
-- uniqueness proof too. Work with both proofs as needed to thread things through.
--
-- The right inverse is: to (from x) = x
from-to-inverseʳ : ∀ { ks : List A} ( uks : Unique ks) →
Inverseʳ ( _≈ᵐ_ { ks} ) ( _≈ⁱᵖ_ { ks} ) ( from { ks} ) ( to { ks} uks) -- to (from x) = x
from-to-inverseʳ { []} _ ( ( [] , empty) , kvs≡ks) rewrite kvs≡ks = ( ( λ k v ( ) ) , ( λ k v ( ) ) )
from-to-inverseʳ { k ∷ ks'} uks@( push k≢ks'₁ uks'₁) fm₁@( m₁@( ( k , v) ∷ fm'₁ , push k≢ks'₂ uks'₂) , refl)
with to uks'₁ ( from ( ( fm'₁ , uks'₂) , refl) ) | from-to-inverseʳ { ks'} uks'₁ ( ( fm'₁ , uks'₂) , refl)
... | ( ( fm'₂ , ufm'₂) , _) | ( fm'₂⊆fm'₁ , fm'₁⊆fm'₂) = ( m₂⊆m₁ , m₁⊆m₂)
Inverseʳ ( _≈ᵐ_ { ks} ) ( _≈ⁱᵖ_ { length ks} )
( from { ks} ) ( to { ks} uks)
from-to-inverseʳ { []} _ ( ( [] , empty) , kvs≡ks) rewrite kvs≡ks =
( ( λ k v ( ) )
, ( λ k v ( ) )
)
from-to-inverseʳ { k ∷ ks'} uks@( push _ uks'₁) fm₁@( ( ( k , v) ∷ fm'₁ , push _ uks'₂) , refl)
with to uks'₁ ( from ( ( fm'₁ , uks'₂) , refl) )
| from-to-inverseʳ { ks'} uks'₁ ( ( fm'₁ , uks'₂) , refl)
... | ( ( fm'₂ , ufm'₂) , _)
| ( fm'₂⊆fm'₁ , fm'₁⊆fm'₂) = ( m₂⊆m₁ , m₁⊆m₂)
where
kvs₁ = ( k , v) ∷ fm'₁
kvs₂ = ( k , v) ∷ fm'₂
m₁⊆m₂ : subset-impl kvs₁ kvs₂
m₁⊆m₂ k' v' ( here refl) = ( v' , ( IsLattice.≈-refl lB , here refl) )
m₁⊆m₂ k' v' ( here refl) =
( v' , ( IsLattice.≈-refl lB , here refl) )
m₁⊆m₂ k' v' ( there k',v'∈fm'₁) =
let ( v'' , ( v'≈v'' , k',v''∈fm'₂) ) = fm'₁⊆fm'₂ k' v' k',v'∈fm'₁
let ( v'' , ( v'≈v'' , k',v''∈fm'₂) ) =
fm'₁⊆fm'₂ k' v' k',v'∈fm'₁
in ( v'' , ( v'≈v'' , there k',v''∈fm'₂) )
m₂⊆m₁ : subset-impl kvs₂ kvs₁
m₂⊆m₁ k' v' ( here refl) = ( v' , ( IsLattice.≈-refl lB , here refl) )
m₂⊆m₁ k' v' ( here refl) =
( v' , ( IsLattice.≈-refl lB , here refl) )
m₂⊆m₁ k' v' ( there k',v'∈fm'₂) =
let ( v'' , ( v'≈v'' , k',v''∈fm'₁) ) = fm'₂⊆fm'₁ k' v' k',v'∈fm'₂
let ( v'' , ( v'≈v'' , k',v''∈fm'₁) ) =
fm'₂⊆fm'₁ k' v' k',v'∈fm'₂
in ( v'' , ( v'≈v'' , there k',v''∈fm'₁) )
private
first-key-in-map : ∀ { k : A} { ks : List A} ( fm : FiniteMap ( k ∷ ks) ) → Σ B ( λ v → ( k , v) ∈ proj₁ fm)
first-key-in-map : ∀ { k : A} { ks : List A} ( fm : FiniteMap ( k ∷ ks) ) →
Σ B ( λ v → ( k , v) ∈ proj₁ fm)
first-key-in-map ( ( ( k , v) ∷ _ , _) , refl) = ( v , here refl)
from-first-value : ∀ { k : A} { ks : List A} ( fm : FiniteMap ( k ∷ ks) ) → proj₁ ( from fm) ≡ proj₁ ( first-key-in-map fm)
from-first-value : ∀ { k : A} { ks : List A} ( fm : FiniteMap ( k ∷ ks) ) →
proj₁ ( from fm) ≡ proj₁ ( first-key-in-map fm)
from-first-value { k} { ks} ( ( ( k , v) ∷ _ , push _ _) , refl) = refl
-- We need pop because reasoning about two distinct 'refl' pattern
@ -123,109 +168,183 @@ module IterProdIsomorphism where
pop : ∀ { k : A} { ks : List A} → FiniteMap ( k ∷ ks) → FiniteMap ks
pop ( ( ( _ ∷ fm') , push _ ufm') , refl) = ( ( fm' , ufm') , refl)
pop-≈ : ∀ { k : A} { ks : List A} ( fm₁ fm₂ : FiniteMap ( k ∷ ks) ) → fm₁ ≈ᵐ fm₂ → pop fm₁ ≈ᵐ pop fm₂
pop-≈ { k} { ks} fm₁ fm₂ ( fm₁⊆fm₂ , fm₂⊆fm₁) = ( narrow fm₁⊆fm₂ , narrow fm₂⊆fm₁)
pop-≈ : ∀ { k : A} { ks : List A} ( fm₁ fm₂ : FiniteMap ( k ∷ ks) ) →
fm₁ ≈ᵐ fm₂ → pop fm₁ ≈ᵐ pop fm₂
pop-≈ { k} { ks} fm₁ fm₂ ( fm₁⊆fm₂ , fm₂⊆fm₁) =
( narrow fm₁⊆fm₂ , narrow fm₂⊆fm₁)
where
narrow₁ : ∀ { fm₁ fm₂ : FiniteMap ( k ∷ ks) } → fm₁ ⊆ᵐ fm₂ → pop fm₁ ⊆ᵐ fm₂
narrow₁ { ( _ ∷ _ , push _ _) , refl} kvs₁⊆kvs₂ k' v' k',v'∈fm'₁ = kvs₁⊆kvs₂ k' v' ( there k',v'∈fm'₁)
narrow₁ : ∀ { fm₁ fm₂ : FiniteMap ( k ∷ ks) } →
fm₁ ⊆ᵐ fm₂ → pop fm₁ ⊆ᵐ fm₂
narrow₁ { ( _ ∷ _ , push _ _) , refl} kvs₁⊆kvs₂ k' v' k',v'∈fm'₁ =
kvs₁⊆kvs₂ k' v' ( there k',v'∈fm'₁)
narrow₂ : ∀ { fm₁ : FiniteMap ks} { fm₂ : FiniteMap ( k ∷ ks) } → fm₁ ⊆ᵐ fm₂ → fm₁ ⊆ᵐ pop fm₂
narrow₂ : ∀ { fm₁ : FiniteMap ks} { fm₂ : FiniteMap ( k ∷ ks) } →
fm₁ ⊆ᵐ fm₂ → fm₁ ⊆ᵐ pop fm₂
narrow₂ { fm₁} { fm₂ = ( _ ∷ fm'₂ , push k≢ks _) , kvs≡ks@refl} kvs₁⊆kvs₂ k' v' k',v'∈fm'₁
with kvs₁⊆kvs₂ k' v' k',v'∈fm'₁
... | ( v'' , ( v'≈v'' , here refl) ) rewrite sym ( proj₂ fm₁) = ⊥-elim ( All¬-¬Any k≢ks ( forget { m = proj₁ fm₁} k',v'∈fm'₁) )
... | ( v'' , ( v'≈v'' , there k',v'∈fm'₂) ) = ( v'' , ( v'≈v'' , k',v'∈fm'₂) )
... | ( v'' , ( v'≈v'' , here refl) ) rewrite sym ( proj₂ fm₁) =
⊥-elim ( All¬-¬Any k≢ks ( forget { m = proj₁ fm₁} k',v'∈fm'₁) )
... | ( v'' , ( v'≈v'' , there k',v'∈fm'₂) ) =
( v'' , ( v'≈v'' , k',v'∈fm'₂) )
narrow : ∀ { fm₁ fm₂ : FiniteMap ( k ∷ ks) } → fm₁ ⊆ᵐ fm₂ → pop fm₁ ⊆ᵐ pop fm₂
narrow : ∀ { fm₁ fm₂ : FiniteMap ( k ∷ ks) } →
fm₁ ⊆ᵐ fm₂ → pop fm₁ ⊆ᵐ pop fm₂
narrow { fm₁} { fm₂} x = narrow₂ { pop fm₁} ( narrow₁ { fm₂ = fm₂} x)
k,v∈pop⇒k,v∈ : ∀ { k : A} { ks : List A} { k' : A} { v : B} ( fm : FiniteMap ( k ∷ ks) ) → ( k' , v) ∈ᵐ pop fm → ( ¬ k ≡ k' × ( ( k' , v) ∈ᵐ fm) )
k,v∈pop⇒k,v∈ : ∀ { k : A} { ks : List A} { k' : A} { v : B} ( fm : FiniteMap ( k ∷ ks) ) →
( k' , v) ∈ᵐ pop fm → ( ¬ k ≡ k' × ( ( k' , v) ∈ᵐ fm) )
k,v∈pop⇒k,v∈ { k} { ks} { k'} { v} ( m@( ( k , _) ∷ fm' , push k≢ks uks') , refl) k',v∈fm =
( ( λ { refl → All¬-¬Any k≢ks ( forget { m = ( fm' , uks') } k',v∈fm) } ) , there k',v∈fm)
( ( λ { refl → All¬-¬Any k≢ks ( forget { m = ( fm' , uks') } k',v∈fm) } )
, there k',v∈fm
)
k,v∈⇒k,v∈pop : ∀ { k : A} { ks : List A} { k' : A} { v : B} ( fm : FiniteMap ( k ∷ ks) ) → ¬ k ≡ k' → ( k' , v) ∈ᵐ fm → ( k' , v) ∈ᵐ pop fm
k,v∈⇒k,v∈pop { k} { ks} { k'} { v} ( m@( ( k , _) ∷ fm' , push k≢ks uks') , refl) k≢k' ( here refl) = ⊥-elim ( k≢k' refl)
k,v∈⇒k,v∈pop { k} { ks} { k'} { v} ( m@( ( k , _) ∷ fm' , push k≢ks uks') , refl) k≢k' ( there k,v'∈fm') = k,v'∈fm'
k,v∈⇒k,v∈pop : ∀ { k : A} { ks : List A} { k' : A} { v : B} ( fm : FiniteMap ( k ∷ ks) ) →
¬ k ≡ k' → ( k' , v) ∈ᵐ fm → ( k' , v) ∈ᵐ pop fm
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'
Provenance-union : ∀ { ks : List A} ( fm₁ fm₂ : FiniteMap ks) { k : A} { v : B} → ( k , v) ∈ᵐ ( fm₁ ⊔ᵐ fm₂) → Σ ( B × B) ( λ ( v₁ , v₂) → ( ( v ≡ v₁ ⊔₂ v₂) × ( ( 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 k ( ( ` m₁) ∪ ( ` m₂) ) ( forget { m = proj₁ ( fm₁ ⊔ᵐ fm₂) } k,v∈fm₁fm₂)
... | ( _ , ( in ₁ ( single k,v∈m₁) k∉km₂ , _) ) with k∈km₁ ← ( forget { m = m₁} 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 { m = m₂} k,v∈m₂) rewrite trans ks₁≡ks ( sym ks₂≡ks) = ⊥-elim ( k∉km₁ k∈km₂)
... | ( _ , ( in ₁ ( single k,v∈m₁) k∉km₂ , _) )
with k∈km₁ ← ( forget { m = m₁} 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 { m = m₂} k,v∈m₂)
rewrite trans ks₁≡ks ( sym ks₂≡ks) =
⊥-elim ( k∉km₁ k∈km₂)
... | ( v₁⊔v₂ , ( bothᵘ { v₁} { v₂} ( single k,v₁∈m₁) ( single k,v₂∈m₂) , k,v₁⊔v₂∈m₁m₂) )
rewrite Map-functional { m = proj₁ ( fm₁ ⊔ᵐ fm₂) } k,v∈fm₁fm₂ k,v₁⊔v₂∈m₁m₂ = ( ( v₁ , v₂) , ( refl , ( k,v₁∈m₁ , k,v₂∈m₂) ) )
rewrite Map-functional { m = proj₁ ( fm₁ ⊔ᵐ fm₂) } k,v∈fm₁fm₂ k,v₁⊔v₂∈m₁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₂ , _) = ( pfm₁fm₂⊆pfm₁pfm₂ , pfm₁pfm₂⊆pfm₁fm₂)
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₂ , _) =
( pfm₁fm₂⊆pfm₁pfm₂ , pfm₁pfm₂⊆pfm₁fm₂)
where
-- pfm₁fm₂⊆pfm₁pfm₂ = {!!}
pfm₁fm₂⊆pfm₁pfm₂ : pop ( fm₁ ⊔ᵐ fm₂) ⊆ᵐ ( pop fm₁ ⊔ᵐ pop fm₂)
pfm₁fm₂⊆pfm₁pfm₂ k' v' k',v'∈pfm₁fm₂
with ( k≢k' , k',v'∈fm₁fm₂) ← k,v∈pop⇒k,v∈ ( fm₁ ⊔ᵐ fm₂) k',v'∈pfm₁fm₂
with ( ( v₁ , v₂) , ( refl , ( k,v₁∈fm₁ , k,v₂∈fm₂) ) ) ← Provenance-union fm₁ fm₂ k',v'∈fm₁fm₂
with ( ( v₁ , v₂) , ( refl , ( k,v₁∈fm₁ , k,v₂∈fm₂) ) )
← Provenance-union fm₁ fm₂ k',v'∈fm₁fm₂
with k',v₁∈pfm₁ ← k,v∈⇒k,v∈pop fm₁ k≢k' k,v₁∈fm₁
with k',v₂∈pfm₂ ← k,v∈⇒k,v∈pop fm₂ k≢k' k,v₂∈fm₂
= ( v₁ ⊔₂ v₂ , ( IsLattice.≈-refl lB , ⊔-combines { m₁ = proj₁ ( pop fm₁) } { m₂ = proj₁ ( pop fm₂) } k',v₁∈pfm₁ k',v₂∈pfm₂) )
=
( v₁ ⊔₂ v₂
, ( IsLattice.≈-refl lB
, ⊔-combines { m₁ = proj₁ ( pop fm₁) }
{ m₂ = proj₁ ( pop fm₂) }
k',v₁∈pfm₁ k',v₂∈pfm₂
)
)
pfm₁pfm₂⊆pfm₁fm₂ : ( pop fm₁ ⊔ᵐ pop fm₂) ⊆ᵐ pop ( fm₁ ⊔ᵐ fm₂)
pfm₁pfm₂⊆pfm₁fm₂ k' v' k',v'∈pfm₁pfm₂
with ( ( v₁ , v₂) , ( refl , ( k,v₁∈pfm₁ , k,v₂∈pfm₂) ) ) ← Provenance-union ( pop fm₁) ( pop fm₂) k',v'∈pfm₁pfm₂
with ( ( v₁ , v₂) , ( refl , ( k,v₁∈pfm₁ , k,v₂∈pfm₂) ) )
← Provenance-union ( pop fm₁) ( pop fm₂) k',v'∈pfm₁pfm₂
with ( k≢k' , k',v₁∈fm₁) ← k,v∈pop⇒k,v∈ fm₁ k,v₁∈pfm₁
with ( _ , k',v₂∈fm₂) ← k,v∈pop⇒k,v∈ fm₂ k,v₂∈pfm₂
= ( v₁ ⊔₂ v₂ , ( IsLattice.≈-refl lB , k,v∈⇒k,v∈pop ( fm₁ ⊔ᵐ fm₂) k≢k' ( ⊔-combines { m₁ = m₁} { m₂ = m₂} k',v₁∈fm₁ k',v₂∈fm₂) ) )
=
( v₁ ⊔₂ v₂
, ( IsLattice.≈-refl lB
, k,v∈⇒k,v∈pop ( fm₁ ⊔ᵐ fm₂) k≢k'
( ⊔-combines { m₁ = m₁} { m₂ = m₂}
k',v₁∈fm₁ k',v₂∈fm₂)
)
)
from-rest : ∀ { k : A} { ks : List A} ( fm : FiniteMap ( k ∷ ks) ) → proj₂ ( from fm) ≡ from ( pop fm)
from-rest : ∀ { k : A} { ks : List A} ( fm : FiniteMap ( k ∷ ks) ) →
proj₂ ( from fm) ≡ from ( pop fm)
from-rest ( ( ( _ ∷ fm') , push _ ufm') , refl) = refl
from-preserves-≈ : ∀ { ks : List A} → { fm₁ fm₂ : FiniteMap ks} → fm₁ ≈ᵐ fm₂ → ( _≈ⁱᵖ_ { ks} ) ( from fm₁) ( from fm₂)
from-preserves-≈ { []} { ( [] , _) , _} { ( [] , _) , _} _ = IsEquivalence.≈-refl ≈ᵘ-equiv
from-preserves-≈ : ∀ { ks : List A} → { fm₁ fm₂ : FiniteMap ks} →
fm₁ ≈ᵐ fm₂ → ( _≈ⁱᵖ_ { length ks} ) ( from fm₁) ( from fm₂)
from-preserves-≈ { []} { _} { _} _ = IsEquivalence.≈-refl ≈ᵘ-equiv
from-preserves-≈ { k ∷ ks'} { fm₁@( m₁ , _) } { fm₂@( m₂ , _) } fm₁≈fm₂@( kvs₁⊆kvs₂ , kvs₂⊆kvs₁)
with first-key-in-map fm₁ | first-key-in-map fm₂ | from-first-value fm₁ | from-first-value fm₂
with first-key-in-map fm₁
| first-key-in-map fm₂
| from-first-value fm₁
| from-first-value fm₂
... | ( v₁ , k,v₁∈fm₁) | ( v₂ , k,v₂∈fm₂) | refl | refl
with kvs₁⊆kvs₂ _ _ k,v₁∈fm₁
... | ( v₁' , ( v₁≈v₁' , k,v₁'∈fm₂) )
rewrite Map-functional { m = m₂} k,v₂∈fm₂ k,v₁'∈fm₂
rewrite from-rest fm₁ rewrite from-rest fm₂
= ( v₁≈v₁' , from-preserves-≈ { ks'} { pop fm₁} { pop fm₂} ( pop-≈ fm₁ fm₂ fm₁≈fm₂) )
=
( v₁≈v₁'
, from-preserves-≈ { ks'} { pop fm₁} { pop fm₂}
( pop-≈ fm₁ fm₂ fm₁≈fm₂)
)
to-preserves-≈ : ∀ { ks : List A} ( uks : Unique ks) { ip₁ ip₂ : IterProd ( length ks) } → _≈ⁱᵖ_ { ks} ip₁ ip₂ → to uks ip₁ ≈ᵐ to uks ip₂
to-preserves-≈ : ∀ { ks : List A} ( uks : Unique ks) { ip₁ ip₂ : IterProd ( length ks) } →
_≈ⁱᵖ_ { length ks} ip₁ ip₂ → to uks ip₁ ≈ᵐ to uks ip₂
to-preserves-≈ { []} empty { tt} { tt} _ = ( ( λ k v ( ) ) , ( λ k v ( ) ) )
to-preserves-≈ { k ∷ ks'} uks@( push k≢ks' uks') { ip₁@( v₁ , rest₁) } { ip₂@( v₂ , rest₂) } ( v₁≈v₂ , rest₁≈rest₂) = ( fm₁⊆fm₂ , fm₂⊆fm₁)
where
fm₁⊆fm₂ : to uks ip₁ ⊆ᵐ to uks ip₂
fm₁⊆fm₂ k v k,v∈kvs₁
inductive-step : ∀ { v₁ v₂ : B} { rest₁ rest₂ : IterProd ( length ks') } →
v₁ ≈₂ v₂ → _≈ⁱᵖ_ { length ks'} rest₁ rest₂ →
to uks ( v₁ , rest₁) ⊆ᵐ to uks ( v₂ , rest₂)
inductive -step { v₁} { v₂} { rest₁} { rest₂} v₁≈v₂ rest₁≈rest₂ k v k,v∈kvs₁
with ( ( fm'₁ , ufm'₁) , fm'₁≡ks') ← to uks' rest₁ in p₁
with ( ( fm'₂ , ufm'₂) , fm'₂≡ks') ← to uks' rest₂ in p₂
with k,v∈kvs₁
... | here refl = ( v₂ , ( v₁≈v₂ , here refl) )
... | there k,v∈fm'₁ with refl ← p₁ with refl ← p₂ = let ( v' , ( v≈v' , k,v'∈kvs₁) ) = proj₁ ( to-preserves-≈ uks' { rest₁} { rest₂} rest₁≈rest₂) k v k,v∈fm'₁ in ( v' , ( v≈v' , there k,v'∈kvs₁) )
... | there k,v∈fm'₁ with refl ← p₁ with refl ← p₂ =
let
( fm'₁⊆fm'₂ , _) = to-preserves-≈ uks' { rest₁} { rest₂}
rest₁≈rest₂
( v' , ( v≈v' , k,v'∈kvs₁) ) = fm'₁⊆fm'₂ k v k,v∈fm'₁
in
( v' , ( v≈v' , there k,v'∈kvs₁) )
fm₁⊆fm₂ : to uks ip₁ ⊆ᵐ to uks ip₂
fm₁⊆fm₂ = inductive -step v₁≈v₂ rest₁≈rest₂
fm₂⊆fm₁ : to uks ip₂ ⊆ᵐ to uks ip₁
fm₂⊆fm₁ k v k,v∈kvs₂
with ( ( fm'₁ , ufm'₁) , fm'₁≡ks') ← to uks' rest₁ in p₁
with ( ( fm'₂ , ufm'₂) , fm'₂≡ks') ← to uks' rest₂ in p₂
with k,v∈kvs₂
... | here refl = ( v₁ , ( IsLattice.≈-sym lB v₁≈v₂ , here refl) )
... | there k,v∈fm'₂ with refl ← p₁ with refl ← p₂ = let ( v' , ( v≈v' , k,v'∈kvs₂) ) = proj₂ ( to-preserves-≈ uks' { rest₁} { rest₂} rest₁≈rest₂) k v k,v∈fm'₂ in ( v' , ( v≈v' , there k,v'∈kvs₂) )
fm₂⊆fm₁ = inductive -step ( ≈₂-sym v₁≈v₂)
( IP.≈-sym ( length ks') rest₁≈rest₂)
from-⊔-distr : ∀ { ks : List A} → ( fm₁ fm₂ : FiniteMap ks) → _≈ⁱᵖ_ { ks} ( from ( fm₁ ⊔ᵐ fm₂) ) ( _⊔ⁱᵖ_ { ks} ( from fm₁) ( from fm₂) )
from-⊔-distr : ∀ { ks : List A} → ( fm₁ fm₂ : FiniteMap ks) →
_≈ⁱᵖ_ { length ks} ( from ( fm₁ ⊔ᵐ fm₂) )
( _⊔ⁱᵖ_ { ks} ( from fm₁) ( from fm₂) )
from-⊔-distr { []} fm₁ fm₂ = IsEquivalence.≈-refl ≈ᵘ-equiv
from-⊔-distr { k ∷ ks} fm₁@( m₁ , _) fm₂@( m₂ , _)
with first-key-in-map ( fm₁ ⊔ᵐ fm₂) | first-key-in-map fm₁ | first-key-in-map fm₂ | from-first-value ( fm₁ ⊔ᵐ fm₂) | from-first-value fm₁ | from-first-value fm₂
with first-key-in-map ( fm₁ ⊔ᵐ fm₂)
| first-key-in-map fm₁
| first-key-in-map fm₂
| from-first-value ( fm₁ ⊔ᵐ fm₂)
| from-first-value fm₁ | from-first-value fm₂
... | ( v , k,v∈fm₁fm₂) | ( v₁ , k,v₁∈fm₁) | ( v₂ , k,v₂∈fm₂) | refl | refl | refl
with Expr-Provenance k ( ( ` m₁) ∪ ( ` m₂) ) ( forget { m = proj₁ ( fm₁ ⊔ᵐ fm₂) } k,v∈fm₁fm₂)
... | ( _ , ( in ₁ _ k∉km₂ , _) ) = ⊥-elim ( k∉km₂ ( forget { m = m₂} k,v₂∈fm₂) )
... | ( _ , ( in ₂ k∉km₁ _ , _) ) = ⊥-elim ( k∉km₁ ( forget { m = m₁} k,v₁∈fm₁) )
... | ( _ , ( in ₁ _ k∉km₂ , _) ) = ⊥-elim ( k∉km₂ ( forget { m = m₂}
k,v₂∈fm₂) )
... | ( _ , ( in ₂ k∉km₁ _ , _) ) = ⊥-elim ( k∉km₁ ( forget { m = m₁}
k,v₁∈fm₁) )
... | ( v₁⊔v₂ , ( bothᵘ { v₁'} { v₂'} ( single k,v₁'∈m₁) ( single k,v₂'∈m₂) , k,v₁⊔v₂∈m₁m₂) )
rewrite Map-functional { m = m₁} k,v₁∈fm₁ k,v₁'∈m₁
rewrite Map-functional { m = m₂} k,v₂∈fm₂ k,v₂'∈m₂
rewrite Map-functional { m = proj₁ ( fm₁ ⊔ᵐ fm₂) } k,v∈fm₁fm₂ k,v₁⊔v₂∈m₁m₂
rewrite from-rest ( fm₁ ⊔ᵐ fm₂) rewrite from-rest fm₁ rewrite from-rest fm₂
= ( IsLattice.≈-refl lB
, IsEquivalence.≈-trans ( IP.≈-equiv ( length ks) ) ( from-preserves-≈ { _} { pop ( fm₁ ⊔ᵐ fm₂) } { pop fm₁ ⊔ᵐ pop fm₂} ( pop-⊔-distr fm₁ fm₂) ) ( ( from-⊔-distr ( pop fm₁) ( pop fm₂) ) )
, IsEquivalence.≈-trans
( IP.≈-equiv ( length ks) )
( from-preserves-≈ { _} { pop ( fm₁ ⊔ᵐ fm₂) }
{ pop fm₁ ⊔ᵐ pop fm₂}
( pop-⊔-distr fm₁ fm₂) )
( ( from-⊔-distr ( pop fm₁) ( pop fm₂) ) )
)
to-⊔-distr : ∀ { ks : List A} ( uks : Unique ks) → ( ip₁ ip₂ : IterProd ( length ks) ) → to uks ( _⊔ⁱᵖ_ { ks} ip₁ ip₂) ≈ᵐ ( to uks ip₁ ⊔ᵐ to uks ip₂)
to-⊔-distr : ∀ { ks : List A} ( uks : Unique ks) → ( ip₁ ip₂ : IterProd ( length ks) ) →
to uks ( _⊔ⁱᵖ_ { ks} ip₁ ip₂) ≈ᵐ ( to uks ip₁ ⊔ᵐ to uks ip₂)
to-⊔-distr { []} empty tt tt = ( ( λ k v ( ) ) , ( λ k v ( ) ) )
to-⊔-distr { ks@( k ∷ ks') } uks@( push k≢ks' uks') ip₁@( v₁ , rest₁) ip₂@( v₂ , rest₂) = ( fm⊆fm₁fm₂ , fm₁fm₂⊆fm)
where
@ -239,27 +358,45 @@ module IterProdIsomorphism where
fm⊆fm₁fm₂ k v ( here refl) =
( v₁ ⊔₂ v₂
, ( IsLattice.≈-refl lB
, ⊔-combines { k} { v₁} { v₂} { proj₁ fm₁} { proj₁ fm₂} ( here refl) ( here refl)
, ⊔-combines { k} { v₁} { v₂} { proj₁ fm₁} { proj₁ fm₂}
( here refl) ( here refl)
)
)
fm⊆fm₁fm₂ k' v ( there k',v∈fm')
with ( fm'⊆fm'₁fm'₂ , _) ← to-⊔-distr uks' rest₁ rest₂
with ( v' , ( v₁⊔v₂≈v' , k',v'∈fm'₁fm'₂) ) ← fm'⊆fm'₁fm'₂ k' v k',v∈fm'
with ( _ , ( refl , ( v₁∈fm'₁ , v₂∈fm'₂) ) ) ← Provenance-union fm₁' fm₂' k',v'∈fm'₁fm'₂ =
( v' , ( v₁⊔v₂≈v' , ⊔-combines { m₁ = proj₁ fm₁} { m₂ = proj₁ fm₂} ( there v₁∈fm'₁) ( there v₂∈fm'₂) ) )
with ( v' , ( v₁⊔v₂≈v' , k',v'∈fm'₁fm'₂) )
← fm'⊆fm'₁fm'₂ k' v k',v∈fm'
with ( _ , ( refl , ( v₁∈fm'₁ , v₂∈fm'₂) ) )
← Provenance-union fm₁' fm₂' k',v'∈fm'₁fm'₂ =
( v'
, ( v₁⊔v₂≈v'
, ⊔-combines { m₁ = proj₁ fm₁} { m₂ = proj₁ fm₂}
( there v₁∈fm'₁) ( there v₂∈fm'₂)
)
)
fm₁fm₂⊆fm : ( fm₁ ⊔ᵐ fm₂) ⊆ᵐ fm
fm₁fm₂⊆fm k' v k',v∈fm₁fm₂
with ( _ , fm'₁fm'₂⊆fm') ← to-⊔-distr uks' rest₁ rest₂
with ( _ , ( refl , ( v₁∈fm₁ , v₂∈fm₂) ) ) ← Provenance-union fm₁ fm₂ k',v∈fm₁fm₂
with ( _ , fm'₁fm'₂⊆fm')
← to-⊔-distr uks' rest₁ rest₂
with ( _ , ( refl , ( v₁∈fm₁ , v₂∈fm₂) ) )
← Provenance-union fm₁ fm₂ k',v∈fm₁fm₂
with v₁∈fm₁ | v₂∈fm₂
... | here refl | here refl = ( v , ( IsLattice.≈-refl lB , here refl) )
... | here refl | there k',v₂∈fm₂' = ⊥-elim ( All¬-¬Any k≢ks' ( subst ( λ list → k' ∈ˡ list) ( proj₂ fm₂') ( forget { m = proj₁ fm₂'} k',v₂∈fm₂') ) )
... | there k',v₁∈fm₁' | here refl = ⊥-elim ( All¬-¬Any k≢ks' ( subst ( λ list → k' ∈ˡ list) ( proj₂ fm₁') ( forget { m = proj₁ fm₁'} k',v₁∈fm₁') ) )
... | here refl | here refl =
( v , ( IsLattice.≈-refl lB , here refl) )
... | here refl | there k',v₂∈fm₂' =
⊥-elim ( All¬-¬Any k≢ks' ( subst ( k' ∈ˡ_) ( proj₂ fm₂')
( forget { m = proj₁ fm₂'} k',v₂∈fm₂') ) )
... | there k',v₁∈fm₁' | here refl =
⊥-elim ( All¬-¬Any k≢ks' ( subst ( k' ∈ˡ_) ( proj₂ fm₁')
( forget { m = proj₁ fm₁'} k',v₁∈fm₁') ) )
... | there k',v₁∈fm₁' | there k',v₂∈fm₂' =
let
k',v₁v₂∈fm₁'fm₂' = ⊔-combines { m₁ = proj₁ fm₁'} { m₂ = proj₁ fm₂'} k',v₁∈fm₁' k',v₂∈fm₂'
( v' , ( v₁⊔v₂≈v' , v'∈fm') ) = fm'₁fm'₂⊆fm' _ _ k',v₁v₂∈fm₁'fm₂'
k',v₁v₂∈fm₁'fm₂' =
⊔-combines { m₁ = proj₁ fm₁'} { m₂ = proj₁ fm₂'}
k',v₁∈fm₁' k',v₂∈fm₂'
( v' , ( v₁⊔v₂≈v' , v'∈fm') ) =
fm'₁fm'₂⊆fm' _ _ k',v₁v₂∈fm₁'fm₂'
in
( v' , ( v₁⊔v₂≈v' , there v'∈fm') )
