nat.prime and unfreezingI

Stream: new members

[Damiano Testa]

Dear All,

in the example below, Lean complains that p.prime is a frozen local instance and gives the error

failed to revert 'hp', it is a frozen local instance (possible solution: use tactic `unfreezing`
to temporarily reset the set of local instances)
state:
p : ℕ,
hp : nat.prime p,
ap : p = 2
⊢ true

Using unfreezingI, as Lean suggests, works. My question though is why this is needed.

import data.nat.prime

lemma nat.prime.dvd_iff_eq {p : ℕ} (hp : p.prime) (ap : p = 2) : true :=
begin
  cases ap,  -- frozen local instance hp
end

Thanks!

[Damiano Testa]

In particular, rw ap at hp does work and Lean is happy with doing it without unfreezingI.

[Eric Wieser]

Is docs#nat.prime tagged with @[class]?

[Eric Wieser]

Ah, the problem is that docs#irreducible is tagged with @[class], and they're defeq

[Eric Wieser]

How much actually relies on irreducible being a class? Changing it to a structure would make your problem go away

[Eric Rodriguez]

I don't know how necessary this is considering the planned refractor to make nat.prime just be prime

[Eric Rodriguez]

I'm not at a pc but i guess it's worth ctrl-fing \[[^\]*irreducibleto see how much it would break

[Damiano Testa]

Eric, thanks! This explains it! I stopped at nat.prime not being a class and did not look further.

[Damiano Testa]

Also, I'm not too bothered by this: it is usable as is. I was just puzzled.

[Damiano Testa]

Maybe I still have a question, though. Why does the rewrite work?

[Damiano Testa]

(I'm no longer at my computer, but I seem to remember that subst does not work.)

[Reid Barton]

Damiano Testa said:

Maybe I still have a question, though. Why does the rewrite work?

Just guessing but maybe because the rewrite just creates a new hypothesis hp while using cases reverts it (and then applies the eliminator for eq)

[Damiano Testa]

It's possible, thanks! Anyway, I am going to move on! :smile: