[Coq-Club] Problem using Coq-equations in a polymorphic setting.

[Yves Bertot]

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.

[Matthieu Sozeau]

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

Post by Yves Bertot
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' 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.

[Yves Bertot]

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

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
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

Post by Yves Bertot
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' 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.

[Matthieu Sozeau]

Hi Yves,

Indeed, it should be typed in a context with just the section variables.
Then you would see the problem more clearly. Can you open an issue on
Equations’ github about it?

Best,
— Matthieu

Post by Yves Bertot
I am now trying to think about what could be a good error message.
Error: Cannot infer this placeholder of type
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
------------------------------
*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
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

Post by Yves Bertot
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' 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.