The Coq mailing list

[manoury <pascal.manoury AT lip6.fr>]

I defined for binary trees the following measure

--
Definition bt_mesure {A:Set} (bt:btree A) : (nat * nat) :=
  match bt with
    Empty => (0,0)
  | Node _ bt1 _ => (btree_size bt, btree_size bt1)
  end.
—

where tree_size is the usual

--
Fixpoint btree_size {A:Set} (bt:btree A) : nat :=
  match bt with
    Empty => 0
  | Node x bt1 bt2 => S (btree_size bt1 + btree_size bt2)
  end.
— 

I proved that lexicographic ordering of pairs of natural (I call it 
nat_lex_lt) is well founded.
Then I try the following:

--
Equations list_of_btree {A:Set} (bt:btree A) : (list A) by wf (bt_mesure bt) 
nat_lex_lt :=
  list_of_btree Empty := nil;
  list_of_btree (Node x Empty bt) := x::(list_of_btree bt);
  list_of_btree (Node x1 (Node x2 bt1 bt2) bt3) :=
    (list_of_btree (Node x1 bt1 (Node x2 bt2 bt3))).
—

And I get the following:

--
Error:
Unable to satisfy the following constraints:

?w : "WellFounded
        (Telescopes.tele_measure
           (Telescopes.ext Set (fun A : Set => Telescopes.tip (btree A))) 
           (nat * nat) (fun (A : Set) (bt : btree A) => bt_mesure bt) 
nat_lex_lt)"
—

Any hint ? Thanks !

        Pascal Manoury.