Empty string refl

Stream: lean4

[Scott Viteri]

Lean3: theorem hi : "".data = [] := by refl
Lean4: example : "".data = [] := by ?

[Kevin Buzzard]

example : "".data = [] := rfl -- fails

#eval "".data == [] -- true
#reduce "".data == [] -- aargh

#reduce "".data -- "".1

[Andrew Kent]

Interestingly String and Array seem to behave differently in this regard:

example : #[].data = ([] : List Char) := by rfl -- works

Both are defined in Prelude.lean and have custom efficient C/C++ implementations backing them. Perhaps this difference is related to the comment by Array's definition stating "The Compiler has special support for arrays." and the lack of such a comment for String...? :shrug:

[Daniel Selsam]

This works:

example : (String.mk []).data  = ([] : List Char) := rfl

I think the issue is just that WHNF sees a String literal and doesn't realize it is morally an application of constructor String.mk and so can project.

[Daniel Selsam]

It seems fixable by adding a String-literal case to https://github.com/leanprover/lean4/blob/master/src/Lean/MonadEnv.lean#L58-L62