Prove the other direction for inverses.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
99fc21cef2
commit
b96bac5518
|
@ -20,8 +20,10 @@ open import Utils using (Unique; push; empty)
|
|||
open import Data.Product using (_,_)
|
||||
open import Data.List.Properties using (∷-injectiveʳ)
|
||||
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)
|
||||
open import Lattice.FiniteMap A B _≈₂_ _⊔₂_ _⊓₂_ ≈-dec-A lB public
|
||||
|
||||
module IterProdIsomorphism where
|
||||
|
@ -65,3 +67,27 @@ module IterProdIsomorphism where
|
|||
-- 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`.
|
||||
|
||||
-- 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.
|
||||
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) ∷ kvs'₁ , push k≢ks'₂ uks'₂) , refl)
|
||||
with to uks'₁ (from ((kvs'₁ , uks'₂) , refl)) | from-to-inverseʳ {ks'} uks'₁ ((kvs'₁ , uks'₂) , refl)
|
||||
... | ((kvs'₂ , ukvs'₂) , _) | (kvs'₂⊆kvs'₁ , kvs'₁⊆kvs'₂) = (m₂⊆m₁ , m₁⊆m₂)
|
||||
where
|
||||
kvs₁ = (k , v) ∷ kvs'₁
|
||||
kvs₂ = (k , v) ∷ kvs'₂
|
||||
|
||||
m₁⊆m₂ : subset-impl kvs₁ kvs₂
|
||||
m₁⊆m₂ k' v' (here refl) = (v' , (IsLattice.≈-refl lB , here refl))
|
||||
m₁⊆m₂ k' v' (there k',v'∈kvs'₁) =
|
||||
let (v'' , (v'≈v'' , k',v''∈kvs'₂)) = kvs'₁⊆kvs'₂ k' v' k',v'∈kvs'₁
|
||||
in (v'' , (v'≈v'' , there k',v''∈kvs'₂))
|
||||
|
||||
m₂⊆m₁ : subset-impl kvs₂ kvs₁
|
||||
m₂⊆m₁ k' v' (here refl) = (v' , (IsLattice.≈-refl lB , here refl))
|
||||
m₂⊆m₁ k' v' (there k',v'∈kvs'₂) =
|
||||
let (v'' , (v'≈v'' , k',v''∈kvs'₁)) = kvs'₂⊆kvs'₁ k' v' k',v'∈kvs'₂
|
||||
in (v'' , (v'≈v'' , there k',v''∈kvs'₁))
|
||||
|
|
Loading…
Reference in New Issue
Block a user