coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Adam Chlipala <adamc AT csail.mit.edu>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Module types as types
- Date: Sun, 13 Mar 2022 08:43:36 -0400
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=adamc AT csail.mit.edu; spf=Pass smtp.mailfrom=adamc AT csail.mit.edu; spf=None smtp.helo=postmaster AT outgoing-stata.csail.mit.edu
- Ironport-data: A9a23:UWqylKvwKidoSfpQ/jHXmIkuPefnVLlYMUV32f8akzHdYApBsoF/q tZmKT/Sb6yPYmSneNBxPYTioU8GvZHSy9Q3GgNrrXsyFyMVgMeUXt7xwmXYb3rDdJWbJK5Ex 5xDMYeYdJhcolv0/ErF3m3J9CEkvU2wbuOgTraCY0idfCc8IMsboUsLd9UR38g52bBVPyvX4 Ymo+5aGYwf8s9JJGjt8B5yr+EsHUMva42twUmwWPZina3eD/5W9JMt3yZCZdxMUcKEMdgKJb 7qrIIWCw4/s10xF5uVJPVrMWhZirrb6ZWBig5fNMkSoqkAqSicais7XOBeAAKtao23hojx/9 DlCnduLFQp2AZHFo6cMaClZAgpsHole/IaSdBBTseTLp6HHW3zx3/ppDUc5eJYE8/p+R2pV/ P0cbjUMclaOi//eLLCTE7M8wJ97apOtZtpH0p1j5Wmx4fIOSJzKRq7i7sRR3TN2g8FSW/vSe qL1bBI/N0WeOUwRUrsRIL03krmWt2TeSmx773KZuJts2zeNnTUkhdABN/KMJ4XRHq25hH2wr WXfum/9HxsyL82a0TPD83S2h+aJkzmTZW4JPLql6vFtgVucg3cPAQEfE1CgqPi9zEu/R5RSJ 1F8FjcSQbYas3f3Q4bCYxSD42+/jh8NcMhzN/U+0VTYokbL2DqxCm8BRz9HTdUpss4qWDAnv mNlefu0X1SDV5XIExqgGqeoQSCaZXJOczNSDcMQZU5auoGy8N5bYgfnE75e/LiJYsoZ8N0a6 xuDqSIkhrkcgKbnPI3jpwmc0lpASnXfJzPZCy3QQ36q6QJ/a8u+e4W04B7Q9v9BKMCcT0XHs XQZ8yR/0AzsJczT/MBuaLxQdF1M2xpjGGeH6bKIN8NwnwlBA1b5IehtDMhWfS+FyPosdz7ze 1P0sghM/pJVN3bCRfYpP93oUp9wkPSxSImNuhXogjxmPMQZmOivon8GWKJs9z6FfLUEy/hna MvHKa5A815BUfk9pNZJewvt+eZ2n3tlrY8ibZXy1A+u2rqDf3OJVaxNMV2VcuEl8b+J6ALbu 8pSPMuMzBFYX/yWX8Uk2dF7ELz+FlBiXcqeg5UOLoare1M2cEl8VaO56e5/KuRNwvQE/s+Vr yrVchIJlzLX2yadQS3UMS8LVV8adcslxZ7NFXZybQ/ANrlKSdvH0ZrzgLNsJOh5rrM/laAoJ xTHEu3Zaslypv3802x1RfHAQEZKLXxHXCqCYHioZiYRZZllS1Cb89PoZFK0piIVByuz884/v /ut2h6CGcgPQAFrDcD3bvOzzg/h4CZAxL4qB0aYcMNOfEjM8ZRxL3CjhPEAJcxRew7IwSGX1 lrLDBpB/bvNroY5/cPnn6eBq4v1QeJyElADRDvQ9r+3MW/f/3blzINdCb7acTfYXWLy2aOje eQJn6yibaFbxA5H6tMuHaxqwKQy48rUi4Vblgk0Tm/Wa1mLC697JiXU18d4sKAQlKRSvhG7W x7S99RXZeeJNcfiHAJDLQYpdL7Th/YJhjbV7PI6ZV7m7TN+urGcWERWeRyNlGpQIKYsaNEpx uIoucg37Q2ji0Z6b4jb0nwMr2ncfGYdV6gHt40BBNO5gAQczFwfM4fXDTX74c3SZtgQYFMmJ CSY2PjLi7hGnBqQdGcvGn/M2+UYnogHpBkMx0QLJlDPn9vZwPI7wUQJozgwSw1UyDRB0v5yZ jg2aRApef3W8mc6ntVHUkCtBxpFWE+T9Hv3xgZbj2beVUSpCjHAIWBV1TxhJ6zFH7+wvwS3/ Y10DE7iTCrle8D30W4pRUd5orroVtVw8kvHmdzhEsiYd3X/jfwJnYf2DVfkaTO+aS/yuKEDj eJx9ed0L6j6KWgdr7BT50yyy+ELUB7dTIBdaagJwU7KdF0wvBm5wjGPLwa0e98LKvDXmaN95 wqCOeoXPymDOO2yQvz3yELCz3KYXBLk2TbaRo7WGA==
- Ironport-hdrordr: A9a23:q0aQPK01kS7o/kqB5k0rAAqjBKUkLtp133Aq2lEZdPUnSKylfq GV9sjzuiWZtN98YgBEpTnEAtjlfZq+z/FICOsqUItKNTOO0ACVxcNZnOnfKlbbehEWmNQttp uIP5IRNOHN
- Ironport-phdr: A9a23:9TD1xB1b0antk7+9smDO9g4yDhhOgF0UFjAc5pdvsb9SaKPrp82kY BaFo6w30hSVBs3y0LFts6LuqafuWGgNs96qkUspV9hybSIDktgchAc6AcSIWgXRJf/uaDEmT owZDAc2t360PlJIF8ngelbcvmO97SIIGhX4KAF5Ovn5FpTdgsipyey+4YDfbxtJiTaybr5/I gi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjT bxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr8zRDqi8 rxrSAf2hygbKz43/mbXislqg6JaphKquhhzzoHQbY2QMvd1Y6HTcs4ARWdZQslfVCJPDYyyY IUSEeQBM+ZWoIvmqlQUsRezHxOhCP/hxzJKgHL9wK000/4mEQHDxAEtA88Bv27RrN7oKqoSU eS1zKjQzTrZa/NZwyr25Y/SfR88u/6MWK5/fNHNxkk0DQzFj1GQpZbgPzOUyuQBqXaU4Pd9V e+2jWMstg5+rCS1yMg2lonJmpwaykrC9ShhwYs4J9O2Rk55bNOlEJVcqSKXOopoT84mTG9mt yU3x78YtZOnYSQHyJoqywLfZvGId4WF/BzuWPiQLDp2hH9oebSyjAu8/0inz+3zTMi00FBSo ypKk9nMqnAN1wHI5cSdS/t9+UGs0iuM2QDL8uxIPF44mKnBJ5Mv3rI8jIQfvV7dEiPrhEn6l K2be0s+9uS29ujqZq/qq56cOoNulw3yLLgil8qiCuoiKAcORXKU+eGk2b3j40L5RLJKg+Uxk qnErJDaKsMbpq+/Aw9ay4oj8Aq/AC260NsCh3UIMElFdwiGj4jtIV3OJfH4Deulj1uyjThr2 ujKPrznAprTMnjOiKrtcah+5kJGxgc/0cpT64xOBr0fPf7/Rlf9tNnCAR84Nwy0zfznCNJ41 o4GQ22AH7WWMKbOvlKT+u0vOPODZI4RuDrnLvgl5uLugWUnllAAYKmlxZ0XZ2ugEfR8P0qZe WbsgssGEWoSowYyVPbqh0GaUT5Pe3ayWLox6S08CIK/FIvMWoStgKGa0yqgBZ1XZmVGCkiWH nvydoWEXe0MaCOILcN7nDwET+vpd4h03ha38QT+1rBPL+zO+yReu4iw+sJy4rj6mRg3vRd0C 8WF2mWEBzV9kmoNTBc9x6l+pQp4y0vF3KRl1a8LXedP7u9EB19pfaXXyPZ3XoyjMuqgVtKAS VL9B86jHSl0VdUphdkHf0d6HdymyBHFxSujRbEPxPSQHJJh1KXa0jDqItpljW7c3fwog1AjS eNELmSnguh69hSVCoLUwA2Cj6j/Ta0Hx2bW8Xubi2+HvUVWSgl1BKzJVHUUTkDNpNX9oEbDU /mjBal0ehBZx5ukLa1HIsbskU0ARPrnP4HGZHmtnm6rGRuS7rSRcIXtemMSmT7BAVQN1QsI9 HeCcw0/GmGsr3+24CVGM1Xpbgus9OB/rCj+VUoo10SRaFUn0bOp+xkTjPjaSvUJ37tCtj1z4 zNzVE2w2d7bEb/i70JoYblcbNUh4VxGyXORtgpzOYalJrxjgVhWehp+vkfn3RF6Qotals1io HQvxQt0YaWWtTEJPzqU1JX7ErbMI2j2uhWud+jb1kyfmNea96ET6egp/k35tVLhHU4j/nN7l thNhiLGttORVExIF8ioChVSlVAyvbzRbygj6pmB0HRtNfLxqTrew5cyA/NjzB+8ftBZOafCF QnoEsRcCdL9TY5i01WvcB8AO/hfsaAuOMbzPfKK0augFO17lTOiy2FG/MZw3l/GpE8eAqbYm o0Ixf2VxF7NXjv1iVyJudv+mIQCYDAOWGez1GK3TJ4Ubap0c4ERDG6oKMDi3dRyianmXHtA/ UKiDVcLsCOwUSKbdEe1nQhZ1EBM5GeihTP91Dts1TcgsquY2iXKheXkbhsOfGBRFiFuilLlI I78iN5/PgDgZgQgkRCN7l3zxqwdoaVjaWTfXA9EcjP3IGdrTqar/uPYM4gUsNVy938OCKy1e hiCR6T4ogcG3i+GfSMW3z09ezyw+934kxF8lGOBPSN2pXvdd9t3wESX79jdSPhNmzseEXAi2 X+MXh7meYPwpYbx9d+LqO21WmO/W4cGdCDqydjFry6n/ShxBgX5mfmvm9rhGAx80Cnh1tAsW z+byXS0KoTtyam+NvpqO0dyA1qpocN2E4R1uoArjZAUn30bmtOY8WdNwgKReZ1LnLnzanYAX 2tBytLc5QPN01ZqL3bPwoPlEHiR34EyArvyKnNT0SU74cdQDa6S57ERhip5rG2zqgfJaOR8l DMQmrM+rWQXiOYTtE8x3z2QV/oMSFJAM3WmxHHqp5iu6b9ab2G1ff2s2VpiyJq/WaqarFgUW W6lKM54TWkrtoMndgqLiSC765m4KoCAK4hN8EXSy1CZ0Y03YNowjqZY3HohYju75Tt9jLdlx R12gcPj5tjBdj8rpOThRUcGfjztOZFJpGm23/oGxs/Ejcf0RN15Bi9DWYuNL7rgETQZsenrO lSLESF6p3uGUazWGQvVgKt/h1TIFZ3jd3SeJX1CiM5nWAHYP0tHxgYdQDQ9mJc9UAGs3s3oN kljtHgX4Rbjpx1Ax/gNVVG3W3rDpAqudjY/SYSOZBtQ4AZY4k7JMMuYputtFiBc95eloUSDM GueLwhPCGgIXASDCTWBdvG24sLc9uGDGuekB/zTfbqJqOpREuyUzI6mlIB99jeIcMCOIj9vA +B6kktPUHZlGtjIzjUCTytE8kCFJ8WfpRq65mh2tpXmqqStA1qpv83VUuMBVLcnswq7iqqCK eOK0SNwKDIDk4gJ2WeN078HmlgblyBpcTCpV7UGry/ECqzKyco1R1YWbT1+MMxQ4ucyxA5Ib ITShtrw3ZZzlfc0DxFAVECnl820L59vQSn1JBbcCUCHOa7TbyXM2N3yaLigRKd4i/hIuBqxv zneCFPqIj3FnCLgVhTpNOBQyiyXIVYN3eP1OgYoAm/lQtX8bxS9O9Iiljw6z4o/gXbSPHIdO zxxG6uihraL5CJcxPB+BypM4mc3dIFsfg6S9ODZLtATsOctDyhpxboyCJUSzKZJ4yZFQvMwg zfbstcoqEqvk+3Jzzt7FhdCt2QT7L8=
- Ironport-sdr: jAVEBKwz7xEW38uDMLeFYAvLxpTbHeiLk1vMiRigOEemMmAx8Gr0unm9+lLAELTzwe1Y42nTTk Fu+K+sf4eaZbU4yK0SkAEoLQxQM8fAMO9OB7Ir+jiR63y53GOlejDOBlXhfhKVicbEsLlvEssA Sl18W7Ba2FFgauIh1DMNpwXuWFTypxTuJd3RmvJc5u+WK/VNLER08ufUHsaatMOMEG25dxuiYa sM6mOtmqXN5LgGKCrOLFriAfeTq3r4QbQ9zmaPNP5Ui9mxSHYHNx3efDxXj446IYlLHfq3OGXi yG1NBD+m9b32MTa/aWTGrIz6
Module Type AbelianGroup.
Include Group.
Axiom comutative : forall a b : T, operation a b =
operation b a.
End AbelianGroup.
[...]
Theorem plus_group : AbelianGroup with T := T, operation
:= plus, identity = zero, inverse = unary_minus).
(* proof that it exists with specified operators *)
End plus_group.
As you've discovered here, modules are not first-class in Coq. There is no way to define a module from within a Gallina term, just to reference module members. I suppose technically the Coq vernacular language could allow use of the tactic mode to define a complete module (albeit with the complication that the goal is no longer a Gallina term), but I don't think that support exists either.
You may not be aware that the style of definition you are
pursuing is already one of the standard uses of Coq, rather than a
fully novel experiment. The Mathematical Components
project may be the most extensive work with algebraic
hierarchies. They use canonical structures (a relative of type
classes) instead of modules.
- [Coq-Club] Module types as types, Constantine Plotnikov, 03/13/2022
- Re: [Coq-Club] Module types as types, Adam Chlipala, 03/13/2022
- Re: [Coq-Club] Module types as types, Meven LENNON-BERTRAND, 03/14/2022
- Re: [Coq-Club] Module types as types, Pierre Courtieu, 03/14/2022
- Re: [Coq-Club] Module types as types, Meven LENNON-BERTRAND, 03/14/2022
- Re: [Coq-Club] Module types as types, Adam Chlipala, 03/13/2022
Archive powered by MHonArc 2.6.19+.