Skip to Content.
Sympa Menu

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

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 
    < Chronological >      < Thread >
  • From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Puzzle: tactic that can check Sort subtyping without adding universe constraints?
  • Date: Fri, 5 Feb 2021 17:34:59 -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-qk1-f174.google.com
  • Ironport-phdr: 9a23:XAJrNhyBSPeeqzDXCy+O+j09IxM/srCxBDY+r6Qd2uofIJqq85mqBkHD//Il1AaPAdyKra4awLaM+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxhMiTanbr5/LRq6oArPusILnYZsN6E9xwfTrHBVYepW32RoJVySnxb4+Mi9+YNo/jpTtfw86cNOSL32cKskQ7NWCjQmKH0169bwtRbfVwuP52ATXXsQnxFVHgXK9hD6XpP2sivnqupw3TSRMMPqQbwoXzmp8qFmQwLqhigaLT406G/ZhMxugqxGoxyupRJ/zYnbb46JO/RzZb/dcNEASGZdRMtdSzJND4WhZIUPFeoBOuNYopHzq1sMqhu+AwisBODxxT9MmHD5w7Y30+skEQ7c3QwgG8gCv2jTrNXwOqsZTOe4zKvPzTXFbvNW2iny6IzWfR8/uvyMUrdwftDQyUkrDQ/KklKQqYn8Mj6Ty+8CvHSV4fB6WuKzl24otRtxoj63y8swhYTFm58Zx07E+Ch6w4s4KsO1RkB0bNCqHpZduT+WOoV2T84/XmxmuCg3xqAYtJC1YiUHy5opyhrfZfKHcIWF5A/oWuWJITpgmn5pZLayiwyx/EWg0OHwSNe43EhQoiZYkNTBuWgB2wLS58SbV/dw+1qt1DKT2A3W5exJIFw4mbbeJpMvzbM/iJ8evl/fESL4hkn7ibGaeVkq+uim7unnbKvpqYKSOoJxhQzzMrkiltG5DO8lKAYBRXKb9v651LD7/U32XrFKjvoun6ncqp/aJMAbqregAw9Wz4ov8hi/Ayqk3dkXh3UHI1VFeBWIj4jtJV7COuz3DfC6g1i0kTdrwe7JPqH5D5nTMnTOlK3tcLV95kJG1gY/085T64hJBrwDL///Qkrxu8bZDh89PQy02eHnCNBl24McXmKPBK6ZMKDMvl+M+O0gPfKBZIAQuDnnKvgl4+TigmM+mV8YZaWpx4cYaGikHvR6JEWUeWbjgtAYEWsTogU+SPHqh0aZXD5IZ3eyWro86SshBIKnC4fDXIGtj6ab0Ce1BJ0FLlxBX1uLCDLjc5iOE6MHbzvXKct8mBQFU6KgQskvz0f9mhX9zu8tLO3S+y4VsZ/u/Ndw7uzX0xo18HY8W8aa1WCOQmV5k0sHQjY32OZ0pkkrmQTL6rRxn/ENTY8b3PhOSApvbceBndw/MMj7X0f6RvnMSFuiRY/4UzQ4T9Z02txXJkgkRInkgRfE0C6nRbQSku7TXcBmwufnx3H0Yv1F5TPezqB41gspR8JOMSutgastr1GCVb6MqF2QkuORTYpZ2SfM8GmZym/X5RNXVQdxVePOWnVNP0Y=
On Fri, 5 Feb 2021 16:12:53 -0500
"jonikelee AT gmail.com" <jonikelee AT gmail.com> wrote:

> On Fri, 5 Feb 2021 15:32:49 -0500
> "jonikelee AT gmail.com" <jonikelee AT gmail.com> wrote:
>
> > 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?
>
> I think I figured it out - the trick is to use backtracking on success
> to undo added constraints:
>
> Ltac issubtype A B := (*assumes A and B are both sorts*)
> first [constr_eq_strict A B
> |let _:=constr:(B:A) in fail 1 "B is constrained <= A"
> |let tA:=type of A in
> let _:=constr:(B:tA) in fail 1 "A and B might be siblings"
> |assert_succeeds (let _:=constr:(A:B) in idtac)
> ].
>

That's not quite right. This is better:

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"
].

Archive powered by MHonArc 2.6.19+.

Top of Page