Using `simp` inductively breaks `deriving_by` proof state

Stream: general

[Ayhon]

When the simp tactic performs an inductive step in a proof, the proof state obtained in the deriving_by section contains duplicated definitions that generally prevent you from closing the goal.

Her's a MWE.

def foo(ls: List Bool)(i: Nat): List Bool :=
  if i + 1 < ls.length then foo ls (i + 1) else ls
termination_by ls.length - i

def length_foo(ls: List Bool)(i: Nat)
: (foo ls i).length = ls.length
:= by
  unfold foo
  split
  · simp [*, length_foo]
  · simp
termination_by ls.length - i
decreasing_by
  try omega
  sorry

The position with the sorry is where one can see the mangled proof state.

[Notification Bot]

This topic was moved here from #general > Weird proof state in deriving_by by Ayhon.

[Robin Arnez]

Hmm looking at this using by? it seems like there are some non-beta reduced proofs: (fun ls i => length_foo ls i) ls (i + 1).

[Robin Arnez]

So you could use a beta-reduction combinator:

import Lean.Elab

def foo (ls : List Bool) (i : Nat) : List Bool :=
  if i + 1 < ls.length then foo ls (i + 1) else ls

open Lean Elab Term Meta in
elab "beta_reduce" x:term : term <= expected => do
  let expected ← instantiateMVars expected
  let expected ← Core.betaReduce expected
  let term ← elabTermAndSynthesize x expected
  let term ← instantiateMVars term
  Core.betaReduce term

theorem length_foo (ls : List Bool) (i : Nat) : (foo ls i).length = ls.length := beta_reduce by
  unfold foo
  split
  · simp [*, length_foo]
  · simp