regression of `exact?`

Stream: general

[Asei Inoue]

in v4.26.0 this code suggest exact h1

example (P : Prop) (h1 : P) (h2 : P) : P := by
  exact? using h1

but in v4.27.0-rc1 it suggests exact ((fun a => h1) ∘ fun a => P) P

[Asei Inoue]

this suggestion is too much complicated...

[Ruben Van de Velde]

Probably this is due to the "significant changes to the behaviour of exact? and apply?" that Kim Morrison mentioned. Do you want to file an issue?

[Damiano Testa]

With exact? +all using h1 you do get more options.

[Asei Inoue]

I want to file an issue

[Damiano Testa]

Although the closest you get is id h1.

[Damiano Testa]

((fun a => h1) ∘ fun a => P) P -- the terms that look reasonable to computers...

[Ruben Van de Velde]

AI will save us

[Asei Inoue]

another example:

example (P Q : Prop) (h : P → Q) (hP : P) : Q := by
  exact? -- suggest `exact (h ∘ fun a => hP) P` instead of `exact h hP`

[Kim Morrison]

@Asei Inoue, this is not what exact? is for. If you want solutions like those use try? or show_term solve_by_elim.

[Nick_adfor]

Asei Inoue said:

this suggestion is too much complicated...

Different versions recommend different fixes without clarifying why a particular one is the default. When you update, the old default might break, forcing you to find a new fix through a new "exact?". It's mostly based on experience—I don't have a specific example, as it's just something that happens occasionally.