The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT ens-lyon.fr>]

Hi,

I am trying to convince Coq to compute with some recursive functions. I
can prove that the number of recursive calls is finite, but I am unable
to give an explicit upper bound on the number of recursive calls. So I
am using well-foundedness instead of structural induction in order to
define the function.

I have attached a reduced testcase. The core code can be summarized as
follow:

        Variable test : nat -> bool.
        Hypothesis stop : exists n, forall a, n <= a -> test a = true.
        Function find (x : nat) { wf } : nat :=
          if test x then x else find (S x).

I have a "test" function from nat to bool, and I know ("stop") that it
always returns true after some point. The "find" function computes the
first integer for which "test" returns true. If I mark the proof "well"
of well-foundedness as Defined, and if I give an explicit upper bound,
then Coq is able to compute the result.

Unfortunately, as I explained, I don't have an explicit upper bound. In
order to express this restriction in the testcase, I have obfuscated the
proof of "stop" with a few classical logic statements, so that Coq
cannot get its hands on the upper bound. After this change, Coq is no
longer able to compute. Moreover, if I mark "well" and "stop" as
Defined, then Coq enters an infinite (?) loop.

I guess my question amounts to: Is it possible to compute recursive
functions in Coq without providing a structurally-decreasing explicit
argument? (The ML-extracted code uses an "implicit" one, and it works
just fine.)

Best regards,

Guillaume

Require Import Omega.
Require Import Classical.

Section function.

Variable test : nat -> bool.
Hypothesis stop : exists n, forall a, n <= a -> test a = true.

Definition order a b :=
  if test b then False else b < a.

Lemma decrease :
  forall x, test x = false ->
  order (S x) x.
intros.
unfold order.
rewrite H.
auto.
Qed.

Lemma well :
  well_founded order.
destruct stop as (n, Hs).
assert (Hu: forall a, n <= a -> Acc order a).
intros.
apply Acc_intro.
intros.
unfold order in H0.
rewrite (Hs _ H) in H0.
elim H0.
assert (Hl: forall a b, n - a <= b -> Acc order b).
clear Hs stop.
induction a.
rewrite <- minus_n_O.
exact Hu.
intros.
apply Acc_intro.
unfold order.
case (test b) ; intros.
elim H0.
apply IHa.
omega.
unfold well_founded.
intros.
case (le_lt_dec n a).
apply Hu.
intros.
apply (Hl (n - a)).
omega.
Qed.

(*
Function find (x : nat) { wf order x } : nat :=
  if test x then x else find (S x).
apply decrease.
apply well.
Defined.
*)

Definition find : nat -> nat.
refine (Fix _ (fun _ => nat) (fun x cont => _)).
apply well.
case_eq (test x) ; intros.
exact x.
apply (cont (S x)).
apply decrease.
exact H.
Defined.

End function.

Definition test n :=
  match n with
  | S (S (S (S (S _)))) => true
  | _ => false
  end.

Lemma stop : exists n, forall a, n <= a -> test a = true.
apply not_all_not_ex.
apply ex_not_not_all.
exists 10.
intros H.
apply H. clear H.
do 10 (intros a ; case a ; [ intros H ; elim (le_not_lt _ _ H) ; omega | 
clear a ]).
trivial.
Qed.

Eval compute in (find test stop O).