coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] universe inconsistency on import

From: Christian Doczkal <christian.doczkal AT ens-lyon.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] universe inconsistency on import
Date: Mon, 2 Dec 2019 17:15:06 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=christian.doczkal AT ens-lyon.fr; spf=Pass smtp.mailfrom=christian.doczkal AT ens-lyon.fr; spf=None smtp.helo=postmaster AT labbe.ens-lyon.fr
Autocrypt: addr=christian.doczkal AT ens-lyon.fr; prefer-encrypt=mutual; keydata= mQINBFIuNbYBEADAiZlQsnkRrXHOkaZ2mZIVNxzcBha3+HhZ8IhtxF4t5QXRNWFLtdwBuE8u D0GMB/Lacm/LujwcI756cPM/7PhrUFAyn1IrYHYsK4/O5gBEgbSBRjD0X8mJ0V3oIm/PtjMC YiXBJwzOMNXOeWp+HcyCR0eh2sQD94gbF9SUOKDoamNB3DbLEHKjYPJ9O3zQw/Xai624OXB0 Wk5yIW77I1mGWhwbWxeHOJ/NmhHEU38YfbxXSzCLeMv98bNTej4oA+cPtMZ94AZOSy/oroMh rsr6wA9PL7NS+B1kRbgv6a5KL9latAI7zPeXcVsYw076rL850PLez/SXDuIr9mud4v8Zvcp9 65vTK4lTAD4C4vneNRGt4iwCOIgGsAN6BgqEgr7EwLX8dAX57OXPKZj0/0TdCbu+qsoSrQ3u +Ul6k374jFeIndqg/e9NiJbHjYAuug3cZZ6mH24SXWtTd4hGWi6f26tQQcRyGiduZkw5Wn26 g0UVgps7o2zHwlp9LJVjL3pCw7a9tKOfZaH+h7dV5JsA/Oq+7F3PhTbyNagi4A9igw+0qU+n Ws/nZDVMRiUv+1HY4PG8q6iEGSfHHjwW8InYS+Ah3stTddJ0sLc+0AGutx8ueTE2Ks14c4c8 aNW5y9bNFI/6/UQmOOwGmBeYC/kjZhjhsC3dTJ9uX4pXlMhpLQARAQABtDFDaHJpc3RpYW4g RG9jemthbCA8Y2hyaXN0aWFuLmRvY3prYWxAZW5zLWx5b24uZnI+iQJUBBMBCAA+AhsDBQsJ CAcCBhUKCQgLAgQWAgMBAh4BAheAFiEE6jiiZvHNwp19meaCj7B3SJxkuY0FAl15aM8FCQ0s Zo4ACgkQj7B3SJxkuY2bwg//QRQ7cPxux6ecvFO7livj3ktIqJd6qsuUMDY9g8lKQui86pKV vzycLKocr7naoizCHq6BfvgTRgTrWuz2zGcesj3CDxHP7EzNGhNmjC/AigYaDnG6UxAwF48n 8Q3QivweEUuCENvPmzUd6B/CRmSx+AepjaVWrw9KDGIeiBlYlPgXoTRv+DPKszKIxfhy1Wln i3JSanWoEPMcu+HRE4xPFJim0ddtZRHiFwgLxPSVQ8FdnHh4lFnRaIQe+8Jwry9zW1hj5ZGV R81q1/G+HUXWIoI4WNj/M5hp6WfVWTwdZJvQyeLAMUUMyrmAY+soRxv8fay3n0eYcaQ6LpAY YkrQBoif3zh2DgHwI4nHbpMlw4+heHjt2GVofkRzhn7POlhcH1tm6MERVyTTlRccoxw5tD/B FwWA95xCoiSOq/sPUQvGvjoqiDeE8HhW7x68brxSSOQ5R6k/KSqySTLNbIM7D3aryNzfybH6 DpfYD8GW7C3MshxK1w8AyxbRt+4nAUb7HtIzQ8TcLdoA5v/b83KnhuNRNW1ddepYtavx1kG7 aRwnd4yTDrS1UotDdP40zlAaYvOyK0ewco5Mk2kLglRyKfN/SRmnEUoyGbVg3wL3YCoRqAzU JLAU93il3zaZA6Oh5pch+89t1yth0O+jbKMkeE50mt9t/i/PEAsbByBwA5S5Ag0EUi41tgEQ ALKCkrZVjm7Jr6wZkeYMPs+OCtICbILfcRODKsM/JxEdcxbr99UA5GGi94OXGxvkQf5yLQxG hCzrLJVbrpBvl+stg72/8DrYGCCSl72gxLTTInfFxEvH3xGpBP/oMXdGjk+jxWA48opzsaar Bd9PxvFNZoWjB9jdgzBPpNMa/ykw4ATVC2fzC5xuo4fwUsl1Wu8DFLbMVwSHGXCqmV6QYUXf 0i3EKnNkKRH3a3rd7JsrC0/6lBL8sLoT54K3J6NGii6dzalhOycsSI4R8czclof3RIy5Mh/Z /rqv4d0OgY2b7QOYnGrITVtyC5UqzGMZx0dnQr5Bm7YOHaCML/LjMoYj2ovFh2zjaU6I/smx 3stVkMRpmqB7/cYPktkpGV8K9S0l6Cgiepn9pymU0/NCBFKXrPuoorKz0+X6j6YsSy7PJ1KC EIh2nSPdhB7/4ezw3DB/COfTE8EY+xbPpTF4DfI+4ARrbP953C4Z2JC7xHUGqH+D/TQ2qYiT mfHdZTrzvWYHCERApZKq1Erdpl7mHfFnwyoDB8OqS9QWfwz3Ql8TeoFPP5LdS4PHkEqog2vH j6njJnLDLUcU5OGKVrGiu8qdMGyIJNeyY6eGcl+4RR+iNJaCVSwLDB+otbxCg2cemGAfvTI4 GGpwxXuf8/r8JL9l9Jgr/zw2WroiZwOJDhPpABEBAAGJAiUEGAECAA8CGwwFAlm49m4FCQlr 9DgACgkQj7B3SJxkuY0LJQ//cnR3s/JabXBWAbkjHbHkISOGg9QA0atjtWcYTR6wHt9keERf CCEe6hEz0JjwDAmOnEMH3ehunLYiENAS3HSw5jbh7qS4EiJt1zDEpe7P8lDmuk+nGwYyI7dA kJMU7SSBys3ZDbkz5ejGocGvfq1tW/dB/0o5OVT8h9STM/Gwka1YZdNdKJtA+WGN5NSfEVQ6 CDePi6qWWBc2DYPy5XAK3HD4UpxmX6nBlDRoW1L04sAY6+NlpusxsAK3bbI8aElunVYtEL6k cJyAvVt/VXC4GbmrPduAJ8+799qk6uwbr42EJO12+S9qb5njH4+rVdngPWyiQpugGwMOR4A2 KFB/V/oFi8Ai/ep2tatXilwiXPnewu+RDY5+rqhbwVuf1mQO0owBUe5ZxraMndEBFQIqyFo9 vM6UJ/4XAo7NqEoMgFuM/oA51vJFQGcc++Nl9UVaO7ss101K6pJGIueaYRI+iZ2fbyrxWhRx hqYkpyxvIHdgUDP9h9VY3rYAOfSiMXAcYDGx1ztR36ARt+ZzygOI/55yf6CT04WtSDUQ6z3w 5UkqbX/YPLYjbzMkZAEfZBBy+PNaW2N779aiqWLfDHe47mt3L8B3/Tkh5vfAG7Rch4NmlXFI Idls4nQdC5B213rkODbQOvFU0BKljxbWmCJoEhprrRBUTui6L9zaF49OWrKJAjwEGAECACYC GwwWIQTqOKJm8c3CnX2Z5oKPsHdInGS5jQUCXXlozwUJDSxmmQAKCRCPsHdInGS5jVbfD/4z JOwGB2nw9gspyb+UgXAPvgKUGzEe3TISLZrAMCjrmSjX5CHMZOkRG0wCYtqpZRrqDjn5e2TH KeRy65BfsyL5h2W41dRev3TVDj1JHnwLU0QY3cYRIUOSr4mowMUdTlhUraVHKY6byjzX8W2S XULi3oe4M4zo2pKWZv1Z0Z5VgJRMKmps/ehNspfLNLDnc+S1MW7brnpKfbel+u587W5ua+jE Hs0fFKazB9pLURGiqdeN7LqU9eglwPThUPVNPnRFguPiJfy2LYaP5ok6/u/MKAWQq7ZmsiTc YSuijijaqlDbRl0M1GD4TkLrrL4EqNpzlrKmZ4jSdwFZevkWTZ3iP05Y/gV35g1bZv6lWNQe fomyBQRPtwjkFZcvtnz61mbzK+zLnch+f1ePRyo51NuATJL0KXfNlcxoKk8LcFbIh/0CBN+Q FOubu1kktnEUcVPGR0RxbkiIUBAdh+xMBDT+MQ340edJS9MG6wzFowPDhasehTd09bYOeA+d y+FKR5Fdnzpkbp+cpPZzRalPL+YLPd3q++eopUPCZ2bOx+xCtiPaazDAEMLIYimMJi/6JUJA JsNjPye3w2YOM4zKc4qxHzmCdI2Fa4N/Mh/PxWc+d7nqtjvBv9ZJIi2NXNNUxmUkUcq/Lr2J 5F0WDyswSrSRCTgk0xLPK17r2Ozs67i9nw==
Ironport-phdr: 9a23:b4ocVBeuthOlYXcJH+RzpbaelGMj4u6mDksu8pMizoh2WeGdxcS4Zx7h7PlgxGXEQZ/co6odzbaP6Oa5BjFLscjJmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRu7oR/MusQUgYZuJaU8xxrUqXZUZupawn9lK0iOlBjm/Mew+5Bj8yVUu/0/8sNLTLv3caclQ7FGFToqK2866tHluhnFVguP+2ATUn4KnRpSAgjK9w/1U5HsuSbnrOV92S2aPcrrTbAoXDmp8qlmRAP0hCoBKjU09nzchM5tg6JBuB+vuRJ/zY7Jbo+WOvRxcKzSctEGSmRORctRSy9MD5mgY4cTAecMP+BVpJT9qVsUqhu+ABGhCf3vyj9Sh3/2xrE60+U7HgHAwQcuEdUOv2jVrdX2LqgSVf2+wa7UwjXDdfNW2Cz96JTJch87p/GAR69/cc3NxkguFAPKlFGQpJf7MDOTzeQBqmyb7upnVeKpkWInpRtxryGpy8wxhIfJgYcVxUrF9SV/2Is1JNu4SFR6YdG+CpdQuTuaOo1rSc0hW2FloDs2x7IatZKhfiUHyo4rywPeZvGFaYSE/AzvWPiJLTtlin9oe6izihKz/ES6xeDxUtO43EtJoydKlNTHq2oD2AbJ6sedT/tw5keh1iiL1wDU8uxEJVo7mrHAJJE/2LI/iJwTsV/aEi/ymET2i6mWel8q+uiy8+jnY7PmqYGAN4Jslw3zPbgilta9DOk6KAQCQmmW9Oam2LH940H1Xq1GjvgsnanYtJDaK94bpqm8AwJNzokj6wy/Dza90NQEnHkINlRFdAiagIjuJ17PIfP4Au27g1m3jjhrwevGMqTlApTNKXjDlq3tfbhn60JE0go80chf545ICrEGOP/8RkjxtMXBAhAlNwy03v3oBc5m1oIeXGKPGrWWPLnTsV+O/OIvIvODaJUbuDbneLAZ4KvlimZ8klsAd4Go24EWYTa2BKdIOUKcNFHsmNYaDWYDuEISS+f4i1SGGWpYZ2yzRL497zd9BIWtH4TKQqighqfE2Da8GNtYfDYVWRi3DX70etDcCL83YyWIL5o5y2FWZf2aU4YkkCqWmkr6xr5gd7uG/iQSv5+l2d5uounCkhd0+yYmV53BgVHIdHl9myYzfxFzxLp2+Bcvx1GYlKxphPoeG8YBv6oYADd/DobVyqlBM/63XwvAetmTT1P/GYerByp0SsM2xZkAeRQkFg==
Openpgp: preference=signencrypt

Hi

On 01/12/2019 18:20, Vadim Zaliva wrote:
> “If it is indeed failing to enforce [Helix.MSigmaHCOL.Memory.16 <
> Coq.FSets.FMapAVL.649], then you may get away with enforcing early that the
> universe for FMap contents is strictly larger than the universe for Memory
> contents.”
>
> How can I enforce something like this?
>
If you use explicit universes in the definitions for instance as follows:

Universe U.
Definition foo (T : Type@{U}) ...

Then you can pose constraints:

Constraint U < V.

See also:
https://coq.inria.fr/distrib/current/refman//addendum/universe-polymorphism.html?highlight=constraint#explicit-universes

In my case, where all definitions involved in the conflict where within the
library I was working in, this was sufficient.

I'm not sure what's the best way to give a name to a universe that's
introduced in a library one is importing (e.g., introduce a universe U and
then define an object that generates the constraint U = Coq.Lib.File.n *).
Maybe someone else can comment on that.

Best,
Christian

Re: [Coq-Club] universe inconsistency on import, Vadim Zaliva, 12/01/2019
- Re: [Coq-Club] universe inconsistency on import, Christian Doczkal, 12/01/2019
  - Re: [Coq-Club] universe inconsistency on import, Vadim Zaliva, 12/01/2019
    - Re: [Coq-Club] universe inconsistency on import, Christian Doczkal, 12/02/2019
      - Re: [Coq-Club] universe inconsistency on import, Gaëtan Gilbert, 12/02/2019
        
        Re: [Coq-Club] universe inconsistency on import, Jason Gross, 12/02/2019
        
        Re: [Coq-Club] universe inconsistency on import, Vadim Zaliva, 12/02/2019