Zulip Chat Archive

Stream: general

Topic: irreducible


view this post on Zulip 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 }

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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 ;-)

view this post on Zulip Gabriel Ebner (Nov 18 2020 at 13:16):

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

view this post on Zulip Mario Carneiro (Nov 18 2020 at 13:49):

for completeness:

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

view this post on Zulip Mario Carneiro (Nov 18 2020 at 13:51):

is there unsafe_exact?

view this post on Zulip 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