The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

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


Require Import Program.Wf.

Definition id A (x:A) := x.
Program Fixpoint bottom (n:nat) { measure n } :=
 match n with
 | O => O
 | S n => S (bottom (S n))
 end.
(*
Obligation 1 of bottom:
forall n : nat,
(forall n0 : nat, n0 < n -> nat) -> forall n0 : nat, S n0 = n -> S n0 < n.
 *)

Next Obligation.
Admitted.

Next Obligation.
Search well_founded.
apply measure_wf.
Require Import Wf_nat.
apply lt_wf.
Defined.

Print bottom.

Print  bottom_obligation_1.


Program Fixpoint div2 (n:nat) { measure n } :=
 match n with
 | O => O
 | S O => O
 | S (S n) => S (div2 n)
 end.
Print div2.