Почему средство проверки завершения Coq не поддерживает случай, когда один аргумент структурно уменьшается, а другие остаются неизменными

Question

Средство проверки завершения Coq не любит такие функции, как:

Fixpoint interleave (A : Type) (l1 l2 : list A) : list A :=
  match l1 with 
  | cons h1 t1 => cons h1 (interleave l2 t1)
  | nil => l2
  end.

Однако некоторые другие языки с похожими контролерами завершения, такие как Lean, Idris и Isabelle, принимают такие функции. Мне интересно, почему средство проверки завершения Coq не будет принимать такие функции, когда хотя бы один аргумент структурно уменьшается каждый раз, а аргументы не увеличиваются. Мне кажется, что если хотя бы один аргумент всегда становится меньше, а ни один не увеличивается, функция должна в конечном итоге завершиться, или я пропускаю какой-то случай?

Редактировать: Кажется, я выбрал ужасный пример здесь, поскольку, очевидно, Идрис и Лин не могут справиться с этим. Лучшим примером была бы формулировка "исправление в исправлении", приведенная в разделе Как работать с действительно большими терминами, сгенерированными программой Fixpoint в Coq? ; Я знаю, что мне удалось реализовать ту же самую функцию непосредственно в Lean и Idris, не требуя создания исправлений. Кроме того, первоначальный вопрос остается в силе: почему эта конструкция не поддерживается?

Answer 1

Как Галле предлагает, вы можете использовать measure:

Require Import PeanoNat.
Require Import Coq.Program.Wf.

Program Fixpoint interleave (A : Type) (l1 l2 : list A) {measure (length l1 + length l2)} : list A :=
  match l1 with
  | nil => l2
  | cons h1 t1 => cons h1 (interleave A l2 t1)
  end.
Next Obligation.
  simpl.
  rewrite Nat.add_comm.
  apply Nat.lt_succ_diag_r.
Defined.
Next Obligation.
Admitted.

После определения нужно доказать две вещи: во-первых, что на каждом шаге мера уменьшается; и во-вторых, эта мера обоснована. После завершения двух доказательств ваше определение готово.