Why is pattern matching sometimes "essential" in Agda?

Question

Why is pattern matching sometimes "essential" in Agda?

I'm taking this out of Programming Language Foundations in Agda.

When not pattern matching, Agda gives doesn't allow refl in the hole:

η-× : ∀ {A B : Set} (w : A × B) → ⟨ proj₁ w , proj₂ w ⟩ ≡ w
η-× x = ?

And it reports this goal and assumptions:

Goal: ⟨ proj₁ x , proj₂ x ⟩ ≡ x
————————————————————————————————————————————————————————————
x : A × B

But Agda can figure out what is going on if I tell it to case split (ctrl-c ctrl-c x Ret)

η-× : ∀ {A B : Set} (w : A × B) → ⟨ proj₁ w , proj₂ w ⟩ ≡ w
η-× ⟨ x , x₁ ⟩ = ?

Goal: ⟨ x , x₁ ⟩ ≡ ⟨ x , x₁ ⟩

Then Agda lets me fill in the hole with refl.

What's going on? How does doing the pattern match give Agda more information?

The PLFA text says:

The pattern matching on the left-hand side is essential, since replacing w by ⟨ x , y ⟩ allows both sides of the propositional equality to simplify to the same term.

but that doesn't say why the pattern match helps the simplification, or when we can expect to see this effect.

Answer 1

The meaning of equality constructed this way can be seen as a proof of existence of two functions: ∀ {A B : Set} (w : A × B) → ⟨ proj₁ w , proj₂ w ⟩ and ∀ {A B : Set} (w : A × B) → w, which must be proven to produce equal output for the same inputs.

In the first case the statement requires a proof that \ w -> ⟨ proj₁ w , proj₂ w ⟩ ≡ \ w -> w. Agda tells you there are no definitional equalities to conclude this from. One could argue that for a single-constructor types it would be possible to work out automatically, but you can see this is not so simple in general.

In the second case, given that pattern matching proves w ≡ ⟨ x , x₁ ⟩, you only need a proof that proj₁ ≡ \ ⟨ x , x₁ ⟩ -> x and proj₂ ≡ \ ⟨ x , x₁ ⟩ -> x₁, which are definitional equalities.