irreducible

Stream: general

[Sebastien Gouezel]

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]

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:

1-3 all make use of the equation lemmas that are automatically generated when you add a definition (check out #print prefix n). This works no matter whether the reduction is definitional is or not. (You can also add your own equation lemmas using docs#environment.add_eqn_lemma!)
4 replaces a constant by its definition, what else did you expect when calling delta n.

[Sebastien Gouezel]

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]

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]

unfold is implemented using simp.
dunfold is implemented using dsimp.
delta is implemented "by hand".

[Mario Carneiro]

for completeness:

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

[Mario Carneiro]

is there unsafe_exact?

[Mario Carneiro]

the unsafe_change proof still sticks an id in the term