Destructuring in function definition

Stream: lean4

[Patrick Massot]

This was probably discussed before but I can’t find it. Is there a reason why fun (⟨x, y⟩ : X × Y) ↦ whatever x y generates fun p ↦ match p with | ⟨x, y⟩ => whatever x y instead of fun p ↦ whatever p.1 p.2?

[Patrick Massot]

Bonus question: does anyone want to have fun writing a simpproc that turns the match version into the other version?

[Aaron Liu]

Patrick Massot said:

Bonus question: does anyone want to have fun writing a simpproc that turns the match version into the other version?

does dsimp only not work?

[Patrick Massot]

It does nothing.

[Aaron Liu]

that's weird, I remember it doing something for me before

[Yury G. Kudryashov]

In my examples simp only simplifies this match. Do you have an #mwe? E.g., this works:

example (f : Nat × Nat → Nat) (hf : f = fun (x, y) => x + y) : f (0, 0) = 0 := by
  simp only at hf
  guard_hyp hf :ₛ f = fun x => x.1 + x.2
  sorry

[Bhavik Mehta]

dsimp only works in this example too

[Patrick Massot]

Sorry about disappearing, I was travelling yesterday. We’re not talking about the same thing. I’m talking about

example : Nat := by
  let g := fun (⟨x, y⟩ : Nat × Nat) ↦ x + y
  simp only at g
  sorry

[Patrick Massot]

The simp only does nothing there.

[Kenny Lau]

example : 0 + 0 = 0 := by simp

example : True := by
  let g : Nat := 0 + 0
  simp at g

but simp doesn't change lets

[Patrick Massot]

I agree, so we need something to fix this issue.

[Kenny Lau]

but my example shows that this isn't about function, this is about the behaviour of simp on let

[Patrick Massot]

I understand, but I think there are not so many cases where you want to use let only to immediately wish dsimp could act on it.

[Yury G. Kudryashov]

I guess, we can have something like simp% and/or dsimp% for these cases.

[Eric Wieser]

It still would be nice to be able to use rw, simp etc on the values of lets, even if indeed it usually isn't useful in polished code.

[Eric Wieser]

I think the answer to Patrick's original question is that fun patterns are intended to be a very simple wrapper around match syntax

[Eric Wieser]

And so without complicating the wrapper, I guess the question is why match p with Prod.mk x y => f x y isn't syntax for f p.1 p.2.