autoParam with deferral

Stream: mathlib4

[Jireh Loreaux]

Is it possible to have an autoParam which just defers a goal it can't solve?

[Kyle Miller]

Here's a giant hack:

import Lean

open Lean Elab Tactic in
elab "defer" : tactic => liftMetaTactic1 fun _ => return none

def foo (x y : Nat) (h : x = y := by defer) : Nat := x

example : True := by
  have := foo 1 2
  /-
  case refine_2
  this: ℕ
  ⊢ True
  case refine_1
  ⊢ 1 = 2
  -/

You could do by tactic_to_try <|> defer

[Kyle Miller]

The way the hack works is that it just ignores the goal completely in the autoParam, and since goals metavariables are ?_ rather than _ metavariables, refine, etc., will turn them into new goals.

[Jireh Loreaux]

this is cool, but unfortunately it's not quite working in my use case (I'll try to #mwe). The issue is that I would like to use autoParams for lemmas used in rewriting (or maybe even simp) and have it fail to prove the desired goal gracefully. (I understand maybe simp can't do this, but at least I would want rwto do it).

I'm also running into the issue that when using simp, even in a case where it should work, it crashes the server because as you are typing, before Lean has enough information to fill in the metavariables to allow the autoParam to succeed, it goes crazy trying to solve it ahead of time.