How to prove an equality that can be `#eval`ed?

Stream: general

[Tobias Bucher]

I have a term like function value and #check knows that it is equal to some result. I want to prove my example : function value = result. With Lean 4.12.0, I was able to use rfl, but in Lean 4.13.0-rc1 (#general>✔ `rfl` regression?) it leads to an error:

def dropLastElemIf {α : Type} (pred : α → Bool) : List α → List α
  | [] => []
  | [a] => if pred a then [] else [a]
  | a :: as => a :: dropLastElemIf pred as

def String.mylines (input : String) : List String := dropLastElemIf String.isEmpty (input.splitOn "\n")

#eval "".mylines
example : "".mylines = [] := by rfl

In Lean 4.12.0, it just passes and tells me that "".mylines evaluates to [].
In Lean 4.13.0-rc1 (and later, also in 4.14.0), it tells me that "".mylines evaluates to [] and then fails the proof:

a.lean:9:32: error: tactic 'rfl' failed, the left-hand side
  "".mylines
is not definitionally equal to the right-hand side
  []
⊢ "".mylines = []

How do I prove the result of a term that Lean knows to evaluate using #eval? How do I tell Lean to "just compute it"?

[nrs]

by native_decide works here but it is discouraged, not sure why (anyone has explanations?)

[Kyle Miller]

The difference between versions is that well-founded recursion stopped unfolding by default. You can "unseal" the relevant definition:

unseal String.splitOnAux in
example : "".mylines = [] := by rfl

(I found this by guessing it might be String.splitOn and looked at the definition.)

[Kyle Miller]

Yes, native_decide invokes #eval, and that's exactly the issue, it means you have to trust the compiler, which is fine if you trust it.

[Niels Voss]

I think native_decide adds an extra axiom to your theorem that is disallowed in Mathlib due to its riskiness (you can check axioms with #print axioms your_theorem)

[Tobias Bucher]

Is there a rfl on 1.14.0 that unfolds everything by default? My example can be proven by just unfolding often enough. I'd love to have a solution where I don't have to look up how all the used functions are defined.

I assume rfl on 1.12.0 didn't need extra axioms?

[Kyle Miller]

The point of that axiom @Niels Voss is that it's a way for the kernel to invoke the #eval machinery.

[Kyle Miller]

@Tobias Bucher In neither 1.12.0 nor 1.14.0 does rfl need any extra axioms.

Maybe @Joachim Breitner has suggestions for how to unseal everything.

One trick I know is

example : "".mylines = [] := by decide +kernel

Depending on your version it might still be decide!.

[Kyle Miller]

What this does effectively is skip the elaborator and ask the kernel directly to do rfl.

[Tobias Bucher]

decide! worked for me on Lean 1.14.0.

[Eric Wieser]

Should we just unseal splitOn globally? While making well-founded recursion irreducible by default is probably sensible to avoid accidental performance issues, it feels like we should opt in wherever is convenient.

[Joachim Breitner]

I am under the impression that any well-founded recursive function can easily lead reduction to go astray – or do you have a good reason why this won’t happen with String.splitOn?

[Joachim Breitner]

/--
error: maximum recursion depth has been reached
use `set_option maxRecDepth <num>` to increase limit
use `set_option diagnostics true` to get diagnostic information
-/
#guard_msgs in
unseal String.splitOnAux in
example : "this is a mildly long string so let's see what happens".splitOn "o" = ["this is a mildly l", "ng string s", " let's see what happens"] := by rfl

[Mario Carneiro]

splitOn was not designed for kernel computation. There is a significantly simpler implementation for the kernel

[Mario Carneiro]

Here's a structural recursive implementation of splitOn optimized for call-by-need:

namespace String

def splitOn' (s : String) (sep : String := " ") : List String :=
  match sep.data with
  | [] => [s]
  | sep₁ :: sep => aux sep₁ sep s.data .mk none
where
  aux (sep₁ : Char) (sep : List Char) :
    (s : List Char) → (List Char → String) → Option (String × Char × List Char) → List String
  | [], acc, _ => [acc []]
  | a :: s, acc, none =>
    «match» (aux sep₁ sep s) a sep₁ sep (acc ∘ List.cons a) (acc [])
  | a :: s, acc, some (s', sep₁', sep') =>
    «match» (aux sep₁ sep s) a sep₁' sep' (acc ∘ List.cons a) s'

  «match» (aux : (List Char → String) → Option (String × Char × List Char) → List String)
      (a sep₁ : Char) (sep : List Char) (acc : List Char → String) (s' : String) : List String :=
    if a = sep₁ then
      match sep with
      | b :: sep' => aux acc (some (s', b, sep'))
      | [] => s' :: aux .mk none
    else aux acc none

example : "this is a mildly long string so let's see what happens".splitOn' "o" =
  ["this is a mildly l", "ng string s", " let's see what happens"] := by rfl

[Daniel Weber]

Perhaps the implementation should change to this, and the current implementation could be a @[csimp]?

[Mario Carneiro]

that was my intent with the suggestion

[Mario Carneiro]

although thinking about it now, this might be an example where we have three separate implementations, since the optimal version for equations is not this either

[Mario Carneiro]

so the definition would be kernel-optimized, the @[csimp] lemma points to a compiler-optimized definition, and the @[simp] lemmas point to a reasoning-optimized version

[Tobias Bucher]

Joachim Breitner said:

I am under the impression that any well-founded recursive function can easily lead reduction to go astray – or do you have a good reason why this won’t happen with String.splitOn?

Your example compiles for me in Lean 1.14.0, no error message about maximum recursion depth.

[Joachim Breitner]

Did you include the guard_msgs command when testing? Then no error message means that that error message was produce :-)

In any case, I produced this on live.lean-lang.org, version Lean 4.15.0-rc1

[Kim Morrison]

Mario Carneiro said:

so the definition would be kernel-optimized, the @[csimp] lemma points to a compiler-optimized definition, and the @[simp] lemmas point to a reasoning-optimized version

If I understand correctly, we don't currently have a reasoning-optimized version, is that right?

If so, I suggest we do this in stages:

1. If someone could write the @[csimp] lemma, we can install Mario's splitOn as a the "official" splitOn, with a @[csimp] lemma replacing it with the current version.
2. I will happily review / merge that.
3. Separately/later, we come up with a reasoning-optimized version and add that (either in Lean or Batteries, I'm happy either way).

[Mario Carneiro]

If I understand correctly, we don't currently have a reasoning-optimized version, is that right?

The reasoning optimized version is basically "have lemmas that say splitOn does something sensible". There is a fair bit of work on this in batteries#743 .