Tactic to "apply" + "congr"

Stream: lean4

[Jeremy Salwen]

Having a hard time figuring out if a tactic like this exists. I would like to apply a lemma, but instead of failing if some of the terms don't match, just generate new hypotheses of their equality.

Here is a MWE:

import Std.Data.List.Basic
import Mathlib.Tactic.applyFun

open Lean

lemma List.isPrefix_double: l <+: l ++ l := sorry

lemma List.examp (a b: List α):  take (length delim) a <+: b ++ [] := by
  -- new_apply_tactic List.isPrefix_self
  -- now (hypothetically) we have the new goal
  -- b ++ [] = (take (length delim) a) ++ (take (length delim) a)

[Scott Morrison]

convert; unlike apply you need to provide all the arguments of the function, but these can be _ and will be solved by unification where possible.

[Jeremy Salwen]

Thanks! It seems like this matches what I was looking for, but it's not as powerful as I expected. Here is an example of its failure:

import Std.Data.List.Basic
import Mathlib.Tactic.applyFun

open Lean

def f (l: List α): Bool := sorry
lemma helper:  ∀ (s t: List α), f (s ++ t) = true := sorry

lemma examp  (a:α): f [a] = true := by
  convert helper _ _
  -- This doesn't work.  Ideally at this point I would just have a new goal:
  -- ∃ s t, s ++ t = [a]

[Kyle Miller]

In Lean 4, there's now a distinction between _ (placeholders that must be solved by unification) and ?_ (placeholders that may create new goals).

lemma examp  (a:α): f [a] = true := by
  convert helper (α := α) ?_ ?_
  -- Three goals:
  -- ⊢ [a] = ?_1 ++ ?_2
  -- ⊢ List α
  -- ⊢ List α

[Kyle Miller]

Note that I had to write (α := α) to fill in what α is supposed to be. I guess convert isn't able to fill in this argument by unification... (I feel that it should though)

[Ruben Van de Velde]

Seems like convert got a bit weaker in lean 4