The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Wed, 09 Mar 2011 08:32:47 +0100,
Pierre Casteran 
<pierre.casteran AT labri.fr>
 a écrit :

That doesn't explain what makes Coq stop the evaluation of bottom.

Try "Compute bottom 1.", coq immediately respond.
Try "Compute bottom 2.", coq almost immediately respond (and go one
                         step further in the evaluation).
Try "Compute bottom 3.", coq doesn't almost immediately respond
                         (goes one more step further).
Try "Compute bottom 4.", be patient.

To better understand what happens, try:
>>>>>>>>
Require Import Program.
Require Import Wf.

Program Fixpoint bottom (n:nat) { measure n } :=
 match n with
 | O => O
 | S n => S (bottom (S n))
 end.
Next Obligation. Admitted.

Ltac x :=
fail
|| (progress cbv zeta; idtac "zeta")
|| (progress cbv iota; idtac "iota")
|| (progress cbv beta; idtac "beta")
.

Goal bottom 1 = 0.
cbv delta [bottom].
x.
x.
cbv delta [bottom_obligation_2].
cbv delta [Fix_sub].
x.
cbv delta [Fix_F_sub].
x.
cbv delta [proj1_sig].
x.
x.
x.
cbv delta [proj2_sig].
x.
x.
x.
cbv delta [Acc_inv].
x.
cbv delta [Wf_nat.lt_wf].
cbv delta [Wf_nat.well_founded_ltof].
x.
x.
cbv delta [Wf_nat.ltof].
x.
cbv delta [lt].
x.
cbv delta [False_ind].
x.
cbv delta [False_rect].
x.
cbv delta [nat_ind].
x.
cbv delta [nat_rect].
x.
x.
x.
x.
x.
x.
x.
x.
x.
x.
x.
x.
x.
cbv delta [MR].
x.
(progress compute)||(idtac "end of computation").
Abort.
<<<<<<<<<<<<<<<<
Note: I know that "cbv delta …" is the same as "unfold …",
and there exists some tactic like "simpl", but doing so make more clear,
what a succession of computations result in.

In particular you can see that there is no heuristic to tell Coq to
stop computations if it seems to loop.

> Hi,
> 
>    In your second example, (on coq8.3), I've got no
> obligation to prove manually. My code differs slightly from
> yours, because yours was not accepted (see attached file).
> 
> 
> So, div2 is well defined (all proof obligations are solved
> and properly "Defined" (not "Admitted").
> 
> This is not the case of bottom, whose "definition" contains
> something like an axiom.
> 
> Pierre
> 
> 
> 
> 
> 
> 
> 
> Quoting Luke Palmer 
> <lrpalmer AT gmail.com>:
> 
> > I'm fairly new to Coq (have been for a couple years ;-), trying to
> > get a feel for well-founded recursion.  I have defined this program
> > using Russell:
> >
> > Definition id A (x:A) := x.
> >
> > Program Fixpoint bottom (n:nat) { measure (id nat) } :=
> >  match n with
> >  | O => O
> >  | S n => S (bottom (S n))
> >  end.
> > Next Obligation. Admitted.
> >
> > Compute bottom 2.
> >
> > I'm wondering how Coq manages not to get into an infinite loop here.
> > It shows me some ghod-awful gnarly term instead, as if it got stuck
> > evaluating the admitted obligation.  What confuses me is that the
> > program:
> >
> > Program Fixpoint div2 (n:nat) { measure (id nat) } :
> >  match n with
> >  | O => O
> >  | S O => O
> >  | S (S n) => S (div2 n)
> >  end.
> > Next Obligation. Admitted.
> >
> > Compute div2 100.
> >
> > Manages to reduce to normal form just fine.  What mechanism is
> > causing Coq to stop evaluating bottom, but not div2?
> >
> > Thanks,
> > Luke
> >
> >
>