Zulip Chat Archive

Stream: new members

Topic: make a goal during elaboration


louq (Oct 05 2024 at 18:36):

How do I make a goal in elab?

elab "myTactic" : tactic => do

let goalType ← mkAppM Nat.add [mkConst Nat, mkConst ``Nat]

Give me an example on lean4 web

Chris Bailey (Oct 06 2024 at 02:26):

Read this

import Lean
open Lean Meta

elab "myTactic" : tactic => do
  let goalType  mkAppM ``True #[]
  let x  liftMetaM (mkFreshExprMVar (some goalType))
  Lean.Elab.Tactic.appendGoals [x.mvarId!]

example : 0 = 0 := by
  myTactic
  trace_state
  rfl
  exact trivial

Chris Bailey (Oct 06 2024 at 02:28):

Also straight from the book:

elab "step_1" : tactic => do
  let mvarId  getMainGoal
  let goalType  getMainTarget

  let Expr.app (Expr.app (Expr.const `Iff _) a) b := goalType | throwError "Goal type is not of the form `a ↔ b`"

  -- 1. Create new `_`s with appropriate types.
  let mvarId1  mkFreshExprMVar (Expr.forallE `xxx a b .default) (userName := "red")
  let mvarId2  mkFreshExprMVar (Expr.forallE `yyy b a .default) (userName := "blue")

  -- 2. Assign the main goal to the expression `Iff.intro _ _`.
  mvarId.assign (mkAppN (Expr.const `Iff.intro []) #[a, b, mvarId1, mvarId2])

  -- 3. Report the new `_`s to Lean as the new goals.
  modify fun _ => { goals := [mvarId1.mvarId!, mvarId2.mvarId!] }

Last updated: May 02 2025 at 03:31 UTC