The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 25/04/2014 19:45, Kirill Taran wrote:
> Didn't know about ConstructiveEpsilon module. Thanks for example.
> But why will your example not compute? I don't see any axiom usage there.

This is not related to axioms. The lack of axioms tells you that the 
existence of f' is consistent; it does not tell you that (f' some_x) 
will reduce to a value of Y different from (f' some_x).

The rule of thumb is that, whenever Coq needs to perform a step of 
computation, it has to consume a constructor from a term somewhere. If 
there are no constructor left to consume, Coq will stop reducing things. 
So, as soon as you have some opaque definitions around, e.g. the 
termination lemma, Coq is cut off from its sources of constructors and 
it stops computing.

But that is not an issue, you just need to artificially introduce 
sufficiently many constructors. The attached example shows how to do it. 
It adds 2^64 constructors, which should guarantee that your computer 
will break down before Coq runs out off constructors.

There is a small test at the end that shows the difference between the 
version that does not compute and the one that does.

Best regards,

Guillaume

PS: Do not try to "Print" the f' function. There seems to be a bug in 
Coq that causes it to display garbage. What you see is definitely not 
how f' is defined; what you see is not even well-typed. (I hope it is 
only a display issue.)
Require Import Arith Omega.

Section computable.

Variable Y : Type.
Variable f : nat -> option Y.
Definition not_yet n :=
  match f n with Some _ => False | _ => True end.

Inductive Acc' (n : nat) : Prop :=
  Acc'_intro : (not_yet n -> Acc' (S n)) -> Acc' n.

Definition f' : forall n, Acc' n -> Y.
Proof.
fix 2.
intros n [].
unfold not_yet.
destruct (f n) as [y|].
intros _.
exact y.
intros H.
apply (f' (S n) (H I)).
Defined.

Hypothesis termination : exists n,
  forall m, n <= m -> not (not_yet m).

Lemma wf : forall k, Acc' k.
Proof.
destruct termination as [n Ht].
intros k.
destruct (le_or_lt n k) as [Hk|Hk].
apply Acc'_intro.
intros Hk'.
elim (Ht k Hk Hk').
replace k with (n - (n - k)) by omega.
cut (n - k <= n). 2: omega.
clear Hk.
generalize (n - k).
clear k.
intros k.
induction k as [|k IHk].
intros _.
rewrite <- minus_n_O.
apply Acc'_intro.
intros Hn.
elim (Ht n (le_n n) Hn).
intros Hk.
apply Acc'_intro.
intros _.
rewrite minus_Sn_m with (1 := Hk).
apply IHk.
apply le_trans with (2 := Hk).
apply le_n_Sn.
Qed.

Fixpoint fuel (n : nat) (acc : forall k, Acc' k) :
  forall k, Acc' k :=
  match n with
  | 0 => acc
  | S n => fun k => Acc'_intro k
    (fun _ => fuel n (fuel n acc) (S k))
  end.

Definition not_fueled := f' 0 (wf 0).
Definition fueled := f' 0 (fuel 64 wf 0).

End computable.

Section test.

Definition odouble (x n : nat) :=
  match x - n with O => Some (x+x) | _ => None end.

Lemma double_termination :
  forall x,
  exists n, forall m, n <= m ->
  not (not_yet nat (odouble x) m).
Proof.
intros x.
exists x.
intros m Hm.
unfold not_yet, odouble.
replace (x - m) with 0 by omega.
intros [].
Qed.

Definition double' (x : nat) :=
  not_fueled _ _ (double_termination x).

Definition double (x : nat) :=
  fueled _ _ (double_termination x).

Eval compute in (double' 20).
Eval compute in (double 20).

End test.