Структурная рекурсия по двум аргументам - PullRequest
Новая
       12

Структурная рекурсия по двум аргументам

1 голос
/ 16 апреля 2019

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

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

Вероятно, я мог бы выполнить обоснованную рекурсию вручную, но я бы хотел использовать программную точку фиксации или уравнения. С программой 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 & nat}, Acc (fun x y : {_ : nat & nat} => tuple_lt (projT1 x, projT2 x) (projT1 y, projT2 y)) a

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

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

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

1 Ответ

3 голосов
/ 16 апреля 2019

В таких простых случаях, как этот, вам не нужно раскрывать определения, такие как 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.
...