Как определить функцию индуктивно по двум аргументам в Coq?

Как я могу убедить Coq, что приведенная ниже рекурсивная функция завершается? Функция принимает два индуктивных аргумента. Интуитивно понятно, что рекурсия завершается, потому что любой аргумент разлагается.

В частности, функция принимает два дерева в качестве входных данных.

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

На деревьях мне нравится делать следующий стиль индукции.

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.

Определение TreePair принято, но определение пары функций выдает сообщение об ошибке:

Error: Cannot guess decreasing argument of fix.

Поэтому меня интересует, как убедить Coq в расторжении.

Определения фиксированной точки Coq требуют, чтобы индуктивные вызовы получали структурно меньший аргумент. В глубине души конструкция с фиксированной точкой принимает один аргумент: нет встроенной концепции рекурсивного определения для двух аргументов. К счастью, определение Coq структурно меньшего размера включает типы высшего порядка, что является чрезвычайно мощным.

Ваше определение точки фиксации с двумя аргументами следует простому шаблону: либо первый аргумент становится меньше, либо первый аргумент остается идентичным, а второй аргумент становится меньше. Этот довольно распространенный шаблон может быть обработан простым исправлением.

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.

Для более сложных случаев, или если ваши вкусы работают таким образом, вы можете использовать рекурсию ближе к тому, как она преподается на курсах по математике, создавая точку фиксации из пошагового вычисления и отдельного аргумента обоснованности , часто используя целочисленную меру . Вы также можете сделать свое определение более похожим на классическую программу на не тотальном языке с отдельным окончанием на Programместном языке .