The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

On Sun, 7 Feb 2021 07:14:51 -0500
Jason Gross <jasongross9 AT gmail.com> wrote:

> I think your check is backwards (admittedly, I gave it to you
> backwards); you want B -> A for "A is a subtype of B".

Wait... What?  I think you had it right the first time.  If an identity
function can witness A->B (modulo coercions again), that means all As
are Bs, hence A is a subtype of B.

>  Also, even
> the corrected tactic gives the wrong answer on checking if Set is a
> subtype of Prop.

You mean "issubtype Prop Set", right?  That passes now.  I think you
have sub and super swapped.

>  Why do you need the element-of check?

That's what prevents additional constraints when the id function is
attempted later.  If B:A typechecks, then either there is an existing B
< A constraint or there is no current constraint between A and B, and
B:A adds a B < A constraint.  It's the second no-current-constraint case
that I want to filter out (well, both, but the first will cause the id
function to fail typechecking) because it indicates that attempting the
A->B id function would add a A < B constraint.