The Coq mailing list

[sorin stratulat <sorinica AT gmail.com>]

Dear Yves,

Your solution works amazingly well !

Thanks again,

Sorin

2016-07-18 8:34 GMT+02:00 Yves Bertot <Yves.Bertot AT inria.fr>:

Here is the code:

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.

Definition combine_results (v1 v2 : Btree) :=
  match v1 with
    Epsilon => Epsilon
  | _ => match v2 with
           Epsilon => Epsilon
         | _ => Epsilon
         end
  end.

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 =>
    combine_results (f tl) (f tr)
  end.
Proof.
intros. simpl. omega.
intros. simpl. omega.
apply (well_founded_lt_compat Btree nr_nodes).
intros. trivial.
Defined.

On 07/18/2016 08:32 AM, Yves Bertot wrote:

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