Не могу определить завершение

Question

Функция для определения, является ли набор подмножеством другого:

Fixpoint subset (s1:bag) (s2:bag) : bool :=
  match s1 with
  | nil => true
  | h :: t => match (beq_nat (count h s1) (count h s2)) with
    | true => subset (remove_all h t) (remove_all h s2)
    | false => false
    end
  end.

Для ясности

• beq_nat определяет равенство двух натуральных чисел
• count подсчитывает, сколько раз данное натуральное число встречается в наборе
• remove_all удаляет каждый экземпляр данного натурального числа из набора

CoqIDE "Не могу угадать уменьшающийся аргумент исправления." Учитывая, что рекурсия выполняется на подмножестве t (хвост s1) почему это не гарантировано прекратить?

Примечание. Эта проблема возникла на этом веб-сайте, авторы которого просят не публиковать решения. Более того, я уже выполнил это упражнение, поэтому решение нежелательно. Объяснение почему coq не могу определить прекращение будет высоко ценится.

Answer 1

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

Вот пример:

Fixpoint plus (n m : nat) : nat :=
  match n with
  | O => m
  | S p => S (plus p m)
  end.

Объяснение для принятия заключается в том, что p является аргументом в ранге 1, он получается как переменная сопоставления с образцом из n, который является начальным аргументом в ранге 1. Таким образом, функция является структурно рекурсивной, убывающей по первому аргументу. Всегда должен быть аргумент, который уменьшается. Совместное уменьшение между несколькими аргументами не принимается.

Вам следует прекратить читать здесь, если вы не хотите, чтобы вас тонули в деталях.

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

Require Import List Arith.

Fixpoint awk1 (l : list nat) :=
  match l with
  | a :: ((b :: l'') as l') => 
    b :: awk1 (if Nat.even a then l' else l'')
  | _ => l
  end.

Так в функции awk1 рекурсивный вызов не для переменной, а для выражения сопоставления с образцом, но это нормально, потому что все возможные значения этого рекурсивного вызова действительно являются переменными, полученными посредством сопоставления с образцом. Это также показывает, насколько разборчивым может быть проверка завершения, потому что выражение (if Nat.even a then (b :: l'') else l'') не будет принято: (b :: l'') не является переменной

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

Definition arg n (l : list nat) :=
  if Nat.even n then
    l 
  else
    match l with _ :: l' => l' | _ => l end.

Fixpoint awk2 (l : list nat) :=
match l with
  a :: l' => a :: awk2 (arg a l')
| _ => l
end.

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

Fixpoint mydiv (n : nat) (m : nat) :=
   match n, m with
     S n', S m' => S (mydiv (Nat.sub n' m') m)
   | _, _ => n
   end.

Если вы распечатаете определение Nat.sub вы увидите, что он тщательно продуман, чтобы всегда возвращать либо результат рекурсивного вызова, либо первого ввода, и, кроме того, в рекурсивных вызовах первый аргумент действительно является переменной, полученной путем сопоставления с шаблоном из первого ввода. Этот вид убывающего свойства признается.

Answer 2

Ваш аргумент завершения корректен, но Coq не достаточно умен, чтобы понять это сам. Грубо говоря, Coq принимает только рекурсивные вызовы, выполняемые на синтаксических подтермах своего основного аргумента. Это очень ограничительное понятие: например, [1; 3] это подсписок [0; 1; 2; 3], но не синтаксическая субтерма.

Если вы хотите, чтобы Coq принял это, вам, вероятно, нужно переписать вашу функцию, используя обоснованную рекурсию. В книге Адама Чипала CPDT есть хорошая глава по этому вопросу.