# Zulip Chat Archive

## Stream: general

### Topic: irreducible

#### Sebastien Gouezel (Nov 18 2020 at 12:27):

On my way to #5035 (making `continuous`

irreducible), I was surprised that `irreducible`

is not as irreducible as I thought it was (so in the end I made it a structure, to avoid this kind of issues). Exercise: in the next lemmas, guess which proof(s?) succeed, if any, and which fail:

```
def n : nat := 37
attribute [irreducible] n
lemma foo0 : n = 37 := by refl
lemma foo1 : n = 37 := by rw n
lemma foo2 : n = 37 := by simp [n]
lemma foo3 : n = 37 := by unfold n
lemma foo4 : n = 37 := by { delta n, refl }
```

#### Gabriel Ebner (Nov 18 2020 at 12:47):

Since people are apparently surprised by this behavior: `irreducible`

only affects definitional equality, i.e. the unification when Lean figures out if two types are the same. (And it doesn't affect the kernel either: you can still write a tactic that produces a `rfl`

proof; check out docs#tactic.unsafe_change.)

:octopus:

#### Sebastien Gouezel (Nov 18 2020 at 13:10):

I thought one of `unfold`

or `delta`

wasn't relying on the equation lemmas, but instead used the bare definition (and so should have been stuck by the irreducible attribute). Clearly, I was wrong! All proofs work fine, except for the `rfl`

one.

#### Kevin Buzzard (Nov 18 2020 at 13:15):

I thought unfold was basically `simp only [equation lemmas]`

and delta was "replace this name by its definition". I "knew" that `irreducible`

would stop at least one from working though ;-)

#### Gabriel Ebner (Nov 18 2020 at 13:16):

`unfold`

is implemented using `simp`

.

`dunfold`

is implemented using `dsimp`

.

`delta`

is implemented "by hand".

#### Mario Carneiro (Nov 18 2020 at 13:49):

for completeness:

```
lemma foo5 : n = 37 := by { tactic.unsafe_change `(37 = 37), refl }
```

#### Mario Carneiro (Nov 18 2020 at 13:51):

is there `unsafe_exact`

?

#### Mario Carneiro (Nov 18 2020 at 13:51):

the `unsafe_change`

proof still sticks an `id`

in the term

Last updated: May 08 2021 at 04:14 UTC