The Coq mailing list

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

I am trying to write a tutorial example using binary trees and show how 
to use the ..._elim theorem generated by the Equations package.  I would 
like some help.

Here is a self contained example.

Require Import Arith.
From Equations Require Import Equations.

Inductive btree (T : Type) : Type :=
  Leaf | Node (val : T) (t1 t2 : btree T).

Arguments Leaf {T}.
Arguments Node {T}.

Fixpoint count {T : Type} (p : T -> bool) (t : btree T) : nat :=
match t with
| Leaf => 0
| Node x t1 t2 =>
  (if p x then 1 else 0) + (count p t1 + count p t2)
end.

Definition size {T : Type} (t : btree T) := count (fun x => true) t.

Lemma size1 {T} (a : T) t1 t2 : size t1 < size (Node a t1 t2).
Proof.
unfold size; simpl.
unfold lt; apply Peano.le_n_S, Nat.le_add_r.
Qed.

Lemma size2 {T} (a : T) t1 t2 : size t2 < size (Node a t1 t2).
Proof.
unfold size; simpl.
unfold lt; apply Peano.le_n_S; rewrite Nat.add_comm; apply Nat.le_add_r.
Qed.


Section redo_rev.

Variable (T : Type).

Definition ltt (t1 t2 : btree T) := size t1 < size t2.

Equations redo_rev_tree (t : btree T) : btree T :=
  redo_rev_tree t by rec t ltt :=
  redo_rev_tree Leaf := Leaf ;
  redo_rev_tree (Node a t1 t2) := Node a (redo_rev_tree t2)
                                        (redo_rev_tree t1).
Next Obligation.
apply size2.
Qed.
Next Obligation.
apply size1.
Qed.

End redo_rev.

Equations redo_rev_tree' {T} (t : btree T) : btree T :=
  redo_rev_tree' t by rec t (@ltt T) :=
  redo_rev_tree' Leaf := Leaf ;
  redo_rev_tree' (Node a t1 t2) := Node a (redo_rev_tree t2)
                                        (redo_rev_tree t1).

I would like to avoid to define my function redo_rev_tree in a section, 
so this is the reason why try to define the function redo_rev_tree'.

It complains That T is unknown, but when I replace T with and 
underscore, it complains that it can't guess the value for this place 
holder, which should be determined in a context where T appears...

Error: The reference T was not found in the current environment.