Convincing Agda that a recursive function is terminating

Question

I'm having some trouble convincing Agda that an argument in a recursive call to a function is structurally smaller than the incoming argument.

I have defined pairs, lists of pairs (representing finite functions as "sets" of input/output pairs), and unions of such lists as follows:

data _x_ {l : Level} (A B : Set l) : Set l where
  <_,_> : A -> B → A x B

data FinFun (A B : Set) : Set where
  nil : FinFun A B
  _::_ : A x B → FinFun A B → FinFun A B

_U_ : {A B : Set} -> FinFun A B -> FinFun A B -> FinFun A B
nil U f' = f'
(x :: xs) U f' = x :: (xs U f')

I have also defined "neighborhoods" and the supremum of two such neighborhoods:

data UniNbh : Set where
  bot : UniNbh
  lam : FinFun UniNbh UniNbh -> UniNbh

_u_ : UniNbh -> UniNbh -> UniNbh
bot u bot = bot
bot u (lam f) = lam f
(lam f) u bot = lam f
(lam f) u (lam f') = lam (f U f')

Finally, and most importantly for this question, I have defined a function which, given a list of pairs of neighborhoods, takes the supremum of all the first components of the pairs in the list:

pre : FinFun UniNbh UniNbh -> UniNbh
pre nil = bot
pre (< x , y > :: f) = x u pre f

The mutually recursive function that causes me trouble essentially looks like this:

f : UniNbh -> UniNbh -> UniNbh -> Result
-- Base cases here. When any argument is bot or lam nil, no
-- recursion is needed.
f (lam (a ∷ as)) (lam (b ∷ bs)) (lam (c ∷ cs)) =
  f (lam (a ∷ as)) (pre (b ∷ bs)) (lam (c ∷ cs))

It seems obvious that either pre f is smaller than lam f, or that one of the base cases will end the recursion, but Agda understandably can't see this. I have tried quite a few different ideas in trying to solve this, but they haven't worked. At this point, I think that the only way is to use Induction.WellFounded from the standard library, but I can't figure out how.

I've unsuccessfully tried to show that the following data type is well founded:

data preSmaller : UniNbh -> UniNbh -> Set where
  pre-base : preSmaller (pre nil) (lam nil)
  pre-step : ∀ (x y f f') ->
             preSmaller (pre f) (lam f') ->
             preSmaller  (pre (< x , y > :: f')) (lam (< x , y > :: f'))

I'm not even sure that this data type would be useful, even if I could prove that it's well founded.

When looking around trying to find information about how to use Induction.WellFounded, I can only find very simple examples showing that < for natural numbers is well founded, and I haven't been able to generalize those ideas to this situtation.

Sorry for the long post. Any help would be greatly appreciated!

Answer 1

I can't see the whole of the definitions because of some unicode - many characters you introduced get rendered as squares. The basic idea of WellFounded is not the proof that some data type gets smaller. The basic idea is that Agda can see Acc _<_ x constructed by accessor function wrapped in Acc _<_ y gets smaller.

In your case it seems as though preSmaller is such a _<_. It's hard to judge if that is so, because a lot of text is missing. Then you'd need to construct a function that can build an Acc preSmaller y for any two given x y : UniNbh.

---

The edited question still misses some of the definitions (like, what is post nil. But I get the gist of what is happening.

Your definition of preSmaller is similar to the following definition of _<_ for Nat:

data _<_ : Nat -> Nat -> Set where
   z<  : {n : Nat} -> zero < (succ n)
   s<s : {m n : Nat} -> m < n -> (succ m) < (succ n)

Note that it is different from the standard definition, because both m and n get bigger. This affects the construction of proof of WellFounded-ness.

-- may just as well import, but let me be self-contained:
data Acc {A : Set} (_<_ : A -> A -> Set) (x : A) : Set where
   acc : ((y : A) -> y < x -> Acc _<_ y) -> Acc _<_ x

Well-founded : (A : Set) -> (R : A -> A -> Set) -> Set
Well-founded A _<_ = (x : A) -> Acc _<_ x

{-# BUILTIN EQUALITY _==_ #-} -- rewrite rule needs this, if I am not using
-- Unicode version of it from Prelude
<-Well-founded : Well-founded Nat _<_
<-Well-founded zero     = acc \_ ()
<-Well-founded (succ x) = acc aux where
   aux : (y : Nat) -> y < (succ x) -> Acc _<_ y
   aux zero     _                                 = <-Well-founded zero
   aux (succ y) (s<s y<x) with <-Well-founded x | is-eq? (succ y) x
   ...          | acc f | no  sy!=x               = f (succ y) (neq y<x sy!=x)
   ...          | wf-x  | yes sy==x rewrite sy==x = wf-x

Helper functions:

data False : Set where

false-elim : {A : Set} -> False -> A
false-elim ()

data Dec (A : Set) : Set where
   yes : A -> Dec A
   no  : (A -> False) -> Dec A

_==?_ : {A : Set} -> A -> A -> Set
_==?_ x y = Dec (x == y)

s== : {m n : Nat} -> (succ m) == (succ n) -> m == n
s== refl = refl

is-eq? : (m n : Nat) -> m ==? n
is-eq? zero     zero     = yes refl
is-eq? (succ m) zero     = no \()
is-eq? zero     (succ n) = no \()
is-eq? (succ m) (succ n) with is-eq? m n
...                        | no  f   = no \sm=sn -> f (s== sm=sn)
...                        | yes m=n = yes (cong succ m=n)

-- if m < n and m+1 /= n, then m+1 < n
neq : {m n : Nat} -> m < n -> ((succ m) == n -> False) -> (succ m) < n
neq {_}      {zero}          ()
neq {zero}   {succ zero}     z<        f = false-elim (f refl)
neq {zero}   {succ (succ n)} z<        f = s<s z<
neq {succ m} {succ n}        (s<s m<n) f = s<s (neq m<n \m=n -> f (cong succ m=n))

The important things to take away:

The standard definition of _<_ allows to build simpler proof of WellFounded-ness, because it is possible to decrement one of the arguments at a time. A different definition of _<_ requires reduction of both, and that seems to be a problem. Yet, with the helper function neq it is possible to construct a recursion where only one and the same of the arguments gets smaller.

Decidability of _==_ for Nat allows me to build such recursion. Agda can see that the recursive call to <-WellFounded is for a structurally smaller x, so that terminates. Then the result of that is used differently based on the outcome of equality test. The branch using neq computes the necessary Acc given the function that <-WellFounded discovered for smaller x: the function terminates, because Agda allowed construction of such a function. The other branch, where x == (succ y), uses the value as-is, because rewrite convinces Agda that it is of the right type.

---

Well-foundedness then can be used to prove a function terminates, by constructing an instance of <-WellFounded:

_-|-_ : Bin -> Bin -> Bin
x -|- y with max-len x y
...   | n , (x<n , y<n) = Sigma.fst (a (<-Well-founded n) b (x , x<n) (y , y<n)) where
  a : {n : Nat} -> Acc _<_ n -> Bin -> S-Bin n -> S-Bin n -> S-Bin (succ n)
  a+O : {n : Nat} -> Acc _<_ n -> Bin -> S-Bin n -> S-Bin n -> S-Bin (succ (succ n))
  a+I : {n : Nat} -> Acc _<_ n -> Bin -> S-Bin n -> S-Bin n -> S-Bin (succ (succ n))

  a+O f c m n with a f c m n
  ...                | r , r<n = r O , s<s r<n

  a+I f c m n with a f c m n
  ...                | r , r<n = r I , s<s r<n

  a {zero} _ _ (_ , ())
  a {succ sz} (acc f) cc mm nn with cc | mm | nn
  ... | b | m O , s<s m< | n O , s<s n< = a+O (f sz n<n1) b (m , m<) (n , n<)
  ... | b | m O , s<s m< | n I , s<s n< = a+I (f sz n<n1) b (m , m<) (n , n<)
   ....-- not including the whole thing here - it is too long.

I am not including the whole construction of addition of two binary numbers (also not an efficient one - just an exercise in proving well-foundedness). The important thing to note here is how the recursion is kicked off, and how it is reused to construct new instances of Acc for matching types - here S-Bin represents a binary number of bit length at most n, and Agda is convinced that Acc _<_ n gets smaller, even though it can't prove S-Bin n gets smaller.