The Coq mailing list

[Yves Bertot <Yves.Bertot AT inria.fr>]

Dear Sorin,

In my opinion, the bug is that this is reported as an anomaly.  I 
participated in the design of the Function command a while ago, and at 
the time, it was clear that nested recursion could not be handled, given 
the technology that was employed.  You code is designed in a way that it 
looks like nested recursion.

the expression 'match f tr with ...' appears in one of the branches of 
the expression 'match f tl'.  In reality you don't use nested recursion, 
because the pattern on 'f tl' in this case is not used (it is an 
anonymous pattern '_'), but this is too hard to guess for our crude code 
analyzer.

Your code could be rewritten to make it obvious that the recursive call 
are direct calls to sub-terms that are already visible even without the 
first call.  One problem with this is that the code you obtain is 
functionally equivalent, but risks having a different complexity 
behavior when the executed with an 'Ocaml-like' evaluation strategy.  
For proof purposes, functional equivalence is enough.  To fix the 
complexity behavior, it depends on the technology you use to obtain the 
final executable code. For instance, if you use extraction, I believe 
you should be able to request that the "combine_results" function be 
inlined.

Here is my replacement for your code.



On 07/17/2016 01:38 PM, sorin stratulat wrote:
> Dear Coq-club,
>
> I have encountered a problem when defining a recursive function on 
> binary trees. A simplified version of the problem is given below:
>
> -----------
> Require Import Recdef.
> Require Import Program.
> Require Import List.
>
> Inductive Btree : Set :=
>   | Epsilon : Btree
>   | Node : Btree -> nat -> Btree -> Btree.
>
> Fixpoint nr_nodes (t: Btree) : nat :=
>   match t with
>     | Epsilon =>  0
>     | Node tl n tr => S ((nr_nodes tl) + (nr_nodes tr))
>   end.
>
> Require Import Omega.
>
> Function  f (t: Btree){wf (fun t1 t2: Btree => (nr_nodes t1) < ( 
> nr_nodes t2)) t}: Btree :=
>   match t with
>     | Epsilon => Epsilon
>     | Node tl _ tr =>
>       match f tl with
>       | Epsilon => Epsilon
>       | _ =>
>         match f tr with
>         | Epsilon => Epsilon
>          |  _ => Epsilon
>         end
>       end
>   end.
> Proof.
> intros. simpl. omega.
> intros. simpl. omega.
> apply (well_founded_lt_compat Btree nr_nodes).
> intros. trivial.
> Defined.
>
> --------
>
> When Defined is executed (the last line), Coq yields "Anomaly: Cannot 
> create equation Lemma. Please report.". This is exactly what I am 
> doing, i.e. reporting this problem.
>
> Is there any way to avoid this problem or should I wait for the next 
> release (I am using 8.5pl2 new version) ?
>
> Thanks for any help,
>
> Sorin