coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?
Chronological Thread
- From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
- To: Pierre Courtieu <pierre.courtieu AT gmail.com>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?
- Date: Sat, 6 Feb 2021 20:28:57 -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-f175.google.com
- Ironport-phdr: 9a23:xo2zeBxGRsHxk47XCy+O+j09IxM/srCxBDY+r6Qd2uwTIJqq85mqBkHD//Il1AaPAdyKra4VwLCJ+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxhMiTanbr5/KBq6oRvTu8ILnYZsN6E9xwfTrHBVYepW32RoJVySnxb4+Mi9+YNo/jpTtfw86cNOSL32cKskQ7NWCjQmKH0169bwtRbfVwuP52ATXXsQnxFVHgXK9hD6XpP2sivnqupw3TSRMMPqQbwoXzmp8rxmQwH0higZKzE58XnXis1ug6JdvBKhvAF0z4rNbI2IKPZyYqbRcNUHTmRDQ8lRTTRMDI28YYUREuQPPuRXr4f6qVQBsRSwChKhBP/txzJSmnP7x7E23/onHArb3AIgBdUOsHHModn7NqcSVua1zKjLzTrda/NZxyny5ZPHchAku/6MXLZwfdDNxkkoEgPJgEibpIvnPzOS0OQNsmub4PRkVe2xlWEqsA5xoj21ycctjonFnJ4aylfB9Shgxos+ONK3RlJhb9G+DJtQqz+VN5FwQs46X21ltzs2xqAYtJO7fyUHy5sqygDRZfGIfYaF7BzuWPifLDp4mX9oZbKxihiv/UW+xOPxSMq53lhOoyRFktfBtXYA3AHQ5MifUvZx4Fut1DKV2w3Q6uxIO104mKvHJ5I737I9lJoevVzdEiL3hEn6kaqbelgg9+e07unqbbTrqoOAO4JxhAzzMLoil8miDuskPAUDXG2W9vmy1L3t8030RbtKgeMqnqXHtZ3XKtoXq6ClDAJTz40t8QywDy2839QdhXQHLExKeBaAj4XxPlHBOvH4DfOmj1S1jDdn2unKPrP8DpjPLnXPirjhfbF6605TzAo808pT6I5TCrEEOP7zW0nxu8LEDhIhLQC43+LqBM9+244eQ26DH66UPL/IvVOV5O8iI/GAZIoPtzb8L/gl6eTujXg8mVIFf6mp2p0XaHG7Hvt4J0WWf2Tjj8wOEWcPpAU+TejqhEeeXj5UYna+R7g86S0jCIK6EYfDQZigj6CG3CeiB5FZemRGCk2XHnrzbIWFW/IMaDqILcN7kzwEU6KhS4472h20ug/60ekvEu2BwiwVr4junPNy+vfPlBwvvWhsDsmHyWzLRGZphH8JSiIe06V2oEg7wVCGh/tWmftdQJZR4PVIUQo+OJP0wOlzCtS0UQXENJ/dSlGgQ9arBTw8Zt00yt4KJU16HoPx3Vj4wyO2DupNxPSwD5su//eZhiCpfpsv+zP9zKAkymIebI5POGmh3PAt8gHSA8vQjxzcmf/1KOIT2ynC8GrFxm2L7hkBDFxAFJ7dVHVaXXP46Mzj7xqbHbCrALUjdABGzJzac/oYWpjSlVxDAczbFpHbamO1lX23AE/RlLyJZYvuPW4a2XeEBQ==
On Sat, 6 Feb 2021 11:06:58 +0100
Pierre Courtieu <pierre.courtieu AT gmail.com> wrote:
> Hi Jonathan
> Nice trick. I never realized that I was creating new constraints by
> doing this carelessly.
> P
Unfortunately, it doesn't quite work either. The issue with:
Ltac issubtype A B :=
first [constr_eq_strict A B
|let _:=constr:(B:A) in fail 1 B "can be <=" A
|assert_succeeds (let _:=constr:(A:B) in idtac)
|fail 1 A "and" B "are constrained to be unrelated"
].
is that if A is in Type then A might be a sort or a type. Unfortunately
there is no way for the tactic to know which it is going to be - and
issubtype's "(B:A)" test only works to filter out bad cases if A is
clearly a sort (when B is at least a type, possibly a sort).
For instance:
Definition test@{i j}(X:Type@{i})(Y:Type@{j}) : True.
Proof.
issubtype X Type@{j}. (*does not fail, but I want it to fail*)
Maybe the necessary trick is to first check if issubtype (type of A)
(type of B) - and only if this passes check issubtype A B:
let tA:=type of A in
let tB:=type of B in
issubtype tA tB; isssubtype A B.
Or, actually, I don't think I need that final issubtype A B check as
issubtype tA tB is conclusive...?
- [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
- 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?, Pierre Courtieu, 02/06/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
Archive powered by MHonArc 2.6.19+.