coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Can one define an implicit coercion from a 1x1 matrix to a scalar?

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Can one define an implicit coercion from a 1x1 matrix to a scalar?
Date: Wed, 21 Aug 2019 16:07:19 +0000
Accept-language: de-DE, en-US
Authentication-results: mail2-smtp-roc.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 mga01.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 11.2.0.6
Ironport-phdr: 9a23:81espBHncFt5fZM2L0bjtp1GYnF86YWxBRYc798ds5kLTJ7zo8qwAkXT6L1XgUPTWs2DsrQY0rCQ6vy7Ej1fqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5sIBmssAncuccbjYRmJ6sz1xDEvmZGd+NKyG1yOFmdhQz85sC+/J5i9yRfpfcs/NNeXKv5Yqo1U6VWACwpPG4p6sLrswLDTRaU6XsHTmoWiBtIDBPb4xz8Q5z8rzH1tut52CmdIM32UbU5Uims4qt3VBPljjoMOjgk+2/Vl8NwlrpWrhK/qRJi347aboKbNPticazSZt4VX3ZNU8JLWiBdHo+wcY0CBPcBM+ZCqIn9okMDoRWjCwmrGuzvxSNIhmXx3a0iy+gqDAbI3A08ENIOqnvbstH1OKkPWu2yyanIzCnMb/NM1jjj7IjEaAshofaSUrJ/bcrR004vFxveg1WRr4zlIy2a1uAXv2eH6OpgUPuihmg6oA9/pTivw90jiojPho8Ny1DE8zl5z5gxJdGiVUF0f9ipG4ZTuSGCL4Z6X8cvT39ytCs6yrAKo562cDYQxJkkxBPTc+GLfomG7x75WuucLy10iGxrdb+7nRq+7EutxvHkWsWp0VtHqjBJnsfMu30CzRDf9NKLR/l780y8wziAzRrT5ftBIU0slarUNZohwrkom5oWvkTMBDP6lFjsgK+XcEUk5van6+D9brr6oZ+cMpd4igD4MqswhsyyGfk0PwwQU2SB+emx1Kfv8E3nTLlQjfA7kbHVsJXAKsQaoq65DRVV0oEm6xunCjem0cgXnXkdI11bfBKLlZPpO1bQL/D3Efe/mVOskC9wyvDHOL3hHovCLnzZnLj9erZ97lZQyBAvwtBH+5JUFrYBLervVU/2rdzUFwM2Mwipw+n8E9h9zYMfWWeXAqCDKq/SsFmI5vguI+aWfoMVtiz9eLAZ4Kukhngg3FQZYKOB3J0NaXn+EO4saxGSZmOpidMcG08LuBA/RarkkgvRfyRUYiP4ZKUx6S0hD5riRaLCTYCkjbjLlHO+H5ZWb21CTEuLHHj0bYKcc/YKdC+WZMRml2pXBvCaV4Y92ET250fBwL19I7+Mo3BKhdfYzNFwotbru1Qy+DhzVpvP1m6EFzgyn2UUSjtw16d68xQkmwWzlJNgivkdLuR9ovZAUwM0L5nZlrUoCtbuVwaHddCMGg//HoeWRAopR9d0+OcgJl5nEoz73BHFwyeuRbQSku7TCQ==

Dear Coq Users,

I wonder if it is possible to define an implicit coercion between a 1x1 matrix (either using mathcomponent’s or Coquelicot’s definition) and the respective scalar type?

I see two problems with this:

1.) I don’t see how I could specialize the coercion to the size parameters 1x1. I can define this as separate type mat11, but then I need to use a type annotation to mat11 to enable the coercion. I tried to make an identity coercion between matrix and mat11 but couldn’t figure it out.

2.) Ideally I would like to have this for matrices of any types, not just specific types like R or C. But I don’t see a way to use a parameter of the first class as second class.

Is it possible to do this?

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, Gary Kershaw
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[Coq-Club] Can one define an implicit coercion from a 1x1 matrix to a scalar?, Soegtrop, Michael, 08/21/2019
- Re: [Coq-Club] Can one define an implicit coercion from a 1x1 matrix to a scalar?, Robert Rand, 08/30/2019