Блог

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

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

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

 Require Import Program Omega.

Inductive tuple_lt : (nat * nat) -> (nat * nat) -> Prop :=
  fst_lt : forall a b c d, a < c -> tuple_lt (a, b) (c, d).

Program Fixpoint f (a : nat) (b : nat) {measure (a, b) (tuple_lt)} :=
match a with
| 0 => 0
| S n => f n b
end.

Next Obligation.
apply fst_lt. auto.
Qed.

Next Obligation.
unfold well_founded. unfold MR.
 

Обязательство выглядит следующим образом:

 forall a : {_ : nat amp; nat}, Acc (fun x y : {_ : nat amp; nat} => tuple_lt (projT1 x, projT2 x) (projT1 y, projT2 y)) a
 

Могу ли я каким-то образом преобразовать доказательство Acc tuple_lt в это уродливое доказательство или избежать его генерации?

Есть ли в стандартной библиотеке доказательство для структурной рекурсии по двум аргументам?

Как мне вообще написать ручное доказательство WF с использованием уравнений? В руководстве это не упоминается.

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

Чтобы разобраться с MR этим, вы можете использовать лемму measure_wf в Program.Wf .

Чтобы доказать обоснованность tuple_lt , вы можете полагаться на леммы, показывающие обоснованность отношения, основанного на обоснованности другого отношения. Здесь мы можем использовать well_founded_lt_compat . В других случаях могут оказаться полезными другие леммы, такие как wf_inverse_image , well_founded_ltof или well_founded_gtof .

Доказательство обоснованности tuple_lt становится простым.

 Lemma tuple_lt_wf : well_founded tuple_lt.
Proof.
  apply well_founded_lt_compat with fst.
  intros ? ? []; assumption.
Defined.
 

То же самое относится и к доказательству второго обязательства.

 Next Obligation.
apply measure_wf. apply tuple_lt_wf.
Defined.
 

(Обратите внимание, что в обоих случаях вы должны заканчивать доказательства с Defined помощью вместо Qed , если вы хотите, чтобы ваша функция, определенная с помощью Program Fixpoint , вычислялась внутри Coq (в противном случае она застревает на непрозрачных доказательствах); кажется, вы можете закончить доказательство первого обязательства с Qed помощью , хотя).

Вы также можете использовать следующее более простое определение для tuple_lt :

 Definition tuple_lt (p1 p2 : nat * nat) := fst p1 < fst p2.
 

В этом случае доказательство обоснованности тривиально.

 Lemma tuple_lt_wf : well_founded tuple_lt.
Proof.
  apply well_founded_ltof.
Defined.