noncomputable card

Stream: general

[Kevin Buzzard]

I'm going to have a summer student working with me on group theory and I wondered whether Sylow 2 and 3 was accessible to them. Talking to @Chris Hughes he seemed to think that a useful prerequisite would be a noncomputable card function which sent infinite types to 0, and claimed that this was @Mario Carneiro 's idea. Does this sound like a sensible thing? I guess that if I were to write it I'd do it in June, because I'd need it by July. I already have bundled normal subgroups and adding metric space examples to Patrick's tutorial project on my Lean pile, plus two more grant applications, so it's unlikely it will happen before then, but I thought I'd run it past the community in case anyone had any comments or tips.

[Mario Carneiro]

It should be easy work

[Mario Carneiro]

you will have a lot of finiteness assumptions though in the theorems, because that 0 garbage case will mess up the algebra

[Reid Barton]

What about an enat-valued card?

[Mario Carneiro]

I like that version the best if we ignore typing problems

[Mario Carneiro]

it's not clear to me how important it is that the value be a nat

[Kevin Buzzard]

@Chris Hughes would an enat-valued version be good enough for applications to Sylow 2/3?

[Mario Carneiro]

Is there a enat.to_nat function? We could compose through that when necessary

[Mario Carneiro]

You can still use the enat version for a predicate like card A = enat.of_nat n

[Mario Carneiro]

which asserts both finiteness and a particular cardinality without a fintype assumption

[Chris Hughes]

enat would be hideous for group theory because you're always raising to the power of the cardinality, and multiplying the cardinality etc.

[Mario Carneiro]

would those theorems work with a predicate like I gave?

[Mario Carneiro]

you have an assumption card A = (n : nat) and then use n in the theorem

[Chris Hughes]

Probably they would. Multiplicity was really bad, because I didn't state theorems like that.

[Johan Commelin]

Why would you need an enat valued card for such predicates?

[Johan Commelin]

Wouldn't the cardinal-valued version suffice?

[Mario Carneiro]

You don't need to import set_theory.cardinal to define the enat version

[Chris Hughes]

Are imports really that bad?

[Jeremy Avigad]

In Lean 2, we had a nonconstructive cast from set to finset which mapped any infinite set to the empty set. So we had set.card s = finset.card (s.to_finset). The cardinality of the empty set still comes out to zero, and it is easy to translate finset theorems (e.g. about card and sum) to set theorems.

The advantage to having card and sum map infinite sets to 0 is that lots of identities hold without preconditions. It makes it much more convenient to work with them. Isabelle follows that approach as well.