Zulip Chat Archive

Stream: mathlib4

Topic: enat

Chris Hughes (Jan 13 2023 at 11:20):

ENat is difficult to port right now because it's definition is being unfolded. I think some backported fix is needed. I think the best thing here is to just get rid of it and use WithTop Nat directly rather than making a structure. The only reason we didn't do that initially was because Mario wanted to use roption (now Part), but we don't do that anymore. Maybe WithTop didn't even exist back then, I'm not sure.

Yaël Dillies (Jan 13 2023 at 11:25):

Yeah, sounds reasonable.

Kevin Buzzard (Jan 13 2023 at 11:29):

Should WithTop Nat be a one field structure though? An inductive type defined the same way as Option? Should there be a backport of any of this?

Yaël Dillies (Jan 13 2023 at 11:31):

These fixes are hard to backport because we have more defeqs in Lean 4.

Eric Wieser (Jan 13 2023 at 11:41):

It would be nice if we had an @[almost_irreducible] attribute that makes definitions irreducible, but paired with a (almost_irreducible.unfold (x : X) : Y) function that unifies X with Y unfolding almost_irreducibles that might appear within X and Y

Eric Wieser (Jan 13 2023 at 11:42):

@Chris Hughes, can you give an example of where it ends up unfolded?

Chris Hughes (Jan 13 2023 at 11:43):

A coercion ends up using WithTop.some even though the type ascribed is ENat.

Eric Wieser (Jan 13 2023 at 11:43):

Can you link to the line where that happens?

Yaël Dillies (Jan 13 2023 at 11:46):

But why do we care about ENat being a definition? We use it in exactly the same way as WithTop Nat, right?

Chris Hughes (Jan 13 2023 at 11:46):

line 101 Sorry, had to take some time to find it

Chris Hughes (Jan 13 2023 at 11:46):

Yaël Dillies said:

But why do we care about ENat being a definition? We use it in exactly the same way as WithTop Nat, right?

Exactly, I propose just getting rid of it and using WithTop Nat

Eric Wieser (Jan 13 2023 at 11:47):

I'm not opposed to that, but I want to work out what causes the unfolding

Eric Wieser (Jan 13 2023 at 11:47):

@Arthur Paulino, when I run lake exe cache get on this PR (https://github.com/leanprover-community/mathlib4/pull/1514), I get

$ lake exe cache get
uncaught exception: no such file or directory (error code: 2)
  file: ./Mathlib/Data/Enat/Basic.lean

Chris Hughes (Jan 13 2023 at 11:47):

Sorry, I see the problem. It uses the theorem WithTop.recTopCoe

Chris Hughes (Jan 13 2023 at 11:48):

Eric Wieser said:

Arthur Paulino, when I run lake exe cache get on this PR (https://github.com/leanprover-community/mathlib4/pull/1514), I get

$ lake exe cache get
uncaught exception: no such file or directory (error code: 2)
  file: ./Mathlib/Data/Enat/Basic.lean

I just fixed it, it's to do with Enat vs ENat in the file name

Eric Wieser (Jan 13 2023 at 11:50):

Ah, so the unwanted unfolding didn't happen in a statement, but in a proof where you asked it to be unfolded explicitly

Eric Wieser (Jan 13 2023 at 11:50):

That sounds like working as intended to me

Chris Hughes (Jan 14 2023 at 14:51):

I made a backporting PR for this https://github.com/leanprover-community/mathlib/pull/18173

Violeta Hernández (Jan 19 2023 at 23:31):

Won't be missing this myself :stuck_out_tongue:

Last updated: Dec 20 2023 at 11:08 UTC