Is is possible to describe set cardinality this way

Stream: general

[Ben]

I can see this having problems with infinite sets. But if I can provide some proof that it is well defined, then is possible to define cardinality in the following way

def cardinality {T: Type} (s: Set T) [Decidable (∃x: T, s x)]: Nat := if
  h1: ∃x: T, s x
then
  let w := h1.w;
  (cardinality (s \ { w })) + 1
else
  0

[Ben]

(and yes, it seems I cannot 'pull' the .w field off of h1?)

[Aaron Liu]

It is possible

[Aaron Liu]

But in the well-defined proof I think it will be very very hard to avoid a cardinality argument

[Ben]

What do you mean by "a cardinality argument"?

[Ben]

Even if this is not the best way, wondering if anyone knows how to extract the .w property. As it is given it is Decidable is should be possible right?

[Aaron Liu]

You definitely need choice for that, specifically one of docs#Classical.choose, docs#Exists.choose, and friends

[Aaron Liu]

Unless you add more Decidable instances

[Aaron Liu]

Ben said:

What do you mean by "a cardinality argument"?

Show that it is well-defined because the sets keep getting smaller in cardinality (you see how this is circular?)

[Aaron Liu]

I'm not saying that a cardinality argument is required (and indeed just now I thought of a way to avoid one)

[Yury G. Kudryashov]

This definition is not well founded for infinite sets.

[Aaron Liu]

You do also have to do fine a way to avoid infinite sets