leanprover-community / leanprover-community/mathlib4

Refactor/define noncomputable `*card`s

Open
#9,794 0 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

Dominant language
Lean
Stars
4.1k
Forks
1.7k
No merged PRs in 30d

Description

Some of these items depend on each other, some don't.

  • Define Cardinal.toENat and a coercion Cardinal.ofENat, #9792.
  • Move Cardinal.toNat to a separate file, #10466.
  • Redefine Cardinal.toNat as the composition of Cardinal.toENat and ENat.toNat, #10472.
  • Define ENat.card without using Cardinals. E.g., 
    protected noncomputable def ENat.card (α : Sort*) : ℕ∞ :=
if h : ∃ n, Nonempty (α ≃ Fin n) then h.some else ⊤
  • Prove basic properties of the new definition.
  • Prove that ENat.card α = Cardinal.toENat (Cardinal.mk α).
  • Redefine Nat.card α as ENat.toNat (ENat.card α)
  • Redefine Set.encard and Set.ncard in terms of the new ENat.card and Nat.card. RFC: definitions or abbrevs?

Contributor guide

Open the contributing guide

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Research direction

Start by reviewing the existing definitions of ENat.card, Cardinal.toENat, Nat.card, Set.encard, and Set.ncard named in the checklist. Work through the requested basic properties and the equality with Cardinal.mk, then confirm the cardinality definitions no longer depend on Cardinal as specified; resolve the definitions-versus-abbrevs RFC for Set.encard and Set.ncard.

Written by the indexing model from the issue text.

Assessment

Domain
tooling
Issue type
Refactor
Difficulty
5/5
Estimated time
Over a week
Activity status
Stale
Clarity
Mostly clear
Newbie friendliness
35/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.