Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Module types as types

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Module types as types


Chronological Thread 
  • 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

On 3/12/22 11:10 PM, Constantine Plotnikov wrote:

  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.




Archive powered by MHonArc 2.6.19+.

Top of Page