Termination check on unionWith

Question

I'm having a problem with termination checking, very similar to the one described in this question and also this Agda bug report/feature request.

The problem is convincing the compiler that the following unionWith terminates. Using a combining function for duplicate keys, unionWith merges two maps represented as lists of (key, value) pairs sorted by key. The Key parameter of a finite map is a (non-tight) lower bound on the keys contained in the map. (One reason for defining this data type is to provide a semantic domain into which I can interpret AVL trees in order 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′)

I've been unable to generalise the solutions discussed in the referenced question to my setting. For example if I introduce an auxiliary function unionWith', defined mutually recursively with unionWith, which is invoked from the latter in the k' < k case:

   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′)

then as soon as I tie the recursive knot by replacing the first missing case in unionWith' with the required call to unionWith, it fails to termination-check.

I also tried introducing additional with patterns, but that's complicated by need to use the result of compare in the recursive calls. (If I use nested with clauses that doesn't seem to help the termination checker.)

Is there a way to use with patterns or auxiliary functions to get this compiling? It seems like a straightforward enough situation, so I'm hoping it just a case of knowing the right trick.

(Maybe the new termination checker in the Agda development branch can deal with this, but I'd like to avoid installing a development version unless I have to.)

Answer 1

It seems the first solution proposed for the earlier list-merge question does indeed work here, but only under Agda version 2.3.3+. Here's the full version, with a slightly nicer syntax for ∷.

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′)

Answer 2

Here's an alternative based on sized types, based on the answer to this later question. You can pick up the Data.Extended-key module from here, or you can tweak the code below so that it uses Data.AVL.Extended-key from the standard library instead.

Preamble:

{-# 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

Now the FiniteMap definition, augmented with size indices.

   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 _↦_∷[_]_

Then we can write a version unionWith that termination-checks, without cheesing around with auxiliary functions.

   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′

We will almost certainly need a version where all the indices are ∞, but that's a minor inconvenience.

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

Proving a property of unionWith using a recursive function will generally require indices to be used in a similar way.

I'm not yet convinced that I won't run into subtleties with more involved use of size indices, but so far I'm impressed by how unintrusive they are. It's certainly less boilerplate than required with the usual Agda termination hacks.