The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I think your check is backwards (admittedly, I gave it to you backwards); you want B -> A for "A is a subtype of B".  Also, even the corrected tactic gives the wrong answer on checking if Set is a subtype of Prop.  Why do you need the element-of check?

On Sat, Feb 6, 2021, 23:27 jonikelee AT gmail.com <jonikelee AT gmail.com> wrote:

On Sat, 6 Feb 2021 22:32:25 -0500
Jason Gross <jasongross9 AT gmail.com> wrote:

> For subtype, can't you just check whether or not (fun x : A => (x :
> B)) typechecks?  This seems to me to be the definition of B being a
> subtype of A.  (Of course, this will insert coercions, so maybe you
> also want to check that no coercions are inserted.)

That's a good point, actually two.  So, to start:

Ltac issubtype A B :=
  first [let _:=constr:(B:A) in fail 1 B "can be ∈" A
        |let _:=constr:((fun x=>x):(A->B)) in idtac
        |fail 1 A "and" B "are constrained to be unrelated"
        ].

The id fun check you suggest makes the constr_eq_strict check
redundant.  Which is good, as I am hitting universe bugs with
constr_eq_strict.  I don't need the assert_succeeds - actually don't
think I ever did.

For the checking for coercions part - I guess I need to parse that
constr to see if the function's body is just x or not.  This might work:

Ltac issubtype A B :=
  first [let _:=constr:(B:A) in fail 1 B "can be ∈" A
        |lazymatch constr:((fun x=>x):(A->B)) with
           | fun x => x => idtac
         end
        |fail 1 A "and" B "are constrained to be unrelated"
        ].

But, the existence of a coercion doesn't mean A isn't a subtype of B,
just that it might not be - admittedly, it probably isn't, else why
need a coercion?  Also, coercions between sorts (other than
something like inhabited:Type->Prop) seem very unlikely.  Still a
little troubling...