Enforcing that arguments are of an inductive type?

Stream: new members

[Li Yao'an]

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?

[Mario Carneiro]

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.

[Mario Carneiro]

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?

[Li Yao'an]

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)

[Chris Hughes]

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.

[Mario Carneiro]

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

[Kevin Buzzard]

You can just do this:

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