Fintype and Finite

Stream: mathlib4

[Peter Nelson]

@Oliver Nash mentioned in his review for #23399 that mathlib is moving to preferring Finite over Fintype in hypotheses, often accompanied by Nat.card over Fintype.card in statements. I'm a huge fan of this!

One annoyance, though, is that because the actual proof will often involve Fintype and sometimes Fintype.card for subtypes, proofs often open with the multi-line fluff have := Fintype.ofFinite a (for one or more types) as well as classical.

I think a one-line tactic that takes care of this invisibly would be nice. But also, one of the features I remember being touted with lean4 was loops in typeclass search. Could Fintype.ofFinite be an instance?

[Kyle Miller]

We definitely don't want Fintype.ofFinite to be a global instance, but inside of proofs you should be able to write have := Fintype.ofFinite rather than doing it per-type.

[Peter Nelson]

It looks like that doesn't always work; if you remove the V on line 227 of Acyclic.lean in the above PR, it breaks two lines after. (I unfortunately don't have the time to minimize this right now)

[Yury G. Kudryashov]

Kyle Miller said:

We definitely don't want Fintype.ofFinite to be a global instance, but inside of proofs you should be able to write have := Fintype.ofFinite rather than doing it per-type.

I guess, you need at least one have per universe.

[Eric Wieser]

Yes, test-case:

import Mathlib
example {α β : Type*} [Finite α] [Finite β] : True := by
  have := Fintype.ofFinite.{u_1}
  have := Fintype.ofFinite.{u_2}
  have : Fintype.card (α × β) = Fintype.card α * Fintype.card β := sorry
  trivial

[Peter Nelson]

Here is a somewhat minimized example where the type is needed, with just one universe in play.

lemma bar (G : SimpleGraph V) [Fintype G.edgeSet] : G.edgeFinset.card = 5 := sorry

lemma foo {V : Type*} {G : SimpleGraph V} [Finite V] : Nat.card G.edgeSet = 5 := by
  have := Fintype.ofFinite V
  classical
  simpa using bar G
  -- succeeds

lemma foo' {V : Type*} {G : SimpleGraph V} [Finite V] : Nat.card G.edgeSet = 5 := by
  have := Fintype.ofFinite
  classical
  simpa using bar G
  /- Fails
    type mismatch, term
      bar G
    after simplification has type
      Fintype.card ↑G.edgeSet = 5 : Prop
    but is expected to have type
      Nat.card ↑G.edgeSet = 5 : Prop -/

[Eric Wieser]

@loogle Nat.card, Fintype.card

[loogle]

:search: Fintype.card_eq_nat_card, Nat.card_eq_fintype_card, and 13 more

[Peter Nelson]

I don't understand the point of this loogle.

[Eric Wieser]

Sorry, I wanted to check if there was a simp lemma to go from the first to the second

[Eric Wieser]

And indeed there is, so its strange that it isn't firing

[Peter Nelson]

Yes - and it fires just fine in the proof of foo.

[Eric Wieser]

have := Fintype.ofFinite.{u_1} suffices

[Peter Nelson]

Would streamlining this kind of thing with a tactic be reasonable? So the tactic invokes classical, then Fintype.ofFinite.{u} for every universe in the context?

[Yury G. Kudryashov]

What about universes like max u v + 1?

[Kyle Miller]

Maybe we could make a finite tactic instead that does what classical does, but locally adds the instance (with general universe parameter)

[Shreyas Srinivas]

what is the cardinality function for Finite?

[Peter Nelson]

Nat.card - it takes a junk value of zero for infinite types.

[Shreyas Srinivas]

Is there an encard?

[Shreyas Srinivas]

I am dealing with finite structures where maximum cardinality of some type being 0 is not very helpful

[Peter Nelson]

Yes, in the form of docs#ENat.card and docs#Set.encard

[Shreyas Srinivas]

Ah okay. That's very helpful. Thanks

[Peter Nelson]

I use it a lot! Also, the new enat_to_nat tactic is wonderful for calculations.

[Peter Nelson]

Kyle Miller said:

Maybe we could make a finite tactic instead that does what classical does, but locally adds the instance (with general universe parameter)

If this is technically feasible, that would be great for readability.

[Shreyas Srinivas]

For almost all discrete math problems, encard appears to be the natural cardinality function. (for example think graph distance algorithms that initially assign distance infinity to unexplored vertices).

[Shreyas Srinivas]

Moving between Finset and Set is much more painful.

[Kyle Miller]

If this is technically feasible

Yes, take a look at the definition of the classical tactic. There's very little code. You'd just have to replace the part that has Classical.propDecidable

[Peter Nelson]

My matroid repo uses ENat heavily, for exactly this reason.

ENat has a less full API than Nat, and in particular arguments that involve something resembling subtraction are very awkward, but this is made a lot better with enat_to_nat.