Вычислить с рекурсивной функцией, определенной четко определенной индукцией

Question

Когда я использую Function чтобы определить неструктурно-рекурсивную функцию в Coq, результирующий объект ведет себя странно, когда запрашивается конкретное вычисление. На самом деле, вместо того, чтобы давать непосредственно результат, Eval compute in ... директива возвращает довольно длинное (обычно 170 000 строк) выражение. Кажется, что Coq не может оценить все и поэтому возвращает упрощенное (но длинное) выражение вместо просто значения.

Кажется, проблема возникает из-за того, что я доказываю обязательства, Function, Сначала я подумал, что проблема возникла из-за непрозрачных терминов, которые я использовал, и я преобразовал все леммы в прозрачные константы. Кстати, есть ли способ перечислить непрозрачные термины, появляющиеся в термине? Или любой другой способ превратить непрозрачные леммы в прозрачные?

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

Например, я определяю log2 на натуральные числа путем многократного применения div2, Вот определение:

Function log2 n {wf lt n} :=
  match n with
  | 0 => 0
  | 1 => 0
  | n => S (log2 (Nat.div2 n))
  end.

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

forall n n0 n1 : nat, n0 = S n1 -> n = S (S n1) -> Nat.div2 (S (S n1)) < S (S n1)

intros. apply Nat.lt_div2. apply le_n_S. apply le_0_n.

Второй проверяет, что lt это обоснованный заказ. Это уже доказано в стандартной библиотеке. Соответствующая лемма Coq.Arith.Wf_nat.lt_wf,

Если я использую это доказательство, результирующая функция ведет себя нормально. Eval compute in log24 10. возвращается 3,

Но если я хочу сделать доказательство самостоятельно, я не всегда получаю такое поведение. Во-первых, если я закончу доказательство Qed вместо Definedрезультат вычисления (даже для небольших чисел) является сложным выражением, а не одним числом. Поэтому я использую Defined и попробуйте использовать только прозрачные леммы.

Lemma lt_wf2 : well_founded lt.
Proof.
  unfold well_founded. intros n.
  apply (lemma1 n). clear n.
  intros. constructor. apply H.
Defined.

Здесь лемма 1 является доказательством обоснованной индукции на натуральные числа. Здесь я снова могу использовать уже существующие леммы, такие как lt_wf_ind, lt_wf_rec, lt_wf_rec1 находится в Coq.Arith.Wf_nat, или даже well_founded_ind lt_wf, Первый не работает, кажется, это потому, что он непрозрачный. Три других работают.

Я пытался доказать это напрямую, используя стандартную индукцию по натуральным числам, nat_ind, Это дает:

Lemma lemma1 : forall n (P:nat -> Prop),
  (forall n, (forall p, p < n -> P p) -> P n) -> P n.
Proof.
  intros n P H. pose proof (nat_ind (fun n => forall p, p < n -> P p)).
  simpl in H0. apply H0 with (n:=S n).
  - intros. inversion H1.
  - intros. inversion H2.
    + apply H. exact H1.
    + apply H1. assumption.
  - apply le_n.
Defined.

С этим доказательством (и некоторыми его вариантами), log2 имеет такое же странное поведение. И в этом доказательстве используются только прозрачные объекты, поэтому, возможно, проблема не в этом.

Как я могу определить Function что возвращает понятные результаты по конкретным значениям?

Answer 1

Мне удалось определить место, которое вызывает проблемы: это inversion H2. в lemma1, Оказывается, нам не нужен этот анализ случая и intuition может закончить доказательство (это не соответствует шаблону на H2):

Lemma lemma1 : forall n (P:nat -> Prop),
  (forall n, (forall p, p < n -> P p) -> P n) -> P n.
Proof.
  intros n P H. pose proof (nat_ind (fun n => forall p, p < n -> P p)).
  simpl in H0. apply H0 with (n:=S n).
  - intros. inversion H1.
  - intros. intuition.
  - apply le_n.
Defined.

Если мы используем lemma1 с этим доказательством, вычисление log2 10 результаты в 3,

Кстати, вот моя версия lt_wf2 (это также позволяет нам вычислять):

Lemma lt_wf2 : well_founded lt.
Proof.
  unfold well_founded; intros n.
  induction n; constructor; intros k Hk.
  - inversion Hk.
  - constructor; intros m Hm.
    apply IHn; omega.
 (* OR: apply IHn, Nat.lt_le_trans with (m := k); auto with arith. *)
Defined.

Я полагаю, что механизмы оценки использования Coq в блоге гнева Ксавье Леруа объясняют такое поведение.

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

В нашем случае мы исключаем доказательство неравенства (inversion H2.) в доказательство lemma1 и Function Механизм делает наши вычисления зависимыми от доказательного члена. Следовательно, оценщик не может продолжить, когда n > 1.

И причина inversion H1. в теле леммы не влияет на вычисления, что для n = 0 а также n = 1, log2 n определяется в рамках match выражение как базовые случаи.

Чтобы проиллюстрировать этот момент, позвольте мне показать пример, когда мы можем предотвратить оценку log2 n на любые значения n а также n + 1 по нашему выбору, где n > 1 и больше нигде!

Lemma lt_wf2' : well_founded lt.
Proof.
  unfold well_founded; intros n.
  induction n; constructor; intros k Hk.
  - inversion Hk.          (* n = 0 *)
  - destruct n. intuition. (* n = 1 *)
    destruct n. intuition. (* n = 2 *)
    destruct n. intuition. (* n = 3 *)
    destruct n. inversion Hk; intuition. (* n = 4 and n = 5 - won't evaluate *)
    (* n > 5 *)
    constructor; intros m Hm; apply IHn; omega.
Defined.

Если вы используете эту модифицированную лемму в определении log2 вы увидите, что он вычисляет везде, кроме n = 4 а также n = 5, Ну почти везде - расчеты с большими nat s может привести к переполнению стека или ошибке сегментации, поскольку Coq предупреждает нас:

Предупреждение: переполнение стека или ошибка сегментации происходит при работе с большими числами в nat (наблюдаемый порог может варьироваться от 5000 до 70000 в зависимости от ограничений вашей системы и от выполняемой команды).

И сделать log2 работать на n = 4 а также n = 5 даже для приведенных выше "ошибочных" доказательств мы могли бы изменить log2 как это

Function log2 n {wf lt n} :=
  match n with
  | 0 => 0
  | 1 => 0
  | 4 => 2
  | 5 => 2
  | n => S (log2 (Nat.div2 n))
  end.

добавив необходимые доказательства в конце.

---

"Обоснованное" доказательство должно быть прозрачным и не может полагаться на сопоставление с образцом на объектах доказательства, потому что Function Механизм на самом деле использует lt_wf лемма, чтобы вычислить убывающую охрану завершения. Если мы посмотрим на термин, производимый Eval (в случае, когда оценка не дает nat), мы увидим что-то вроде этого:

fix Ffix (x : nat) (x0 : Acc (fun x0 x1 : nat => S x0 <= x1) x) {struct x0}

Это легко увидеть x0 : Prop то есть стирается при извлечении функциональной программы log2 в, скажем, OCaml, но внутренний механизм оценки Coq должен использовать его для обеспечения завершения.

Answer 2

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

Легче полагаться на собственные тактики и леммы для сокращения функций, определенных таким образом. Во-первых, я бы порекомендовал Program Fixpoint над Functionпотому что последний намного старше и (я думаю) менее ухоженный. Таким образом, вы получите такое определение:

Require Import Coq.Numbers.Natural.Peano.NPeano.
Require Import Coq.Program.Wf.
Require Import Coq.Program.Tactics.

Program Fixpoint log2 n {wf lt n} :=
  match n with
  | 0 => 0
  | 1 => 0
  | n => S (log2 (Nat.div2 n))
  end.

Next Obligation.
admit.
Qed.

Теперь вам просто нужно использовать program_simpl тактика упрощения звонков log2, Вот пример:

Lemma foo : log2 4 = 2.
Proof.
  program_simpl.
Qed.