From 2a06e6ae2d5fb7eb6d74a99de3208dbba4cc9287 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 25 Feb 2024 12:17:19 -0800 Subject: [PATCH] Adjust 'to' to make it easier to reason about Signed-off-by: Danila Fedorin --- Lattice/FiniteValueMap.agda | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/Lattice/FiniteValueMap.agda b/Lattice/FiniteValueMap.agda index 8bc8cae..7eed51b 100644 --- a/Lattice/FiniteValueMap.agda +++ b/Lattice/FiniteValueMap.agda @@ -19,6 +19,8 @@ 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 Data.List.Relation.Unary.All using (All) +open import Relation.Nullary using (¬_) open import Lattice.FiniteMap A B _≈₂_ _⊔₂_ _⊓₂_ ≈-dec-A lB public @@ -35,7 +37,15 @@ module IterProdIsomorphism where 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) + ... | ((kvs' , ukvs') , kvs'≡ks') = + let + -- This would be easier if we pattern matched on the equiality proof + -- to get refl, but that makes it harder to reason about 'to' when + -- the arguments are not known to be refl. + k≢kvs' = subst (λ ks → All (λ k' → ¬ k ≡ k') ks) (sym kvs'≡ks') k≢ks' + kvs≡ks = cong (k ∷_) kvs'≡ks' + in + (((k , v) ∷ kvs' , push k≢kvs' ukvs') , kvs≡ks) private