refl doesn't unfold reducible definitions

[kbuzzard]

Prerequisites

• [X ] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
    • Specifically, check out the wishlist, open RFCs, or feature requests.
  • Reduced the issue to a self-contained, reproducible test case.

Description

The reflexivity tactic won't work on definitions which unfold to things tagged with refl.

Steps to Reproduce

example {n : ℕ} : n ≥ n := by refl

Expected behavior: [What you expect to happen]

Success.

Actual behavior: [What actually happens]

"reflexivity tactic failed, target is not a relation application with the expected property."

Reproduces how often: [What percentage of the time does it reproduce?]

100%

Versions

Current nightly on Ubuntu.

Additional Information

A workaround is

@[refl] lemma ge_refl {α : Type} [preorder α] {a : α} : a ≥ a := show a ≤ a, by refl

but rather than adding these lemmas one could encourage refl to unfold ge seeing as it is marked as reducible.

The below script shows that the issue is also there for the symmetry and transitivity tactics

constants α β : Type constant R : α → α → Prop @[refl] constant R_refl : ∀ a : α, R a a @[symm] constant R_symm : ∀ a b : α, R a b → R b a @[trans] constant R_trans : ∀ a b c : α, R a b → R b c → R a c

variables a b c : α

lemma is_R_refl : R a a := by reflexivity lemma is_R_symm (H : R a b) : R b a := by symmetry;assumption lemma is_R_trans (H1 : R a b) (H2 : R b c) : R a c := by transitivity;assumption

@[reducible] def S : α → α → Prop := λ a b, R b a

lemma is_S_refl : S a a := by reflexivity lemma is_S_symm (H : S a b) : S b a := by symmetry;assumption lemma is_S_trans (H1 : S a b) (H2 : S b c) : S a c := by transitivity;assumption

The last three lemmas all fail. Adding "dunfold S;" at the start of the proofs makes them all succeed.

I don't have a good enough understanding of Lean to know whether there are performance issues associated with the suggestion that these tactics do the reducible definitional unfolding, but my experience is that reducible definitional unfolding happens almost everywhere else, so I was surprised to see it not happening here.