The Coq mailing list

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

I am now trying to think about what could be a good error message.

The problem is then that if you replace the (@ltt T) with (@ltt _), the error message is different:

Error: Cannot infer this placeholder of type
"Type" in environment:
T : Type
t : btree T

This seems to imply that T should be available in the context where the relation is provided and is

misleading to the user.  Is there a good reason for this error message to mention a context where

T is apparent?

Yves

---

From: "Matthieu Sozeau" <mattam AT mattam.org>
To: "coq-club" <coq-club AT inria.fr>
Sent: Thursday, October 4, 2018 7:19:02 PM
Subject: Re: [Coq-Club] Problem using Coq-equations in a polymorphic setting.

Hi Yves,

  there is an issue indeed that [by rec] expects the relation to be independent from

the parameters (otherwise, the functional it would produce would not allow 

to change T at recursive calls, i.e it would change the type of redo_rev_tree in the body

of the function). It should give you an error rather than this puzzling not-found, I agree.

One solution is to use a section as you did to make it explicit that T is a fixed parameter.

Equations also allows to do recursion on an arbitrary combination of the arguments, so 

you can also do the following:

Definition ltt (t1 : {T & btree T}) (t2 : {T & btree T}) :=

  size (projT2 t1) < size (projT2 t2).

Equations redo_rev_tree {T} (t : btree T) : btree T :=

   redo_rev_tree t by rec (existT (fun T => btree T) T 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.

Best,

-- Matthieu

On Thu, Oct 4, 2018 at 5:06 PM Yves Bertot <yves.bertot AT inria.fr> wrote:

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.