The Coq mailing list

[Xavier Leroy <xavier.leroy AT college-de-france.fr>]

On Sun, Oct 3, 2021 at 10:30 AM mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> wrote:

What is the difference between the  poslt_wf in wf_proof and the poslt_wf  in wf_not_reducing?

I don't know.  But, generally speaking, it is difficult to write accessibility proofs that compute efficiently (or even compute at all).  You'd better use Krebbers' trick: https://sympa.inria.fr/sympa/arc/coq-club/2013-09/msg00034.html.

- Xavier Leroy

More context: I have a function bgcd [1] that uses the poslt_wf [2, 3], from the wf_not_reducing. When I evaluate the bgcd [1] on some input --Time Eval compute in bgcd 2 3 2 3 1 1 0 0 1. [4]-- I get heaps of text (no concrete value), but if I replace poslt_wf [2, 3] by poslt_wf, from the wf_proof (in the Coq code, replace poslt_wf by Reducing.poslt_wf),  bgcd [1] works fine and produces concrete value. Therefore, my question is: what is the difference between these two poslt_wf? (in both cases, About poslt_wf produces:  poslt_wf is not universe polymorphic, poslt_wf is transparent. However, if both are transparent then why one reduces and other does not?)

Best,

Mukesh

Section wf_proof.

  Let f (c : Z) (a : Z) := Z.abs_nat (a - c).

  Definition zwf (c : Z) (x y : Z) := (f c x < f c y)%nat.

  Lemma zwf_well_founded (c : Z) : well_founded (zwf c).
  Proof.
    exact (well_founded_ltof Z (f c)).
  Defined.
   
  Lemma pos_acc : forall x a, Zpos a <= x -> Acc Pos.lt a.
  Proof.
    intro x.
    induction (zwf_well_founded 1 x) as [z Hz IHz].
    intros ? Hxa.
    constructor; intros y Hy.
    eapply IHz with (y := Z.pos y).
    unfold zwf. clear Hz; clear IHz.
    apply Zabs_nat_lt.
    split; nia.
    reflexivity.
  Defined.


  Lemma poslt_wf : well_founded Pos.lt.
  Proof.
    red; intros ?.
    eapply pos_acc.
    instantiate (1 := Z.pos a).
    reflexivity.
  Defined.

End wf_proof.

Require Import Coq.ZArith.Zwf.

Section wf_not_reducing.

Lemma poslt_wf : well_founded Pos.lt.
Proof.
  unfold well_founded.
  assert (forall (x : Z)  a, x = Zpos a -> Acc Pos.lt a).
  intros x. induction (Zwf_well_founded 1 x);
  intros a Hxa.
  constructor; intros y Hy.
  eapply H0 with (y := Z.pos y).
  unfold Zwf. split; nia.
  reflexivity.
  intros ?. eapply H with (x := Z.pos a).
  reflexivity.
Defined.

End wf_not_reducing.

[1] https://github.com/mukeshtiwari/Coq-automation/blob/master/Gcd.v#L196-L228
[2] https://github.com/mukeshtiwari/Coq-automation/blob/master/Gcd.v#L175-L187
[3] https://github.com/mukeshtiwari/Coq-automation/blob/master/Gcd.v#L226
[4] https://github.com/mukeshtiwari/Coq-automation/blob/master/Gcd.v#L237