coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Is there something like especialize?

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Is there something like especialize?
Date: Mon, 30 Apr 2018 09:54:13 +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 mga17.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 11.0.200.100
Ironport-phdr: 9a23:WxgTwBG9BsjrWX3hsbaZAp1GYnF86YWxBRYc798ds5kLTJ7zo8SwAkXT6L1XgUPTWs2DsrQY07GQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmDSwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KOT4n/m/Klsx+gqFVoByjqBx+34Hbb46bOeFifqzGYd8WWXZNUtpTWiFHH4iyb5EPD+0EPetAoYXzulwOogWxBQmwHuPvzSdIimfr1qM90uQuDQHG0xY+ENIKvnjfsdL4NKITUe+pzKnH1yvMb/dM1Tfm74jHbB8hoe2WXbJ3acrc0kgvFwXZjlqOrYzpJS+a1uMIs2WC6edrSOyhi2kiqw5rozivwN8hiojPhoIJ1F/E8T91z5srKtC+VUV1YsakHYNNuyyeKYd6WMMvTmFytCs61LEKo4O3cSgXxJg/2hLSavKKf5KG7x/tTuqdPzl1iXZ/dL6ihBu+71CsxvD9W8SwylpGsCpIn9bWunwTzRDf9MeKR/9780y8wziAzRrT5ftBIU0slarUNZohwrkom5oWvkTMBDL6lUfsgK+XcEUk5van6+D9brr6oZ+cMpd4igD4MqswhsyyGfk0PwwQU2SB+emx1Kfv8E3nTLlQk/E7krTVvIjfJcsBp665BwFV0pwk6xa6Fzqm1dUYkmUHLF1fZh2Hi5LlO0rJIP/mAve/n06skDBzx/3dP73hBInNIWbHkLv7Ybl97EtcxBIpzd9D/5JUFq0BIPXrV0Dts9zYFwY1PBCww+b6E9pwzZgeWGKKAq+BKqzeq16I5uQ1I+mNfoAZojj9K+J2r8Lp2DUynkZYdq2017MWbmq5F7JoOQ/RNXHrm5IKFXoAlgs4Vu3jzlOYB219fXG3CugH4Tw0FJihFcOLY4GmgLWM2G3zSphXbWBPB1TKCnDleJmeXO8kaSSOL8snmTsBA+vyA7Q93A2j4Vepg4FsKfDZr3VB5MDTkeNt7uiWrikcsDl9DsCTyWaIFjgmn2UUSjtw16d68xUklgWzlJNgivkdLuR9outTW15jZ5/a0+F+Tdv1X1CZJ4rbeBOdWtyjRAoJYJcxztsJOhkvHtqr10+F3iy2DrtTnLuOVsQ5

Dear Pierre,

> I think that would make a good feature wish.

fine, I will create one.

Does the syntax you outlined work for eapply? I am not such a fan of the
"with" syntax and would like to write:

especialize (H t u _ ?[h2])

in the case you outlined, assuming H has parameters x y and two hypothesis.
Not sure if the ?[name] syntax works for eapply, though. I tend to use it
only with refine.

I think one should keep the syntax and options identical to eapply - in the
end it is not that much of a difference if one tries to solve the current
goal or a prerequisite of a hypothesis.

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

[Coq-Club] Is there something like especialize?, Soegtrop, Michael, 04/30/2018
- Re: [Coq-Club] Is there something like especialize?, Pierre Courtieu, 04/30/2018
  - RE: [Coq-Club] Is there something like especialize?, Soegtrop, Michael, 04/30/2018
    - Re: [Coq-Club] Is there something like especialize?, Pierre Courtieu, 04/30/2018
      - RE: [Coq-Club] Is there something like especialize?, Soegtrop, Michael, 04/30/2018