coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Scheme Equality

From: Aaron Bohannon <bohannon AT cis.upenn.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Scheme Equality
Date: Thu, 15 Apr 2010 09:33:18 -0400
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:date:x-google-sender-auth:message-id:subject :from:to:content-type; b=ZmuMdxTKWX+7CXaLPGtJsWMbPJH5vGORA6E94bZ5k6gpH76Hh1EUzmj/tv8mYGZooA dVkDvcSpU2a0DGGrXZx3e5Mo+vevAtQ6o1aW2/ciThOpWXk3+VZuznqz3dZqs3hY0Z+l CTOC2wNessfAxVi7Tm6RV+Ma/q18axFRS5b4U=

Hi,

I think "Scheme Equality" is a great feature.  It seems to have a few
limitations, though.

First, type aliasing is a problem.  If you have "Definition foo :=
nat.", you aren't allowed to use "Scheme Equality" for foo, and, more
importantly, you can't use "Scheme Equality" for any type that refers
to foo.  I know this is a big can of worms, but it would make "Scheme
Equality" much more useful if it could handle some forms of defined
types.

Second, if you do "Scheme Equality for list.", you will get this type
for list_eq_dec:

list_eq_dec
     : forall (A : Type) (eq_A : A -> A -> bool),
       (forall x y : A, eq_A x y = true -> x = y) ->
       (forall x y : A, x = y -> eq_A x y = true) ->
       forall n m : list A, {n = m} + {n <> m}

I would have expected (and hoped) this type would be the same as the
one of list_eq_dec in the standard library.

Third, if you have a type like this --

Inductive tree: Set :=
| branch: list tree -> tree.

-- "Scheme Equality for tree" responds:

tree_beq is defined
Error while computing decidability scheme. Please report.

So I'm reporting it.  Maybe it's asking too much for it to handle
cases like that, but it sure would be nice.

BTW, I'm using Coq v8.2pl1.

- Aaron

[Coq-Club] Scheme Equality, Aaron Bohannon