not a rfl-lemma, even though marked as rfl

Stream: general

[Eric Wieser]

In #8783 I have a lemma that produces the error message

not a rfl-lemma, even though marked as rfl

If I change the proof from := rfl to := by exact rfl the error goes away. Is this a bug?

[Eric Wieser]

Or does "a rfl-lemma" have more meaning behind it than just "has a proof of rfl"

[Eric Rodriguez]

relevant c++ code: https://github.com/leanprover-community/lean/blob/ef197a6a83aa1a157a941c72151a09ce807f2867/src/library/tactic/simp_lemmas.cpp#L810

[Eric Rodriguez]

my guess would be that this code isn't expecting a let in the definition, but I'm then not sure why the by exact hack fixes it

[Eric Wieser]

I couldn't work out how to eliminate the let here without a very large amount of verbosity, since I'm having to fight typeclass inference

[Eric Wieser]

I pushed a commit on that PR to remove the offending lemma, but the behavior's still visible in an old commit if anyone is interested.

[Eric Wieser]

This is enough to repro it:

lemma foo : let x := 1 in x = 1 := rfl

[Eric Rodriguez]

yeah, so if I just run this sort of stuff in my local debug lean, there's actually an assertion violation of is_eq(type, lhs, rhs), so i'd assume this is_eq doesn't ‹_›-reduce, where ‹_› is whatever greek letter is used for let binder reductions

[Eric Rodriguez]

so in util.cpp:104, is_app_of doesn't unfold past let binders, which then cascades to is_eq returning false

[Eric Rodriguez]

meanwhile, the by exact rfl doesn't go through the same check (my breakpoint at is_rfl_lemma didn't pop), so it's checked for being rfl somewhere else

[Eric Rodriguez]

so there's two different ways of checking if something is rfl, it seems

[Eric Rodriguez]

I don't know who to CC but this shouldn't be a big fix, if you know where the other rfl check is

[Floris van Doorn]

This sounds like it shouldn't be a refl-lemma, and we should just add a check if (is_let(type)) return false; to the function.
simp isn't able to look under let's anyway (and I think _refl_lemma is used by dsimp?):

def bar := 1
@[simp] lemma foo : let x := 1 in bar = x := by exact rfl
example : bar = 1 := by simp

I believe the by exact rfl hack work since the code for _refl_lemma checks that the proof is actually just rfl or eq.refl _, not produced by a tactic.

def bar := 1
lemma baz : bar = 1 := by refl
#print baz -- not a _refl_lemma