Defeq abuse with ENat

Stream: mathlib4

[Daniel Weber]

Using functions like docs#WithTop.untop' and docs#WithTop.map with docs#ENat is defeq abuse, and causes them to simp badly, as ENat uses Nat.cast instead of WithTop.some. How should that be resolved? Should we add ENat.toWithTop and ENat.ofWithTop equivalences and use them? Should we copy needed functions from WithTop to ENat? Some other approach?

[Daniel Weber]

Would it be possible to add WithTop Nat = ENat as a simp lemma?

[Violeta Hernández]

I don't see why you'd ever want to use the former if you have the latter available

[Violeta Hernández]

So I vote yes

[Violeta Hernández]

Since this is def-eq simp should have no trouble doing the replacement

[Daniel Weber]

I made #18782, although I'm not sure how to interpret the benchmark

[Damiano Testa]

In case it is helpful, the bench summary bot did not post anything since there were no entries that differed by at least 10^9 instructions.

[Damiano Testa]

(Right now, the action fails and posts nothing in this case, but it could be changed to posting what I said above instead!)

[Daniel Weber]

I closed it because after trying to use it for a bit I don't think it helps with defeq abuse. I think I'm leaning more towards ENat.toWithTop and ENat.ofWithTop now

[Eric Wieser]

Daniel Weber said:

Would it be possible to add WithTop Nat = ENat as a simp lemma?

Unless docs#ENat is reducible, this doesn't seem like a good idea to me

[Daniel Weber]

Yes, I agree. I tried making it reducible, but it had some weird failure

[Daniel Weber]

/poll How to use WithTop functions on ENat?
Add toWithTop and ofWithTop functions
Copy the appropriate theorems/definition for ENat when needed
Make ENat abbrev

[Daniel Weber]

I made #19149 for map. A potential problem with this is that map needs three versions: Nat -> Nat, Nat -> α, α -> Nat. This PR has the the second of those

[Daniel Weber]

This passes CI now, but I really dislike the duplication

[Daniel Weber]

#19164 implements the first approach, of adding toWithTop and ofWithTop

[Yaël Dillies]

Why don't we make ENat an abbrev? It really is semantically the same as WithTop Nat

[Daniel Weber]

Daniel Weber said:

Yes, I agree. I tried making it reducible, but it had some weird failure

I tried that, but it had failures I didn't understand how to fix

[Yaël Dillies]

Aha, do you have some logs I can look at?

[Daniel Weber]

I'm not at home for a week and I don't think I published the branch to GitHub, so unfortunately no

[Yaël Dillies]

Ah that's okay, I can wait