## Stream: general

### Topic: rfl better than refl

#### Kevin Buzzard (Jul 19 2019 at 10:42):

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 (Jul 19 2019 at 10:49):

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 (Jul 19 2019 at 10:51):

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

#### Mario Carneiro (Jul 19 2019 at 10:56):

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 (Jul 19 2019 at 10:56):

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

#### Kevin Buzzard (Jul 19 2019 at 10:57):

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 (Jul 19 2019 at 10:57):

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 (Jul 19 2019 at 10:57):

right

Last updated: Dec 20 2023 at 11:08 UTC