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.