nicer calculation in Lean

Stream: Is there code for X?

[Asei Inoue]

In Lean, when I want to interactively perform equational reasoning using tactics in a situation where the answer is not already known, what is the best approach?

Currently, the best method I have is to use the example command with the right-hand side filled in with sorry. However, ideally, I would like something that makes the #conv command easier to use.

namespace Playground

/-- A function that reverses a list.
This is a very inefficient implementation because it uses `(· ++ ·)` recursively. -/
def reverse {α : Type} (xs : List α) : List α :=
  match xs with
  | [] => []
  | x :: xs => reverse xs ++ [x]

#guard reverse [1, 2, 3] = [3, 2, 1]

/-- A more general version of the `reverse` function. -/
def reverse' {α : Type} (xs ys : List α) : List α :=
  reverse xs ++ ys

set_option warn.sorry false

/-- Property (computation) for the base case -/
example {α : Type} (ys : List α) : reverse' [] ys = sorry := by
  rw [reverse']
  dsimp [reverse]
  -- ys = sorry
  sorry

/-- Property (computation) for the recursive case -/
example {α : Type} (x : α) (xs ys : List α) :
  reverse' (x :: xs) ys = sorry := by
  rw [reverse']
  dsimp [reverse]
  ac_nf
  rw [← reverse']
  -- reverse' xs ([x] ++ ys) = sorry
  sorry

end Playground

[Asei Inoue]

Ideally, I would like a command that can be used with a syntax similar to example, but allows applying tactics like the #conv command.