Jak zdefiniować funkcję indukcyjnie na podstawie dwóch argumentów w Coq?

Jak przekonać Coq, że podana poniżej funkcja rekurencyjna kończy się? Funkcja przyjmuje dwa argumenty indukcyjne. Intuicyjnie rekursja kończy się, ponieważ którykolwiek argument jest rozkładany.

W szczególności funkcja przyjmuje dwa drzewa jako dane wejściowe.

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

Na drzewach lubię stosować następujący styl indukcji.

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.

Definicja TreePair jest akceptowana, ale definicja pary funkcji zwraca komunikat o błędzie:

Error: Cannot guess decreasing argument of fix.

Jestem więc zainteresowany tym, jak przekonać Coq o wypowiedzeniu.

Definicje punktów Coq wymagają, aby wywołania indukcyjne otrzymywały strukturalnie mniejszy argument. Głęboko w konstrukcji punktu stałego bierze się jeden argument: nie ma wbudowanej koncepcji definicji rekurencyjnej na podstawie dwóch argumentów. Na szczęście definicja Coq strukturalnie mniejsza obejmuje typy wyższego rzędu, co jest niezwykle potężne.

Definicja punktu stałego z dwoma argumentami jest prosta: albo pierwszy argument staje się mniejszy, albo pierwszy argument pozostaje identyczny, a drugi argument staje się mniejszy. Ten dość powszechny wzorzec można rozwiązać za pomocą prostej poprawki.

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.

W przypadku bardziej skomplikowanych przypadków lub jeśli twoje poglądy przebiegają w ten sposób, możesz użyć rekurencji bliżej sposobu nauczania na kursach matematycznych, budując punkt stały z obliczeń kroków i osobnego uzasadnionego argumentu , często stosując miarę całkowitą . Możesz także sprawić, by twoja definicja wyglądała bardziej jak klasyczny program w języku niecałkowitym z oddzielnym zakończeniem za pomocą Programjęzyka ojczystego .