coercion from PNat to Nat is not reducing

Stream: mathlib4

[David Renshaw]

import Mathlib.Data.PNat.Basic

lemma foo (p : ℕ → Prop) (k' : ℕ) (hk': 0 < k') (hpk' : p k') :
    ∃ k : ℕ+, p k.val := by
  use ⟨k', hk'⟩
  dsimp -- (doesn't do anything!?)
  -- I expect goal to be `p k'` here,
  -- but instead it's `p ↑{ val := k', property := hk' }`
  sorry

[David Renshaw]

How can I get { val := k', property := hk' }.val to reduce to k'? In mathlib3, dsimp worked here.

[Jireh Loreaux]

docs4#PNat.mk_coe ?

[Jireh Loreaux]

I think the problem is that the arrow is PNat.val instead of Subtype.val (but these are defeq)

[David Renshaw]

Yep, rw[PNat.mk_coe] works: https://github.com/dwrensha/math-puzzles-in-lean4/commit/3cae4ff98f250319450f6ff408369f1822df2f15

[David Renshaw]

Thanks!

[David Renshaw]

It's still counterintuitive to me that this doesn't just reduce on its own.

[Jeremy Tan]

@David Renshaw can you formalise a proof of IMO 1988 Q6 (the "Vieta jumping" problem)?

[Eric Wieser]

Jeremy Tan said:

David Renshaw can you formalise a proof of IMO 1988 Q6 (the "Vieta jumping" problem)?

Have you seen https://leanprover-community.github.io/mathlib_docs/imo/imo1988_q6.html?

[Eric Wieser]

Jireh Loreaux said:

docs4#PNat.mk_coe ?

This feels like it should be marked simp, and the porting note is wrong.

[Eric Wieser]

!4#2989