coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?
Date: Fri, 5 Feb 2021 15:32:49 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt1-f169.google.com
Ironport-phdr: 9a23:PGbUGhIOFvieQOXLv9mcpTZWNBhigK39O0sv0rFitYgfKvnxwZ3uMQTl6Ol3ixeRBMOHsqMC17Sd7/qocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmT6wbal9IRi3ogncudcaipZ+J6gszRfEvmFGcPlMy2NyIlKTkRf85sOu85Nm7i9dpfEv+dNeXKvjZ6g3QqBWAzogM2Au+c3krgLDQheV5nsdSWoZjBxFCBXY4R7gX5fxtiz6tvdh2CSfIMb7Q6w4VSik4qx2ThLjlSUJOCMj8GzPhMJ+jLxVrg+iqRJ4zIHbfI6bOeFifq7fZ94WWXBMUtpPWyFHH4iyb5EPD+0EPetAoYX9pVwOrR2/BQmvGuzvziFHiWHt0K011uQuCwDG3Ag6E90St3TUqdv5P7oVXOC3y6nIyzTDb/BI1jf59ofHbAssof6JXb1qcMrRzVMjGB/CjlWVsIHoOS6e2esRvWaB9eVgSf6vhHA9qwF3ujWj28chhInGi48L1lzJ6SV0zYQ7KNCkR0N3fd6pHIZeuS2GM4Z7Q8MsTmJ2tSom1rALpIC3cSoWxZk6yRPSa/KJfo6V6RzgTOacOSl0iG5hdb6lhBu/8VKsxvD9W8WoylpGsytIn93UunwT1hHf9tWLR/5g8kqlxTmC0g/e5+BYLUwokKfWJZEszaA1m5UIrUvOEDH6lUDogKCKeEUk9O2l6+r5bbr7qJKRMoB5hwHjPqgznMG0HP42PRIUX2eB/OSxzL3j8lP9QLVNlvA2l7PWsJHeJcgCv665HxJZ3p8t6xqiDjqr1M4UnXYALFJCdxKHi5bmN0vSL/D/CPezm1WskDF1yPDaJrDtHInBI3zZnLrifbtx8VNQxQsvwdxF+p5ZC7UMLOr2WkDrtdzYChE5Mxazw+biENh91IQeWWSOAq+aLqzStUGH6fw0LumDYY8aojf9K/w/6/Hyin85nEcRfbO10psPdHC4AvNmLl2Fbnrrm9cNCHsFvg4jTOPxk1CCSj5SZ3OqX60m/D07CYSmDZ3CRo+3mrCB0j27TdVqYTVNDUnJGnP1fc3QUPAVLSmWP8VJkzoeVLHnRZV3hj+0swqvgbhgKOvX9ykVuLrs0dF046vYkhR4vWh2CMKc0GyJQmxckWYBRjtw16d69x8ugmyf2LR11qQLXedY4OlEB19jaMzsitdiAtW3YTrvO9eETFH8HIejCDA1C8stmpoAOhgsXdqliR/H0myhBLpHz+XXVqxxybrV2j3KH+g402zPjfBzgFwvQ88JPmqj1PYmplrjQrXRmkDcrJ6EMKEV3SrD7mCGlDPcs0RRUQo2WqLADykS

Is it possible for an Ltac or Ltac2 tactic to check if one sort A is
a subtype of another sort B (an existing i<=j constraint between
sorts A=Type@{i} and B=Type{j}) without adding any new universe
constraints?

[Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?, jonikelee AT gmail.com, 02/05/2021
- Re: [Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?, jonikelee AT gmail.com, 02/05/2021
  - Re: [Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?, jonikelee AT gmail.com, 02/05/2021
    - Re: [Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?, Pierre Courtieu, 02/06/2021
      - Re: [Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?, jonikelee AT gmail.com, 02/07/2021
        
        Re: [Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?, Jason Gross, 02/07/2021
        
        Re: [Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?, jonikelee AT gmail.com, 02/07/2021
        
        Re: [Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?, Jason Gross, 02/07/2021
        Re: [Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?, jonikelee AT gmail.com, 02/07/2021
        Re: [Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?, jonikelee AT gmail.com, 02/07/2021