Geek asks and answers

Checking unionWith connection termination

I had a problem with checking for completion, very similar to that described in this question , as well as this Agda Error / Error Report / Function .

The problem convinces the compiler that the next one is unionWithending. Using the join function for duplicate keys, unionWithcombines two cards, presented in the form of lists of pairs (key, value), sorted by key. The Key parameter of the final display is the (inflexible) lower boundary of the keys contained in the map. (One of the reasons for defining this data type is to provide a semantic domain into which I can interpret AVL trees to prove various properties about them.)

open import Function
open import Relation.Binary renaming (IsEquivalence to IsEq)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

module FiniteMap
   {k v ℓ ℓ′}
   {Key : Set k}
   (Value : Set v)
   {_<_ : Rel Key ℓ}
   (isStrictTotalOrder : IsStrictTotalOrder _≡_ _<_)
   {_≈_ : Rel Value ℓ′}
   (isEquivalence : IsEq _≈_)
   where

   open import Algebra.FunctionProperties
   open import Data.Product
   open IsStrictTotalOrder isStrictTotalOrder
   open import Level

   KV : Set (k ⊔ v)
   KV = Key × Value

   data FiniteMap (l : Key) : Set (k ⊔ v ⊔ ℓ) where
      [] : FiniteMap l
      _∷_ : (kv : KV) → let k = proj₁ kv in l < k → (m : FiniteMap k) → FiniteMap l

   unionWith : ∀ {l} → Op₂ Value → Op₂ (FiniteMap l)
   unionWith _ [] [] = []
   unionWith _ [] m = m
   unionWith _ m [] = m
   unionWith _⊕_ (_∷_ (k , v) k<l m) (_∷_ (k′ , v′) k′<l m′) with compare k k′
   ... | tri< k<k′ _ _ = _∷_ (k , v) k<l (unionWith _⊕_ m (_∷_ (k′ , v′) k<k′ m′))
   ... | tri≈ _ k≡k′ _ rewrite P.sym k≡k′ = {!!} --_∷_ (k , v ⊕ v′) k<l (unionWith _⊕_ m m′)
   ... | tri> _ _ k′<k = _∷_ (k′ , v′) k′<l (unionWith _⊕_ (_∷_ (k , v) k′<k m) m′)

, , , . , unionWith', unionWith, k' < k:

   unionWith : ∀ {l} → Op₂ Value → Op₂ (FiniteMap l)
   unionWith′ : ∀ {l} → Op₂ Value → (kv : KV) → let k = proj₁ kv in l < k → FiniteMap k → Op₁ (FiniteMap l)

   unionWith _ [] [] = []
   unionWith _ [] m = m
   unionWith _ m [] = m
   unionWith _⊕_ (_∷_ (k , v) k<l m) (_∷_ (k′ , v′) k′<l m′) with compare k k′
   ... | tri< k<k′ _ _ = _∷_ (k , v) k<l (unionWith _⊕_ m (_∷_ (k′ , v′) k<k′ m′))
   ... | tri≈ _ k≡k′ _ rewrite P.sym k≡k′ = {!!} --_∷_ (k , v ⊕ v′) k<l (unionWith _⊕_ m m′)
   ... | tri> _ _ k′<k = _∷_ (k′ , v′) k′<l (unionWith′ _⊕_ (k , v) k′<k m m′)

   unionWith′ _ (k , v) l<k m [] = _∷_ (k , v) l<k m
   unionWith′ _⊕_ (k , v) l<k m (_∷_ (k′ , v′) k′<l m′) with compare k k′
   ... | tri< k<k′ _ _ = {!!}
   ... | tri≈ _ k≡k′ _ = {!!}
   ... | tri> _ _ k′<k = _∷_ (k′ , v′) k′<l (unionWith′ _⊕_ (k , v) k′<k m m′)

, unionWith' unionWith, .

with, compare . ( with, , , .)

with ? , , , , .

(, Agda , , .)

+1
2

, . Data.Extended-key , , Data.AVL.Extended-key .

:

{-# OPTIONS --sized-types #-}

open import Relation.Binary renaming (IsStrictTotalOrder to IsSTO)
open import Relation.Binary.PropositionalEquality as P using (_≡_)

-- A list of (key, value) pairs, sorted by key in strictly descending order.
module Temp
   {𝒌 𝒗 ℓ}
   {Key : Set 𝒌}
   (Value : Key → Set 𝒗)
   {_<_ : Rel Key ℓ}
   (isStrictTotalOrder′ : IsSTO _≡_ _<_)
   where

   open import Algebra.FunctionProperties
   open import Data.Extended-key isStrictTotalOrder′
   open import Function
   open import Level
   open import Size
   open IsStrictTotalOrder isStrictTotalOrder

FiniteMap, .

   data FiniteMap (l u : Key⁺) : {ι : Size} → Set (𝒌 ⊔ 𝒗 ⊔ ℓ) where
      [] : {ι : _} → .(l <⁺ u) → FiniteMap l u {↑ ι}
      _↦_∷[_]_ : {ι : _} (k : Key) (v : Value k) → .(l <⁺ [ k ]) → 
                 (m : FiniteMap [ k ] u {ι}) → FiniteMap l u {↑ ι}

   infixr 3 _↦_∷[_]_

unionWith, , .

   unionWith : ∀ {l u} → (∀ {k} → Op₂ (Value k)) →
               {ι : Size} → FiniteMap l u {ι} → {ι′ : Size} → 
               FiniteMap l u {ι′} → FiniteMap l u
   unionWith _ ([] l<⁺u) ([] _) = [] l<⁺u
   unionWith _ ([] _) m = promote m
   unionWith _ m ([] _ )= promote m
   unionWith ∙ (k ↦ v ∷[ _ ] m) (k′ ↦ v′ ∷[ _ ] m′) with compare [ k ] [ k′ ]
   ... | (tri< k<⁺k′ _ _) = k ↦ v ∷[ _ ] unionWith ∙ m (k′ ↦ v′ ∷[ _ ] m′)
   unionWith ∙ (k ↦ v ∷[ l<⁺k ] m) (.k ↦ v′ ∷[ _ ] m′) | (tri≈ _ P.refl _) =
      k ↦ (v ⟨ ∙ ⟩ v′) ∷[ l<⁺k ] unionWith ∙ m m′
   ... | (tri> _ _ k′<⁺k) = k′ ↦ v′ ∷[ _ ] unionWith ∙ (k ↦ v ∷[ _ ] m) m′

, ∞, .

   unionWith′ : ∀ {l u} → (∀ {k} → Op₂ (Value k)) → Op₂ (FiniteMap l u)
   unionWith′ ∙ x y = unionWith ∙ x y

unionWith .

, , , . , , , .

+1

, , , , Agda 2.3.3+. ∷.

data FiniteMap (l : Key) : Set (k ⊔ v ⊔ ℓ) where
   [] : FiniteMap l
   _∷[_]_ : (kv : KV) → let k = proj₁ kv in l < k → (m : FiniteMap k) → FiniteMap l

-- Split into two definitions to help the termination checker.
unionWith : ∀ {l} → Op₂ Value → Op₂ (FiniteMap l)
unionWith′ : ∀ {l} → Op₂ Value → (kv : KV) → let k = proj₁ kv in l < k → FiniteMap k → Op₁ (FiniteMap l)

unionWith _ [] [] = []
unionWith _ [] m = m
unionWith _ m [] = m
unionWith _⊕_ ((k , v) ∷[ k<l ] m) ((k′ , v′) ∷[ k′<l ] m′) with compare k k′
... | tri< k<k′ _ _ = (k , v) ∷[ k<l ] (unionWith _⊕_ m ((k′ , v′) ∷[ k<k′ ] m′))
... | tri≈ _ k≡k′ _ rewrite P.sym k≡k′ = (k , v ⊕ v′) ∷[ k<l ] (unionWith _⊕_ m m′)
... | tri> _ _ k′<k = (k′ , v′) ∷[ k′<l ] (unionWith′ _⊕_ (k , v) k′<k m m′)

unionWith′ _ (k , v) l<k m [] = (k , v) ∷[ l<k ] m
unionWith′ _⊕_ (k , v) l<k m ((k′ , v′) ∷[ k′<l ] m′) with compare k k′
... | tri< k<k′ _ _ = (k , v) ∷[ l<k ] (unionWith _⊕_ m ((k′ , v′) ∷[ k<k′ ] m′))
... | tri≈ _ k≡k′ _ rewrite P.sym k≡k′ = (k , v ⊕ v′) ∷[ l<k ] (unionWith _⊕_ m m′)
... | tri> _ _ k′<k = (k′ , v′) ∷[ k′<l ] (unionWith′ _⊕_ (k , v) k′<k m m′)
+1

More articles:


All Articles