The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

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