Zulip Chat Archive

Stream: general

Topic: not a rfl-lemma, even though marked as rfl


Eric Wieser (Aug 20 2021 at 21:53):

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 (Aug 20 2021 at 21:54):

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

Eric Rodriguez (Aug 20 2021 at 21:58):

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

Eric Rodriguez (Aug 20 2021 at 21:59):

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 (Aug 20 2021 at 22:10):

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 (Aug 21 2021 at 09:22):

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 (Aug 21 2021 at 09:23):

This is enough to repro it:

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

Eric Rodriguez (Aug 21 2021 at 09:31):

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 (Aug 21 2021 at 09:39):

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

Eric Rodriguez (Aug 21 2021 at 09:41):

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 (Aug 21 2021 at 09:41):

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

Eric Rodriguez (Aug 21 2021 at 09:41):

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 (Aug 21 2021 at 18:48):

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

Last updated: Dec 20 2023 at 11:08 UTC