Tactic similar to `apply` but generates equalities

Stream: Is there code for X?

[Winston]

Hi, are there any tactics like apply but which generates equalities for any failed unification attempts? Something like:

inductive Test : Int → Int → Bool → Prop where
  | mk (l r : Int) : Test l r (l < r)
theorem test (n : Nat) : Test (Int.negSucc n) 0 true := by
  apply Test.mk
  -- Generates a goal `Int.negSucc n < 0 = true`, or even something like: `Int.negSucc n = ?l`, `0 = ?r`, and `?l < ?r = true`.

Thanks! Sorry if I've missed anything in the docs/source/zulip.

[Martin Dvořák]

I don't understand your example, but your description sounds like convert (when you already have a proof of what you claim to be equivalent to your goal) or convert_to (when the new goal is yet to be proved) is what you might want.

[Junyan Xu]

convert Test.mk _ _ should work in this case, at least in Lean 3.
But why don't you do

inductive Test : Int → Int → Prop where
  | mk (l r : Int) : l < r → Test l r
theorem test (n : Nat) : Test (Int.negSucc n) 0 := Test.mk _ _ (by ...)

?

[Winston]

Thanks for both your suggestions! I've tried them and I'm getting a bit further but I think unfortunately my actual example is a bit more complex (sorry I think I may have minimised it incorrectly in the first place):

inductive Value where
  | bool : (b : Bool) → Value
  | int : (i : Int) → Value

inductive Expr where
  | int (i : Int)
  | intLt (l r : Expr)

inductive Eval : Expr → Value → Prop where  -- `Eval e v` means that the expression `e` can evaluate to `v`.
  | int (i : Int) : Eval (Expr.int i) (Value.int i)
  | intLt (l r : Expr) (li ri : Int)
    (lEval : Eval l (Value.int li)) (rEval : Eval r (Value.int ri))  -- Witnesses that `l` evaluates to `li` and `r` to `ri`.
    : Eval (Expr.intLt l r) (Value.bool (li < ri))

theorem test (n : Nat) : Eval (Expr.intLt (Expr.int (Int.negSucc n)) (Expr.int 0)) (Value.bool true) := by
  convert Eval.intLt _ _ _ _ _ _
  -- I run into a whole bunch of:
  --   don't know how to synthesize placeholder for argument 'l'
  --   don't know how to synthesize placeholder for argument 'r'
  --   <repeat for `li`, `ri`, `lEval`, and `rEval`>

I should also state that I'm using leanprover/lean4:nightly-2022-12-23, I think @Junyan Xu's suggestion of convert Test.mk _ _ also produces don't know how to synthesize placeholder for argument :(

I get a bit further if I try convert Eval.intLt ?_ ?_ ?_ ?_ ?_ ?_ but then I'm unable to discharge goals like Expr.int (Int.negSucc n) = ?_1 with rfl, (It may be possible I am running into https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Synthetic.20metavariables.20in.20exact/near/240212860 ?).