irreducible_def

Stream: mathlib4

[Jireh Loreaux]

Mathport translated an @{irreducible] def to an irreducible_def. Is there a reason to prefer this to the former? I had a bit of trouble with irreducible_def and actually getting Lean to unfold the definition, but presumably I'm missing something.

[Chris Hughes]

irreducible_def foo generates a lemma foo_def which unfolds the definition

[Jireh Loreaux]

okay, so do we prefer irreducible_def over @[irreducible] def for that reason then?

[Gabriel Ebner]

The advantage of irreducible_def is that it also applies to the kernel. @[irreducible] only affects the elaborator.

[Gabriel Ebner]

There were some issues with protected irreducible_def. These are fixed by !4#3395

[Chris Hughes]

Chris Hughes said:

irreducible_def foo generates a lemma foo_def which unfolds the definition

I actually didn't know about this until today, so there are some ported files where I changed an irreducible_def to an @[irreducible] def that should probably be changed back.

[Gabriel Ebner]

Another open issue is that irreducible_def doesn't work with to_additive.

[Chris Hughes]

I think almost everything should be an irreducible_def.

[Patrick Massot]

I think it would be really nice to add a paragraph about irreducible_def to the porting wiki, because I was really puzzled by this too.

[Jireh Loreaux]

I have added a paragraph about this to the #port-guide

[Gabriel Ebner]

Note that #port-wiki doesn't like to the porting wiki. The paragraph is here: https://github.com/leanprover-community/mathlib4/wiki/Porting-wiki#irreducible_def

[Jireh Loreaux]

We have too many port related linkifiers. Fixed.

[Patrick Massot]

Gabriel, I don't want you to think I don't like irreducible_def but the following took me a while to understand in a non-minimized context:

import Mathlib.Tactic.IrreducibleDef

class Foo where
(n : Nat)

class Bar extends Foo where
(h : n = 0)

def x : Foo := {n := 0}

irreducible_def y : Bar := {x with h := sorry}

resulting in error messages like

Scratch.lean:11:0
function expected
  y src✝
Scratch.lean:11:0
tactic 'rewrite' failed, did not find instance of the pattern in the target expression
  Wrapper.value✝ wrapped✝
⊢ sorryAx (Sort u_1) true

with a Lean server error on top:

Lean (version 4.0.0-nightly-2023-03-31, commit 742d053a97bd, Release)
Watchdog error: Got `shutdown` request, expected an `exit` notification
Watchdog error: Got `shutdown` request, expected an `exit` notification
[Error - 10:37:00] Connection to server got closed. Server will not be restarted.
[Error - 10:37:00] Stopping server failed
  Message: Pending response rejected since connection got disposed
  Code: -32097
Watchdog error: Got `shutdown` request, expected an `exit` notification
[Error - 21:27:42] Connection to server got closed. Server will not be restarted.
[Error - 21:27:42] Stopping server failed
  Message: Pending response rejected since connection got disposed
  Code: -32097
elan 1.4.2 (4a1b1b918 2022-09-13)
Lean (version 4.0.0-nightly-2023-03-31, commit 742d053a97bd, Release)
Cannot send message to unknown document 'file:///home/pmassot/lean/mathlib4/Mathlib/Algebra/Algebra/Hom.lean':
{"params":{"uri":"file:///home/pmassot/lean/mathlib4/Mathlib/Algebra/Algebra/Hom.lean","sessionId":"10413944821563192556"},"method":"$/lean/rpc/keepAlive","jsonrpc":"2.0"}

[Patrick Massot]

Probably the server error has nothing to do with this, but it happens quite often tonight.

[Patrick Massot]

Oh actually it has nothing to do with sorry either. It also fails when using an actual proof.

[Patrick Massot]

So the new mwe is

import Mathlib.Tactic.IrreducibleDef

class Foo where
(n : Nat)

class Bar extends Foo where
(h : n = 0)

def x : Foo := {n := 0}

irreducible_def y : Bar := {x with h := rfl}

where replacing irreducible_def by def works just fine.

[Gabriel Ebner]

Thank you for the bug report! Here's an even shorter MWE:

import Mathlib.Tactic.IrreducibleDef
irreducible_def y : Nat := let x := 42; x

[Patrick Massot]

Do you want me to open an issue in the mathlib4 repo?

[Gabriel Ebner]

I've already pushed a fixed to the latest irreducible_def refactor !4#3399

[Patrick Massot]

Thanks!

[Patrick Massot]

@Mario Carneiro it would be nice to merge !4#3399 rather soon if you are happy with it since it blocks progress.