Termination check on unionWith

Question 1

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.

Question 2

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