How to unfold a coercion?

Stream: new members

[Darij Grinberg]

I am having a goal that contains both ofNat and ↑ in it. From what I understand, the latter is just an alias of the former, but this suffices to confuse rw. I can use erw to break through this wall, but is there a way to just replace ↑ throughout the goal?

[Kenny Lau]

@Darij Grinberg they aren't literally the same, otherwise you would see the same result; the solution is that usually there are simp lemmas to convert a non-standard form to a standard form

[Darij Grinberg]

how can I find the one that unfolds a coercion? I'm not sure it's even a lemma; looks like it is the definition of the ↑ here

[Kenny Lau]

which ofNat are you looking at?

[Kenny Lau]

#mwe

[Kenny Lau]

if you don't have mwe (which you should, try extract_goal), can you at least post a screenshot after you click into the ofNat that appears in the goal

[Darij Grinberg]

Int.ofNat

[Darij Grinberg]

image.png

[Darij Grinberg]

the arrow is @Nat.cast ℤ instNatCastInt n : ℤ
the ofNat is ofNat : ℕ → ℤ

[Kenny Lau]

@Darij Grinberg the simmp lemma is Int.ofNat_eq_coe which is already tagged with simp

[Darij Grinberg]

ah thak you!

[Kenny Lau]

Darij Grinberg said:

how can I find the one that unfolds a coercion?

this is the wrong question, we keep getting into an #xy problem, you shouldn't "unfold coercion", the correct thing is to do it the other way

[Darij Grinberg]

oh lol, i see i can finish the proof with simp at that point

[Kenny Lau]

it's a beginners' trap to try to unfold everything, that is rarely the best way to do things

[Darij Grinberg]

i don't mind the coercion per se, i mind having two different forms of it :)

[Darij Grinberg]

which one should i be using in definitions?

[Kenny Lau]

what do you mean two different forms

[Darij Grinberg]

↑ and ofNat

[Kenny Lau]

and what do you mean use in definition

[Kenny Lau]

coercion only refers to the uparrow

[Kenny Lau]

Int.ofNat is just another random function from Nat to Int

[Darij Grinberg]

i have
def intfac (n : ℕ) := Int.ofNat (factorial n)
and i'm wondering if i should replace it by
def intfac (n : ℕ) := ↑(factorial n)

[Kenny Lau]

you shouldn't have it in the first place, what's the point of it

[Darij Grinberg]

i guess not much now that the arrow is so short

[Kenny Lau]

no, you should never type the arrow, that's another beginner's trap (some people have disagreed with me on this point, but I stand by it)

[Darij Grinberg]

OK. what is it i should be doing? I want n! as an integer, not as a nonnegative integer

[Kenny Lau]

the correct way is (factorial n : ℤ) (and not a separate definition)

[Darij Grinberg]

ah!

[Darij Grinberg]

yeah i guess it's pretty pointless given how simple this is

[Kenny Lau]

and btw n.factorial is more preferred

[Darij Grinberg]

because it's closer to the math notation?

[Kenny Lau]

no, dot notation is just preferred

[Aaron Liu]

Kenny Lau said:

no, dot notation is just preferred

how come I've never heard of this

[Kenny Lau]

sorry i meant I personally prefer it, I should have been clear

[Darij Grinberg]

:joy: