Why simp doesn't simplify projection?

Stream: lean4

[Pavel Klimov]

Here is not minimal but small working example:

def qwe : Nat → Nat × Nat := (fun x =>
  let a := x + 1
  (if a > 10 then a + 10 else a * 5, a - 2))

example : (fun x => (qwe x).2) = fun x => x - 1 := by
  unfold qwe
  simp
  rfl

Here simp failing. For some reason simp only is working. But I want to avoid zeta reduction. But simp -zeta only doesn't work. Also any my attempt to use Prod.snd failed. I also tried to write theorem:

theorem Prod_snd {α β : Type} : ∀ (a : α) (b : β), (a, b).snd = b := by
  intro a b
  rfl

and use this theorem with no success. Any explanation?

[Henrik Böving]

What do you mean by "simp failing"? simp does solve this goal right away and you get an error on rfl because there are no more goals to be solved.

[Pavel Klimov]

Henrik Böving писал/а:

What do you mean by "simp failing"? simp does solve this goal right away and you get an error on rfl because there are no more goals to be solved.

I mean this:

`simp` made no progress

[Henrik Böving]

This doesn't happen on the versions available on live.lean-lang.org.

[Henrik Böving]

What's the output of #version for you?

[Pavel Klimov]

Hmm! In clean file simp does stuff. Interesting! Looks like definition of simproc using simproc is adding it into simp by default? Is there a way to avoid adding it, and use manually?

[Pavel Klimov]

If I use simp -zeta [-mySimProc] where mySimProc is my custom simproc, it works as I wanted. Is there a way to not add simproc into default list?

[Pavel Klimov]

Oh, sorry, even though it's not failing, it's still not reducing .2 projection :frown: .

[Bhavik Mehta]

Pavel Klimov said:

Is there a way to avoid adding it, and use manually?

Change the simproc to simproc_decl

[Filippo A. E. Nuccio]

Bhavik Mehta said:

Pavel Klimov said:

Is there a way to avoid adding it, and use manually?

Change the simproc to simproc_decl

Can you elaborate on what this is?

[Bhavik Mehta]

In brief, simproc = simproc_decl but also turn it on by default

[Filippo A. E. Nuccio]

As opposed to?

[Robin Arnez]

Well, simproc_decl is a raw simplification procedure declaration that you can refer to in simp calls and simproc is like simproc_decl + @[simp], i.e. it is a simplification procedure that is used by default in simp [...] calls (although not in simp only calls).

[Bhavik Mehta]

simproc_decl will make the simproc for you to use later in simp calls (in the same way that lemma makes a lemma for you), but simproc will make the simproc, and also mark it @[simp] (in the same way that @[simp] lemma does)