Coq не может вычислить обоснованную функцию на Z, но она работает на nat

Question

Я пишу (для себя) объяснение того, как сделать обоснованную рекурсию в Coq. (см., например, книгу Coq'Art, глава 15.2). Сначала я сделал пример функции на основе nat и это работало нормально, но потом я сделал это снова для Zи когда я использую Compute чтобы оценить это, это не сводит весь путь к Z значение. Зачем?

Вот мой пример (я поместил текст внутри комментариев, чтобы можно было скопировать и вставить все это в ваш редактор):

---

(* Тест обоснованной рекурсии *)

(* TL; DR: чтобы сделать обоснованную рекурсию, сначала создайте "функционал", а затем создайте рекурсивную функцию, используя Acc_iter, итератор для доступных отношений *)

(* В качестве примера, вычислите сумму ряда от 1 до n, примерно так:

исправить f n:= (если n = 0, то 0, иначе n + f (n-1))

Теперь давайте не будем использовать структурную рекурсию для n.

Вместо этого мы используем обоснованную рекурсию по n, используя то, что отношение меньше чем ('lt') корректно. Функция f завершается, потому что рекурсивный вызов выполняется на структурно меньшем члене (в убывающей Acc-цепочке). *)

(* Сначала мы делаем это для nat *)

Require Import Arith.Arith.
Require Import Program.Utils. (* for 'dec' *)
Require Import Wellfounded.

(* Из доказательства того, что отношение является вполне обоснованным, мы можем получить доказательство того, что определенный элемент в его области доступен.

Команды проверки здесь не нужны, просто для документации, уважаемый читатель. *)

Check well_founded : forall A : Type, (A -> A -> Prop) -> Prop.
Check lt_wf : well_founded lt.
Check (lt_wf 4711 : Acc lt 4711).

(* Сначала определите "функциональный" F для f. Это функция, которая принимает функцию F_rec для "рекурсивного вызова" в качестве аргумента. Поскольку нам нужно знать n <> 0 во второй ветви, мы используем "dec" для превратить булево условие if в sumbool, и мы получим информацию об этом в ветвях.

Мы пишем большую часть этого с уточнением, и оставляем некоторые дыры, которые будут заполнены тактикой позже. *)

Definition F (n:nat) (F_rec : (forall y : nat, y < n -> nat)): nat.
  refine ( if dec (n =? 0) then 0 else n + (F_rec (n-1) _ ) ).

  (* now we need to show that n-1 < n, which is true for nat if n<>0 *)
  destruct n; now auto with *.
Defined.

(* Функционал может использоваться итератором для вызова f столько раз, сколько необходимо.

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

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

(* Тип Acc_iter довольно волосатый *)

Check Acc_iter :
      forall (A : Type) (R : A -> A -> Prop) (P : A -> Type),
       (forall x : A, (forall y : A, R y x -> P y) -> P x) -> forall x : A, Acc R x -> P x.

(* P есть, потому что тип возвращаемого значения может зависеть от аргумента,
но в нашем случае f:nat->nat и R = lt, поэтому мы имеем *)

Check Acc_iter (R:=lt) (fun _:nat=>nat) :
  (forall n : nat, (forall y : nat, y < n -> nat) -> nat) ->
   forall n : nat, Acc lt n -> nat.

(* Здесь первый аргумент - это функционал, который принимает итератор, второй аргумент n - это ввод для f, а третий аргумент является доказательством доступности n. Итератор возвращает значение f, примененное к n.

Некоторые из аргументов Acc_iter являются неявными, а некоторые могут быть выведены. Таким образом, мы можем определить f просто следующим образом: *)

Definition f n := Acc_iter _ F (lt_wf n).

(* Отлично работает *)

Compute (f 50). (* This prints 1275 *)
Check eq_refl : f 50 = 1275.

(* Теперь давайте сделаем это для Z. Здесь мы не можем использовать lt или lt_wf, потому что они для nat. Для Z мы можем использовать Zle и (Zwf c), который принимает нижнюю границу. Для нее нужна нижняя граница, под которой мы знать, что функция всегда завершается, чтобы гарантировать завершение. Здесь мы используем (Zwf 0), чтобы сказать, что наша функция всегда будет заканчиваться на уровне или ниже 0. Мы также должны изменить оператор if на 'if n <= 0, то 0 else ...'поэтому мы возвращаем ноль для аргументов меньше нуля. *)

Require Import ZArith.
Require Import Zwf.

Open Scope Z.

(* Теперь мы определим функцию g на основе функционала G *)

Definition G (n:Z) (G_rec :  (forall y : Z, Zwf 0 y n -> Z)) : Z.
  refine (if dec (n<?0) then 0 else n + (G_rec (n-1) _ )).

  (* now we need to show that n-1 < n *)
  now split; [ apply Z.ltb_ge | apply Z.lt_sub_pos].
Defined.

Definition g n := Acc_iter _ G (Zwf_well_founded 0 n).

(* Но теперь мы не можем вычислить! *)

Compute (g 1).

(* Мы просто получаем огромный термин, начинающийся с

     = (fix
        Ffix (x : Z)
             (x0 : Acc
                     (fun x0 x1 : Z =>
                      (match x1 with
                       | 0 => Eq
                       | Z.pos _ => Lt
                       | Z.neg _ => Gt
                       end = Gt -> False) /\
                      match x0 with
                      | 0 => match x1 with
                             | 0 => Eq
                             | Z.pos _ => Lt
                             | Z.neg _ => Gt
                             end
                      | Z.pos x2 =>

    ...

 end) 1 (Zwf_well_founded 0 1)
     : (fun _ : Z => Z) 1
   ) 

---

Комментарий: я заметил, что Zwf_well_founded определяется как Opaque в библиотеке, поэтому я попытался сделать это Transparent скопировав доказательство и закончив лемму Defined. вместо Qed. но это не помогло...

Добавлено наблюдение:

Если я определю f' за nat с Fixpoint вместо этого, и запишите на доказательство доступности, и закончите сDefined. тогда это вычисляет. Но если я закончу Qed. это не уменьшает. Это связано? Я думаю, что есть проблема прозрачности в определении G или же g где-то... или я полностью ошибаюсь?

Fixpoint f' (n:nat) (H: Acc lt n) : nat.
  refine (if dec (n<=?0) then 0 else n + (f' (n-1) (Acc_inv H _))).
  apply Nat.leb_gt in e.
  apply Nat.sub_lt; auto with *.
Defined.  (* Compute (f' 10 (lt_wf 10)). doesn't evaluate to a nat if ended with Qed. *)

Во всяком случае, моя проблема сохраняется для Z,

Fixpoint g' (n:Z) (H: Acc (Zwf 0) n) : Z.
  refine (if dec (n<=?0) then 0 else n + (g' (n-1) (Acc_inv H _))).
  split; now apply Z.leb_gt in e; auto with *.
Defined.

Compute (g' 10 (Zwf_well_founded 0 10)).

Answer 1

Изготовление Zwf_well_founded Прозрачность не поможет, потому что она определена в стандартной библиотеке:

Lemma Zwf_well_founded : well_founded (Zwf c).
...
    case (Z.le_gt_cases c y); intro; auto with zarith.
...
Qed.

Если вы замените строку в приведенном выше доказательстве на

     case (Z_le_gt_dec c y); intro; auto with zarith.

и заменить Qed. с Defined. (что вы уже сделали) все должно работать. Это связано с тем, что исходное доказательство зависит от логического термина, и это мешает оценщику выполнить сопоставление с образцом, потому что логическая сущность Z.le_gt_cases непрозрачен, в то время как вычислительная сущность Z_le_gt_dec прозрачный См. Использование механизмов оценки Coq в блоге гнева Ксавье Леруа. Вы также можете найти полезное сообщение от Gedory Malecha.

Вместо того, чтобы изменить доказательство Zwf_well_founded Вы можете использовать повторно Zlt_0_rec вот так:

Require Import Coq.ZArith.ZArith.

Open Scope Z.

Definition H (x:Z) (H_rec : (forall y : Z, 0 <= y < x -> Z)) (nonneg : 0 <= x) : Z.
  refine (if Z_zerop x then 0 else x + (H_rec (Z.pred x) _ )).
  auto with zarith.
Defined.

Definition h (z : Z) : Z :=
  match Z_lt_le_dec z 0 with left _ => 0 | right pf => (Zlt_0_rec _ H z pf) end.

Check eq_refl : h 100 = 5050.

Это немного менее удобно, потому что теперь мы имеем дело с отрицательными числами в h,