The Coq mailing list

[Benjamin Gregoire <Benjamin.Gregoire AT sophia.inria.fr>]

Did you try the lazy strategy?
  B

Guillaume Melquiond wrote:

> 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).
>