refine and implicit constructors

Stream: general

[Eric Rodriguez]

it's always made me sad that stuff like this:

example (p q : Prop) : p ∧ q ↔ q ∧ p :=
begin
  refine ⟨λ ⟨hp, hq⟩, ⟨hq, hp⟩, λ ⟨hq, hp⟩, _⟩,
  exact ⟨hp, hq⟩
end

doesn't work. is this a technical limitation? fixable in lean4?

[Floris van Doorn]

Oh, I didn't even know this was an issue. This looks like something that is fixable (but maybe not worth it in Lean 3), without knowing the details.
It's very possible that this issue has rarely been encountered before, because you're combining refine (tactic mode) with the term mode λ ⟨hq, hp⟩, which is then usually written with cases, since you were in tactic mode anyway.

[Yaël Dillies]

Oh really? I thought this was well-known because I literally pester it three times a day.

[Yaël Dillies]

This arbitrary rule has been impressed to the very core of my soul and I always look out for it.