Strictly-monotone "max" operation for constructive Brouwer-trees?

Question

The Setting

I'm trying to use Agda's well-founded ordering to prove that something is terminating using Brouwer Trees i.e.

data Ord where
  zero : Ord
  succ : Ord -> Ord
  limit : (Nat -> Ord) -> Ord

We can define a well-founded ordering like so:

data _≤_ where
    ≤-zero      : ∀ {x} → zero ≤ x
    ≤-succ-mono : ∀ {x y} → x ≤ y → succ x ≤ succ y
    ≤-cocone    : ∀ {x} f { k} → (x ≤ f k) → (x ≤ limit f )
    ≤-limiting  : ∀ f {x} → ((k : ℕ) → f k ≤ x) → limit f  ≤ x

And then define x < y to be succ x ≤ y.

The Problem

The issue is that I'm trying to show termination for mutually recursive functions. One has one argument, but the other has two arguments, and is "symmetric" i.e. there isn't one "dominant" argument that is decreasing. So I can't use a lexicographic ordering. The 2-arg function sometimes calls the 1-arg function when one of arguments is size 1, and the 1-arg function sometimes calls the 2-arg function with two arguments strictly smaller than its argument.

What I'm really trying to show is that the "maximum" of the two sizes is decreasing. We can define:

max x y = limit (\ n -> if n == 0 then x else y)

which does in fact compute a least upper bound on x and y for ≤.

But, this function is not strictly monotone, i.e., there's no way to conclude that max a b < max c d from a < c and b < d. And we need it to be strictly monotone to show that recursive calls are being made with the arguments strictly decreasing.

The reason we can't show this is that there's no way to show that succ (lim f) ≤ lim (\n -> succ (f n)).

My question

Is there some kind of well-founded relation that avoids this issue?

• Can the definition of < and ≤ be altered while keeping it well-founded, without having to reach to things like HITs?
• Is there a different function that can be used instead of max? For example, I can imagine showing that the sum of the two ordinals is decreasing. But (I think) you run into the same issues with showing that + is strictly monotone.
• Is there different notion of ordinal, or some other well-founded relation, that doesn't suffer from this issue for max?

Answer 1

You can define a max that will be better behaved by induction on x and y. Something like:

max : Ord → Ord → Ord
max zero y = y
max x zero = x
max (lim f) y = lim (λ k → max (f k) y)
max x (lim f) = lim (λ k → max x (f k))
max (suc x) (suc y) = suc (max x y)

I didn't work all the way through your desired property, but I'm pretty confident it's possible (just a lot of cases).

However, actually doing it that way might be more work than figuring out a better way to characterize the termination of your functions. For instance, if $R$ and $S$ are both well-founded relations, then the relation $R \oplus S$ on pairs given by:

data _⊕_ (R : A → A → Set) (S : B → B → Set) : (p q : A × B) → Set where
  left : R x y → (R ⊕ S) (x , z) (y , z)
  right : S y z → (R ⊕ S) (x , y) (x , z)

is also well-founded. Proving that is less work than working out the facts about max on Ord, so it'd be easier if it works for you.

P.S. To answer ionchy's comment, the reason this would be expected to work is that the $f$ used is not a strictly increasing/unbounded function. It's representing the supremum of a 2 element set. The problem with proving that it actually behaves like the maximum using the available methods is that you have to give an index $k$ up front that picks either $\mathsf{suc}\ x$ or $\mathsf{suc}\ y$ to be greater than $\mathsf{suc}(\mathsf{max}\ x\ y)$, meaning you need to pick the bigger of the two. Most set theorists will probably tell you to just use excluded middle to do this.

If it were possible to directly define strict inequality so that an index could be given for the left side first, that might work (constructively) for the original max definition. But I'm not certain if this can be done.