# Zulip Chat Archive

## Stream: new members

### Topic: Enforcing that arguments are of an inductive type?

#### 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 `subset`

that 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 (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`

.

#### 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`

?

#### 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)

#### 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.

#### 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

#### 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