toNat

Stream: mathlib4

[Yury G. Kudryashov]

TIL that we have docs#toNat that is

• in the root namespace
• abuses defeq between Set X and X -> Prop in all lemmas.

What should I do about it?

[Eric Wieser]

The defeq fix is easy, right?

[Yury G. Kudryashov]

I can fix it to operate on predicates, or I can change all the lemmas to use fun x => x \in s

[Yury G. Kudryashov]

I don't know which one makes more sense in this context.

[Eric Wieser]

Are there defeq abuses in the callers, or just the implementation?

[Eric Wieser]

To me

def toNat (s : Set α) : Set ℕ :=
  (Encodable.decode · |>.getD default) ⁻¹' s

is the obvious correction

[Yury G. Kudryashov]

The next several lemmas abuse defeq because they feed sets to docs#ManyOneReducible

[Yury G. Kudryashov]

The file is authored by @Minchao Wu and @Mario Carneiro and IMHO lacks a useful module docstring.

[Yury G. Kudryashov]

BTW, all the docs talk about sets. Should I redefine ManyOneReducible to take sets instead?

[Yury G. Kudryashov]

@Mario Carneiro Should I change toNat and ManyOneReducible to deal with predicates or sets? Also, what would be good less generic name for toNat or a good namespace for it?