coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Generalizing binders don't seem to work as described

From: Tej Chajed <tchajed AT mit.edu>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Generalizing binders don't seem to work as described
Date: Fri, 30 Mar 2018 10:53:04 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=tchajed AT mit.edu; spf=Pass smtp.mailfrom=tchajed AT mit.edu; spf=None smtp.helo=postmaster AT dmz-mailsec-scanner-7.mit.edu
Ironport-phdr: 9a23:9N8kbBcFR+0fEkpGZaNIygA+lGMj4u6mDksu8pMizoh2WeGdxcu5YR7h7PlgxGXEQZ/co6odzbaO6Oa4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahb75+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM28m/XhMx+gqxYvRyvuQBwzpXOb42JLvdzZL/Rcc8YSGdHQ81fVzZBAoS5b4YXEeQOI+RYpJTjqlsOtxS+BxejC/7ywTJPmn/5wa063P4jEQ7YwQMtBNcOsHXIrNnvKqgdTP21wbDOwD7eYf1W3jL955LJchAnufyMXLRwcdDQyUY1DQ/FgE+QpIr4ND2WzuQAq3WX4ul6We+tkWIqqgJ8riKhy8otkoXFmJ4Zx1Te+Sh6wIs5P8O0RFN5bNK+DZddtTyWOo1rSc04WW5oojw1yrgetJ67YicKzJMnygbCZPyCcomE+xfjW/yQITd8n3JqZq6wiw+p8Ue80OL8UM+030hQriZckNTArHUN1x3P6sSdVPRy41qh1S6O1wDV9O5EPVg5mbfYJpI7wLM8jJsevEfZEiL4mUj6lKqWeV8l+uis5eTneLLmppqEOo9olg7+Mr4hms6hDuslKQUOWmmb+fim2LL94EL5Xa1GjucqnanBrJDaOcMbq7alDA9Sy4Yv8gqwDzO70NsDhnQHN1JEeBefj4fzIV3OIfb4De2+g1u2ijtryerGbfXdBcDGKWGGm7P8d/4p4ElFjQE30Np35pROC7hHLuilCWHrs9mNMhI7eye0yuTqBJ0pyogeUGCCDoecMb+UvFOVsLF8a9KQbZMY7W6uY8Mu4OTj2CdgyA0tOJKx1J5SU0iWW/FvIkGXe33p04UEEHtMswYjHrWz1A+yFAVLbnP3ZJoSoykhAdP0CIbfAI2hne7ZhXrpLthtfmlDT2u0PzLoeoGDAK5eZCeAZ8pokzgfWLPkUIQo0xejrkqljb9mMqzZ9jBK7Z8=

You just need to mark identifiers as being generalizable with Generalizable Variable A. (for individual variables) or Generalizable All Variables. See the relevant vernacular documentation for more info.

On Mar 30, 2018, 10:45 AM -0400, Karl Crary <crary AT cs.cmu.edu>, wrote:

I'm puzzled by the behavior of generalizing binders. This is code from
Coq manual:

Class EqDec (A : Type) :=
{ eqb : A -> A -> bool ;
eqb_leibniz : forall x y, eqb x y = true -> x = y }.

Definition neqb_impl `{eqa : EqDec A} (x y : A) := negb (eqb x y).

In regards to the second declaration, the manual says "Here A is
implicitly generalized." But this seems not to be the case. I get the
error message:

Error: Unbound and ungeneralizable variable A

What am I doing wrong?

-- Karl Crary

[Coq-Club] Generalizing binders don't seem to work as described, Karl Crary, 03/30/2018
- Re: [Coq-Club] Generalizing binders don't seem to work as described, Li-yao Xia, 03/30/2018
- Re: [Coq-Club] Generalizing binders don't seem to work as described, Tej Chajed, 03/30/2018