How to define a function inductively on two arguments in Coq?

Question

How can I convince Coq that the recursive function given below terminates? The function takes two inductive arguments. Intuitively, the recursion terminates because either argument is decomposed.

Specifically, the function takes two trees as input.

Inductive Tree :=
| Tip: Tree
| Bin: Tree -> Tree -> Tree.

On Trees, I like to do the following style of induction.

Inductive TreePair :=
| TipTip : TreePair
| TipBin : Tree -> Tree -> TreePair
| BinTip : Tree -> Tree -> TreePair
| BinBin : TreePair -> TreePair -> TreePair.

Fixpoint pair (l r: Tree): TreePair :=
  match l with
    | Tip =>
      match r with
        | Tip => TipTip
        | Bin rl rr => TipBin rl rr
      end
    | Bin ll lr =>
      match r with
        | Tip => BinTip ll lr
        | Bin rl rr => BinBin (pair l rl) (pair lr r)
      end
  end.

The definition of TreePair is accepted, but the definition of the function pair yields the error message:

Error: Cannot guess decreasing argument of fix.

So I am interested in how to convince Coq of the termination.

Answer 1

Coq's fixpoint definitions require that inductive calls receive a structurally smaller argument. Deep down, a fixpoint construct takes a single argument: there's no built-in concept of a recursive definition over two arguments. Fortunately, Coq's definition of structurally smaller includes higher-order types, which is extremely powerful.

Your two-argument fixpoint definition follows a simple pattern: either the first argument becomes smaller, or the first argument remains identical and the second argument becomes smaller. This fairly common pattern can be handled by a simple fix-in-fix.

Fixpoint pair l := fix pair1 (r : Tree) :=
  match l with
    | Tip => match r with
              | Tip => TipTip
              | Bin rl rr => TipBin rl rr
            end
    | Bin ll lr => match r with
                    | Tip => BinTip ll lr
                    | Bin rl rr => BinBin (pair1 rl) (pair lr r)
                   end
  end.

For more complex cases, or if your tastes run that way, you can use recursion closer to the way it's taught in math courses, building the fixpoint from a step computation and a separate well-foundedness argument, often using an integer measure. You can also make your definition look more like a classical program in a non-total language with a separate termination using the Program vernacular.