Skip to Content.
Sympa Menu

coq-club - RE: [Coq-Club] Simplification for typeclass instances

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Simplification for typeclass instances


Chronological Thread 
  • From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: RE: [Coq-Club] Simplification for typeclass instances
  • Date: Mon, 12 Sep 2016 07:04:34 +0000
  • Accept-language: de-DE, en-US
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga04.intel.com
  • Ironport-phdr: 9a23:182eehzV5nOc/NbXCy+O+j09IxM/srCxBDY+r6Qd0eMXIJqq85mqBkHD//Il1AaPBtSCrawbwLCG4+igATVGusfZ9ihaMdRlbFwssY0uhQsuAcqIWwXQDcXBSGgEJvlET0Jv5HqhMEJYS47UblzWpWCuv3ZJQk2sfTR8Kum9IIPOlcP/j7n0oMyKJVsXz2DtMfsydEzw9lSJ8JFOwMNLEeUY8lPxuHxGeuBblytDBGm4uFLC3Pq254Np6C9KuvgspIZqWKT+eLkkH/QDVGx1ezN92Mq+/xLEVE6E4mYWemQQiBtBRQbfplmuVZDo9yD+q+BV2S+APMSwQ6piChq46KI+AiTvhSgbLTkhtCnyi8dwha9f6lr1oh10w4fZZMeOM/dxYrnaZfsbQ3ZMWoBaUCkXUdD0VJcGE+dUZbUQlIL6vVZb9RY=
Dear Jonathan, Daniel,

> On 09/09/2016 01:46 PM, Jonathan Leivent wrote:

> However, I still think there's no way to detect instances vs. other
> definitions.

I think there is a way to show that an instance of the same type as the term
in question exists:

eauto 1 with nocore typeclasses

This should only proof goals which are immediate typeclass instances (search
depth = 1). Then one could check if the proof term obtained in this way is
equal to the term in question. This would check if a term is equal to an
instance.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

Archive powered by MHonArc 2.6.18.

Top of Page