The Coq mailing list

[sorin stratulat <sorinica AT gmail.com>]

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