The Coq mailing list

[Robbert Krebbers <mail AT robbertkrebbers.nl>]

Hi Mukesh,

Thanks for finding out the original source of this trick.

Note that the trick is in the Coq standard library these days:

  https://github.com/coq/coq/blob/master/theories/Init/Wf.v#L163

You could submit a PR to add a comment to acknowledge Georges Gonthier 
for discovering it.

Robbert

On 09/10/2021 03.16, mukesh tiwari wrote:
> Hi Xavier
>
> Thanks for pointing to the Krebbers' answer and now the Coq code [1]
> is producing concrete values. During my Google search to solve this
> problem, I also found the same trick by Thomas Braibant [2] from 2009
> and yesterday, on Zulip chat, Guillaume Melquiond pointed to the
> Georges Gonthier  [3]  from 2007.
>
> Best,
> Mukesh
>
> [1] https://github.com/mukeshtiwari/Coq-automation/blob/master/Gcd_guarded.v
> [2] 
> https://coq-club.inria.narkive.com/gO2dnKc4/well-founded-recursion-stuck-on-opaque-proofs
> [3] https://sympa.inria.fr/sympa/arc/coq-club/2007-07/msg00013.html
>
>
> On Sun, Oct 3, 2021 at 7:50 PM Xavier Leroy
> <xavier.leroy AT college-de-france.fr> wrote:
> > 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