rfl better than refl

Stream: general

[Kevin Buzzard]

def S {X Y : Type} (f : X → Y) : X → X → Prop := λ x₁ x₂, f x₁ = f x₂

example {X Y : Type} (f : X → Y) : reflexive (S f) := λ x, rfl -- works
example {X Y : Type} (f : X → Y) : reflexive (S f) := λ x, begin refl end -- fails!

I was surprised that refl fails. It doesn't unfold S?

[Kevin Buzzard]

I am trying to encourage learners away from the unfold tactic and am trying to get them to do the unfolding in their head, because "everything works when you unfold in your head". But refl doesn't? It's like rw -- it needs syntactic equality and I just never noticed this? I'm sure I've used refl to close all sorts of goals before.

[Chris Hughes]

It is surprising. Looking at the definition of refl it seems like it should unfold semireducibles.

[Mario Carneiro]

refl uses the @{refl]attribute. It looks at the head of the expression, assuming it has the form R x x, to find the proof

[Kevin Buzzard]

Oh, so it refuses to unfold because it has a better idea?

[Kevin Buzzard]

It's like "aha, this must be asking for a proof of reflexivity of S, I'll just look it up in my database, oh dear it's not there"

[Mario Carneiro]

more like it figured out the relevant definition, it's S, and it's complaining that this definition doesn't have a @[refl] declaration

[Mario Carneiro]

right