Coq не может вычислить обоснованные, определенные с помощью Fix, но может, если определено с помощью программы Fixpoint

Question

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

Расширенный евклидов алгоритм работает с целыми числами, поэтому мне нужны некоторые обоснованные отношения с целыми числами. Я пытался использовать отношения в Zwf, но все не работает (мне нужно увидеть больше примеров). Я решил, что будет проще сопоставить Z в nat с Z.abs_nat функция, а затем просто использовать Nat.lt как отношение. Наш друг wf_inverse_image приходит мне на помощь Итак, вот что я сделал:

Require Import ZArith Coq.ZArith.Znumtheory.
Require Import Wellfounded.

Definition fabs := (fun x => Z.abs_nat (Z.abs x)). (* (Z.abs x) is a involutive nice guy to help me in the future *) 
Definition myR (x y : Z) := (fabs x < fabs y)%nat.
Definition lt_wf_on_Z := (wf_inverse_image Z nat lt fabs) lt_wf.

Расширенный евклидов алгоритм работает так:

Definition euclids_type (a : Z) := forall b : Z, Z * Z * Z.

Definition euclids_rec : (forall x : Z, (forall y : Z,(myR y x) -> euclids_type y) -> euclids_type x).
  unfold myR, fabs.
  refine (fun a rec b => if (Z_eq_dec a 0) then (b, 0, 1)
                      else let '(g, s, t) :=  rec (b mod a ) _ a 
                           in (g, t - (b / a) * s, s)
                      ).
apply Zabs_nat_lt. split. apply Z.abs_nonneg. apply Z.mod_bound_abs. assumption.
Defined.

Definition euclids := Fix lt_wf_on_Z _ euclids_rec. 

Теперь посмотрим, работает ли это:

Compute (euclids 240 46). (* Computation takes a long time and results in a huge term *)

Я знаю, что это может произойти, если какое-то определение непрозрачно, однако все мои определения заканчиваются на Defined., Окей, что-то еще непрозрачно, но что? Если это определение библиотеки, то я не думаю, что было бы здорово просто переопределить его в моем коде.

Кажется, моя проблема связана с этим, с этим другим и с этим тоже.

Я решил дать Program Fixpoint попытка, так как я никогда не использовал это. Я был удивлен, увидев, что я могу просто скопировать и вставить мою программу.

Program Fixpoint euclids' (a b: Z) {measure (Z.abs_nat (Z.abs a))} : Z * Z * Z :=
  if Z.eq_dec a 0 then (b, 0, 1)
  else let '(g, s, t) := euclids' (b mod a) a in
       (g, t - (b / a) * s, s).
Next Obligation.
apply Zabs_nat_lt. split. apply Z.abs_nonneg. apply Z.mod_bound_abs. assumption. 
Defined.

И еще больше удивляет то, что это прекрасно работает:

Compute (euclids' 240 46). (* fast computation gives me (2, -9, 47): Z * Z * Z *)

Что непрозрачно в euclids это не в euclids'? И как сделать euclids Работа?

Answer 1

Окей, что-то еще непрозрачно, но что?

wf_inverse_image непрозрачен, как и леммы, на которые он опирается: Acc_lemma а также Acc_inverse_image, Если вы сделаете эти три прозрачными euclids будет вычислять.

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

И как сделать euclids Работа?

К счастью, вам не нужно накатывать свои собственные прозрачные версии вышеупомянутых стандартных определений, так как well_founded_ltof лемма в Coq.Arith.Wf_nat который уже прозрачен, поэтому мы можем использовать его снова:

Lemma lt_wf_on_Z : well_founded myR.
Proof. exact (well_founded_ltof Z fabs). Defined.

Это оно! После исправления lt_wf_on_Z остальная часть вашего кода просто работает.