Alternative MetaM

Stream: mathlib4

[Scott Morrison]

failed to synthesize instance
  Alternative MetaM

Am I expecting the wrong thing here?

I've been implementing solve_by_elim in Lean4, and I have a very hacky solution with mutable variables inside try ... catch blocks in order to test if a tactic is failing, but the "obvious" approach using List.firstM or similar fails with the error above.

[Scott Morrison]

Providing a #mwe:

import Lean.Meta.Tactic.Apply
import Lean.Elab.Tactic.Basic

open Lean.Elab.Tactic

/-- Attempt to solve the given metavariable by repeating applying a local hypothesis. -/
def Lean.Meta.solveByElim : Nat → MVarId → MetaM Unit
  | 0, mvarId => throwError "fail"
  | (n+1), mvarId => do
    -- We attempt to find a local declaration which can be applied,
    -- and for which all resulting sub-goals can be discharged using `solveByElim n`.
    let r ← (← getLCtx).findDeclRevM? fun localDecl => do
      if localDecl.isAuxDecl then
        return none
      else
        let mut success := false
        let s ← try
          for g in (← apply mvarId localDecl.toExpr) do solveByElim n g
          success := true
        catch | _ => success := false
         if success then some Unit.unit else none

namespace Lean.Elab
namespace Tactic

elab "solveByElim" : tactic => withMainContext do
  Meta.solveByElim 6 (← getMainGoal)

end Tactic
end Lean.Elab

def test1 (h : Nat) : Nat := by solveByElim
def test2 {α β : Type} (f : α → β) (a : α) : β := by solveByElim
def test3 {α β : Type} (f : α → α → β) (a : α) : β := by solveByElim
def test4 {α β γ : Type} (f : α → β) (g : β → γ) (a : α) : γ := by solveByElim
def test5 {α β γ : Type} (f : α → β) (g : β → γ) (b : β) : γ := by solveByElim

demonstrates the bare bones of solveByElim, but the success variable is obviously all boilerplate.

I'd hoped I could just write

import Lean.Meta.Tactic.Apply
import Lean.Elab.Tactic.Basic

namespace Lean.LocalContext

universe u v
variable {m : Type u → Type v} [Monad m] [Alternative m]
variable {β : Type u}

/-- Return the result of `f` on the first local declaration on which `f` succeeds. -/
def firstDeclM (lctx : LocalContext) (f : LocalDecl → m β) : m β :=
  do match (← lctx.findDeclM? (optional ∘ f)) with
  | none   => failure
  | some b => b

end Lean.LocalContext

open Lean.Elab.Tactic

/-- Attempt to solve the given metavariable by repeating applying a local hypothesis. -/
def Lean.Meta.solveByElim : Nat → MVarId → MetaM Unit
  | 0, mvarId => throwError "fail"
  | (n+1), mvarId => do
    -- We attempt to find a local declaration which can be applied,
    -- and for which all resulting sub-goals can be discharged using `solveByElim n`.
       (← getLCtx).firstDeclM fun localDecl => do
         if localDecl.isAuxDecl then
           failure
         else
           for g in (← apply mvarId localDecl.toExpr) do solveByElim n g

instead, but this fails trying to synthesize Alternative MetaM.

Recommendations for a concise solution welcome! :-)

[Leonardo de Moura]

Added https://github.com/leanprover/lean4/commit/5a7044365b70a434d59d34f0d302c88ce83f9715