The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi Jonathan

Nice trick. I never realized that I was creating new constraints by doing this carelessly.

P

Le ven. 5 févr. 2021 à 23:35, jonikelee AT gmail.com <jonikelee AT gmail.com> a écrit :

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