Zulip Chat Archive

Stream: new members

Topic: Enforcing that arguments are of an inductive type?

view this post on Zulip Li Yao'an (Nov 14 2019 at 08:59):

I've been thinking about using Types to mimic sets. For each set α, we can construct a structure tset with a field of type α and a proof that α is in the set. However, I have run into a problem when defining subsets: what I want is a function subsetthat takes in two tsets and says whether the first is a subset of the second. Informally, we want subset to be : ∀ s : S, ∃ t : T, ↑ s = ↑ t. However, the equality only makes sense if the types of the sets building S and T were the same.

This would be solved if we could enforce that arguments be of a certain type by writing something like :

def subtset {α : Type} {S' T' : set α} (S := tset S') (T := tset T')  :=
    ∀ s: S, ∃ t : T, ↑ s = ↑ t

where (S := tset S') is trying to mean that S is an object of type tset S'.

Naturally, this doesn't work. I've also tried type classes, but that failed for me as well.

What is a sensible way to specify that an argument must be of a given inductive type?

view this post on Zulip Mario Carneiro (Nov 14 2019 at 09:57):

In mathlib, there is a coercion from set A to Type that constructs the subtype, so you can wrote a : s if s : set A and it means what you are calling tset.

view this post on Zulip Mario Carneiro (Nov 14 2019 at 09:58):

It's not clear to me what it means for an element of s : set A to be a subset of an element of some other t : set A, because these elements are both just elements of A, which don't have any subset relation between them. Surely you mean to say simply s \sub t?

view this post on Zulip Li Yao'an (Nov 14 2019 at 10:30):

Thanks for the reply.

I have not seen the automatic coercion of a set to a subtype in Mathlib. Where can I find the code or a reference explaining it?

I meant for S and T to be the tsets (subtypes), but I guess it was not so clear I was inventing notation.

Additionally, for learning purposes, let's say I want to rewrite that part of Mathlib myself.

Say I have a coercion coer : set → α. For two set α's S and T, I wish to express S ⊂ T without mentioning the sets explicitly. That is, I wish to construct a function subset' so that subset' ( (coer S) (coer T) ) is the Prop that S is a subset of T. However, the arguments to subset' don't make sense if S and T are sets over different Types, so I want to enforce the condition that my first argument is exactly tset S' for some S : set α.

In short, my question was: is the above possible? (with direct methods preferred over indirect methods)

view this post on Zulip Chris Hughes (Nov 14 2019 at 10:50):

No. In Lean two types with the same cardinality are indistinguishable, so for example you cannot even prove nat \ne int and you could not prove that two infinite subtypes of nat are not equal to each other, or to any other countably infinite type.

view this post on Zulip Mario Carneiro (Nov 14 2019 at 11:50):

Well, technically you can assert that a type is equal to tset S for some S : set A, but as Chris says type constructors are not necessarily injective so you can't recover S from this fact, and hence there will be no well defined subset relation on such types

view this post on Zulip Kevin Buzzard (Nov 14 2019 at 14:15):

You can just do this:

def subtset {α : Type} {S' T' : set α}  :=
     s: S',  t : T', s.val = t.val

Last updated: May 10 2021 at 23:11 UTC