RFC: nat.card as a simp normal form

Stream: general

[Yury G. Kudryashov]

Hi, what do you think about the following change?

• We define enat.card and redefine nat.card without cardinals, see here.
• Optional: we prove fin.equiv_iff_eq in another way to avoid dependency on finset/fintype.
• We make nat.card, not fintype.card, the simp-normal form.

Pros

• No non-Prop argument in card.
• We can define card without theory about list.perm, finset etc.
• Don't duplicate API (currently we state many lemmas both for fintype.card and nat.card).

Cons

• Loss of computability.

[Kevin Buzzard]

Some people would regard loss of computability as another pro!

[Yury G. Kudryashov]

I don't know if this can cause troubles for meta programming.

[Yury G. Kudryashov]

Here is a proof that works in data.fin.basic, right after pred_inj:

lemma nonempty_embedding_iff : nonempty (fin n ↪ fin m) ↔ n ≤ m :=
begin
  refine ⟨λ h, _, λ h, ⟨(cast_le h).to_embedding⟩⟩,
  induction n with n ihn generalizing m, { exact m.zero_le },
  cases h with e,
  rcases exists_eq_succ_of_ne_zero (pos_iff_nonempty.2 (nonempty.map e infer_instance)).ne'
    with ⟨m, rfl⟩,
  refine nat.succ_le_succ (ihn ⟨_⟩),
  refine ⟨λ i, (e.set_value 0 0 i.succ).pred (e.set_value_ne i.succ_ne_zero _), λ i j h, _⟩,
  simpa only [pred_inj, embedding_like.apply_eq_iff_eq, succ_inj] using h,
end

lemma equiv_iff_eq : nonempty (fin n ≃ fin m) ↔ n = m :=
⟨λ ⟨e⟩, le_antisymm (nonempty_embedding_iff.1 ⟨e⟩) (nonempty_embedding_iff.1 ⟨e.symm⟩),
  λ h, h ▸ ⟨equiv.refl _⟩⟩

[Yury G. Kudryashov]

It relies on this addition to logic.embedding.basic:

theorem set_value_ne {α β} (f : α ↪ β) {a a' : α} (h : a' ≠ a) (b : β) [∀ a', decidable (a' = a)]
  [∀ a', decidable (f a' = b)] : set_value f a b a' ≠ b :=
((set_value f a b).injective.ne_iff' $ set_value_eq f a b).2 h

[Kyle Miller]

Yury G. Kudryashov said:

• We make nat.card, not fintype.card, the simp-normal form.

I worry about this one -- sometimes one can use the fintype instance to get a specific convenient finset where it's easy to get the cardinality. That said, I think it should be fine if we leave the fintype.card ==> nat.card lemma non-simp (that way it's opt-in).

I agree with preferring nat.card over fintype.card for whenever you don't need an actual fintype instance.

[Kyle Miller]

It also makes sense for enat.card and nat.card to be defined only in terms of fin and equiv, at least for sake of removing dependencies for the basic notion of finite cardinalities. (Having #ₙ α notation is a nice idea too.)

[Yaël Dillies]

I don't see much point in removing dependencies for the sake of removing dependencies. From what I understand, this will mostly end up duplicating API.

[Yury G. Kudryashov]

@Yaël Dillies We need to prove that the projection from cardinal to enat is a ring homomorphism. We can either prove it directly (by a choice analysis) or by using this trick.

[Yury G. Kudryashov]

So, there is not much code duplication here.

[Yury G. Kudryashov]

@Kyle Miller If we have a nice fintype structure, then we should add a lemma about nat.card _ = _ that rewrites to fintype.card.

[Yury G. Kudryashov]

But nat.card ((s : finset _) : set _) should be simplified to finset.card s.

[Yury G. Kudryashov]

So, we can completely remove fintype.card (and use nat.card instead) and use finset.univ.card whenever you want a specific fintype instance.

[Kyle Miller]

I wouldn't go as far as removing fintype.card, since it can be useful for programming (though admittedly types with specific enumerations are more useful programming wise). My comment was mainly about just avoiding having a fintype.card ==> nat.card simp lemma since that strips away potentially useful information (the specific fintype instance in the term), and there's no need to normalize one to the other.

[Yaël Dillies]

Yury G. Kudryashov said:

So, we can completely remove fintype.card (and use nat.card instead) and use finset.univ.card whenever you want a specific fintype instance.

Unfortunately that would be much longer to type because Lean can't infer the type of finset.univ. If anything, making fintype.card an abbreviation sounds like a much better way of achieving this specific goal.

[Yury G. Kudryashov]

Kyle Miller said:

I wouldn't go as far as removing fintype.card, since it can be useful for programming (though admittedly types with specific enumerations are more useful programming wise). My comment was mainly about just avoiding having a fintype.card ==> nat.card simp lemma since that strips away potentially useful information (the specific fintype instance in the term), and there's no need to normalize one to the other.

If we don't normalize, then we need lemmas about both nat.card and fintype.card everywhere.

[Junyan Xu]

Simplifying fintype.card to nat.card is like simplifying docs#category_theory.groupoid.inv to docs#category_theory.inv (#16624, exactly for the purpose of reusing simp lemmas for category_theory.inv) but surely has a much larger impact. I guess I'm in favor of the change if you could make mathlib compile :)

[Kyle Miller]

@Yury G. Kudryashov I'm not sure what assumptions you're making to reach this conclusion.

I'll say my concern in a different way: one should be able to decide whether to simp with fintype.card X ==> nat.card X or with fintype.card X = finset.univ.card. This is a nonconfluence junction unless you turn all finset.card into nat.card as well. I doubt we want to do that, so it should be left to the user.

We don't need a rich set of simp lemmas for fintype.card since if someone is using it for whatever reason, to prove things about it the first step should be to decide whether it's better to go via nat.card or finset.card.

[Kyle Miller]

Somewhat relatedly, I think it would be nice additionally having a set.ncard s := nat.card s specifically to preserve that the argument is a set. I've run into a number of situations where there are well-meaning simp lemmas that convert fintype.card s into something involving an equivalent subtype, which isn't good because the next steps would be rewriting types, one of those evils in type theory. Keeping things in the language of set means congr and friends are more likely to work.

[Yury G. Kudryashov]

Rewriting types is not that bad if you don't have a [fintype s] assumption nearby.

[Peter Nelson]

Kyle Miller said:

Somewhat relatedly, I think it would be nice additionally having a set.ncard s := nat.card s specifically to preserve that the argument is a set. I've run into a number of situations where there are well-meaning simp lemmas that convert fintype.card s into something involving an equivalent subtype, which isn't good because the next steps would be rewriting types, one of those evils in type theory. Keeping things in the language of set means congr and friends are more likely to work.

Would there be support for a PR that adds this? That is, a new file defining set.ncard that contains more or less the same lemmas as data.finset.card, in noncomputable forms with each (s : finset a) argument being replaced with (s : set a) as well as [finite s] where needed.

I'm doing stuff involving cardinality calculations for complicated sets where I want the full set API as well as cardinality, and the instance mismatch issues associated with to_finset are getting really annoying. This would be a solution. It's not even very much work.

[Yury G. Kudryashov]

Looks like a good idea to me. I postponed my refactor till after the porting to mathlib4 to avoid doing it twice but yours suggestion adds a leaf file instead of making a refactor.

[Eric Wieser]

Reiterating my comment from the PR (#18576) it seem a bit weird to add a shorthand for nat.card (coe_sort s), but then have the shorthand use finite (coe_sort s) instead of the correspondings.finite shorthand

[Peter Nelson]

Thanks for the comments!

At @Yury G. Kudryashov 's suggestion, I'm refactoring the PR to use (hs : s.finite) instead of [finite s],
with auto_params to make things work smoothly in the case where s is a set in a finite type.
This is working ok, but it seems like it gives some annoying behaviour while writing proofs that
use the auto_param lemmas. Here is what I mean.

import data.finite.card

variables {α : Type*} {s t : set α}

open set

/-- A tactic that finds a `t.finite` term for a set `t` in a `finite` type. -/
meta def to_finite_tac : tactic unit := `[apply set.to_finite]

/-- Cardinality -/
noncomputable def set.ncard (s : set α) := nat.card s


@[simp] lemma ncard_eq_zero (hs : s.finite . to_finite_tac) :
  s.ncard = 0 ↔ s = ∅ :=
sorry

example (ht : t.finite) (hst : s ⊆ t) (hs : s.ncard = 0) : s = ∅  :=
begin
  -- proving this lemma using the one above. I don't know that s is finite yet, but I'll
  -- prove that in a minute; in the meantime I'll state the lemma I need.
  have := ncard_eq_zero,
  /- Won't tell me what the lemma actually says until I supply the parameter; instead
   gives me a red underline and uninformative error message

    tactic failed, there are unsolved goals
    state:
    α : Type u_1,
    s t : set α,
    ht : t.finite,
    hst : s ⊆ t,
    hs : s.ncard = 0
    ⊢ ?m_2.finite

    This is fixed by appending an `@`, but then it is quite hard to read the lemma signature
    because of all the `auto_param` boilerplate. -/
end

Is this just an inherent thing with auto_param, or is there a good way to handle this?

[Yury G. Kudryashov]

I don't know.

[Yury G. Kudryashov]

In this case, you'll have to use ncard_eq_zero (ht.subset hst) anyway.

[Eric Wieser]

have := λ h, ncard_eq_zero h should work as you intend