Tactics

Tactics are Lean programs that manipulate a custom state. All tactics are, in the end, of type TacticM Unit. This has the type:

-- from Lean/Elab/Tactic/Basic.lean
TacticM = ReaderT Context $ StateRefT State TermElabM

But before demonstrating how to use TacticM, we shall explore macro-based tactics.

Tactics by Macro Expansion

Just like many other parts of the Lean 4 infrastructure, tactics too can be declared by lightweight macro expansion.

For example, we build an example of a custom_sorry_macro that elaborates into a sorry. We write this as a macro expansion, which expands the piece of syntax custom_sorry_macro into the piece of syntax sorry:

import Lean.Elab.Tactic

macro "custom_sorry_macro" : tactic => `(tactic| sorry)


example : 1 = 42 := by
  custom_sorry_macro

Implementing trivial: Extensible Tactics by Macro Expansion

As more complex examples, we can write a tactic such as custom_tactic, which is initially completely unimplemented, and can be extended with more tactics. We start by simply declaring the tactic with no implementation:

syntax "custom_tactic" : tactic

/- error: Tactic `tacticCustom_tactic` has not been implemented -/
example : 42 = 42 := by
  custom_tactic
  sorry

We will now add the rfl tactic into custom_tactic, which will allow us to prove the previous theorem

macro_rules
| `(tactic| custom_tactic) => `(tactic| rfl)

example : 42 = 42 := by
  custom_tactic

We can now try a harder problem, that cannot be immediately dispatched by rfl:

/-
error: Tactic `rfl` failed: The left-hand side
  43 = 43
is not definitionally equal to the right-hand side
  42 = 42

⊢ 43 = 43 ∧ 42 = 42
-/
example : 43 = 43 ∧ 42 = 42 := by
  custom_tactic

We extend the custom_tactic tactic with a tactic that tries to break And down with apply And.intro, and then (recursively (!)) applies custom_tactic to the two cases with (<;> trivial) to solve the generated subcases 43 = 43, 42 = 42.

macro_rules
| `(tactic| custom_tactic) => `(tactic| apply And.intro <;> custom_tactic)

The above declaration uses <;> which is a tactic combinator. Here, a <;> b means "run tactic a, and apply "b" to each goal produced by a". Thus, And.intro <;> custom_tactic means "run And.intro, and then run custom_tactic on each goal". We test it out on our previous theorem and see that we dispatch the theorem.

example : 43 = 43 ∧ 42 = 42 := by
  custom_tactic

In summary, we declared an extensible tactic called custom_tactic. It initially had no elaboration at all. We added the rfl as an elaboration of custom_tactic, which allowed it to solve the goal 42 = 42. We then tried a harder theorem, 43 = 43 ∧ 42 = 42 which custom_tactic was unable to solve. We were then able to enrich custom_tactic to split "and" with And.intro, and also recursively call custom_tactic in the two subcases.

Implementing <;>: Tactic Combinators by Macro Expansion

Recall that in the previous section, we said that a <;> b meant "run a, and then run b for all goals". In fact, <;> itself is a tactic macro. In this section, we will implement the syntax a and_then b which will stand for "run a, and then run b for all goals".

-- 1. We declare the syntax `and_then`
syntax tactic " and_then " tactic : tactic

-- 2. We write the expander that expands the tactic
--    into running `a`, and then running `b` on all goals produced by `a`.
macro_rules
| `(tactic| $a:tactic and_then $b:tactic) =>
    `(tactic| $a:tactic; all_goals $b:tactic)

-- 3. We test this tactic.
theorem test_and_then: 1 = 1 ∧ 2 = 2 := by
  apply And.intro and_then rfl

/-
info: theorem test_and_then : 1 = 1 ∧ 2 = 2 :=
⟨Eq.refl 1, Eq.refl 2⟩
-/
#print test_and_then

Exploring TacticM

The simplest tactic: sorry

In this section, we wish to write a tactic that fills the proof with sorry:

example : 1 = 2 := by
  custom_sorry

We begin by declaring such a tactic:

elab "custom_sorry_0" : tactic => do
  return


example : 1 = 2 := by
  custom_sorry_0
  -- unsolved goals: ⊢ 1 = 2
  guard_target =ₛ 1 = 2
  sorry

This defines a syntax extension to Lean, where we are naming the piece of syntax custom_sorry_0 as living in tactic syntax category. This informs the elaborator that, in the context of elaborating tactics, the piece of syntax custom_sorry_0 must be elaborated as what we write to the right-hand-side of the => (the actual implementation of the tactic).

Next, we write a term in TacticM Unit to fill in the goal with sorryAx α, which can synthesize an artificial term of type α. To do this, we first access the goal with Lean.Elab.Tactic.getMainGoal : Tactic MVarId, which returns the main goal, represented as a metavariable. Recall that under types-as-propositions, the type of our goal must be the proposition that 1 = 2. We check this by printing the type of goal.

But first we need to start our tactic with Lean.Elab.Tactic.withMainContext, which computes in TacticM with an updated context.

open Lean Elab Tactic Meta in

elab "custom_sorry_1" : tactic => withMainContext do
  let goal ← getMainGoal
  let goalDecl ← goal.getDecl
  let goalType := goalDecl.type
  Lean.logInfo f!"raw goal type: {goalType}"
  Lean.logInfo f!"goal type: {← ppExpr goalType}"


/-
info: raw goal type: Eq.{1} Nat (OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))
---
info: goal type: 1 = 2
-/
example : 1 = 2 := by
  custom_sorry_1

  -- unsolved goals: ⊢ 1 = 2
  guard_target =ₛ 1 = 2

  sorry

To sorry the goal, we can use the helper Lean.Elab.admitGoal:

open Lean Elab Tactic in

elab "custom_sorry_2" : tactic => withMainContext do
  let goal ← getMainGoal
  admitGoal goal

/- warning: declaration uses `sorry` -/
theorem test_custom_sorry : 1 = 2 := by
  custom_sorry_2

/-
info: theorem test_custom_sorry : 1 = 2 :=
sorry
-/
#print test_custom_sorry

And we no longer have the error unsolved goals: ⊢ 1 = 2.

The custom_assump tactic: Accessing Hypotheses

In this section, we will learn how to access the hypotheses to prove a goal. In particular, we shall attempt to implement a tactic custom_assump, which looks for an exact match of the goal among the hypotheses, and solves the theorem if possible.

In the example below, we expect custom_assump to use (H2 : 2 = 2) to solve the goal (2 = 2):

theorem assump_correct (H1 : 1 = 1) (H2 : 2 = 2) : 2 = 2 := by
  custom_assump

#print assump_correct
-- theorem assump_correct : 1 = 1 → 2 = 2 → 2 = 2 :=
-- fun H1 H2 => H2

When we do not have a matching hypothesis to the goal, we expect the tactic custom_assump to throw an error, telling us that we cannot find a hypothesis of the type we are looking for:

theorem assump_wrong (H1 : 1 = 1) : 2 = 2 := by
  custom_assump

#print assump_wrong
-- tactic 'custom_assump' failed, unable to find matching hypothesis of type (2 = 2)
-- H1 : 1 = 1
-- ⊢ 2 = 2

We begin by accessing the goal and the type of the goal so we know what we are trying to prove. The goal variable will soon be used to help us create error messages.

open Lean Elab Tactic Meta in

elab "custom_assump_0" : tactic => withMainContext do
    let goalType ← getMainTarget
    Lean.logInfo f!"raw goal type: {goalType}"
    Lean.logInfo f!"goal type: {← ppExpr goalType}"


/-
info: raw goal type: Eq.{1} Nat (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))
---
info: goal type: 2 = 2
-/
example (H1 : 1 = 1) (H2 : 2 = 2): 2 = 2 := by
  custom_assump_0

  -- unsolved goals
  -- H1 : 1 = 1
  -- H2 : 2 = 2
  -- ⊢ 2 = 2
  guard_hyp H1 :ₛ 1 = 1
  guard_hyp H2 :ₛ 2 = 2
  guard_target =ₛ 2 = 2

  sorry


/-
info: raw goal type: Eq.{1} Nat (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))
---
info: goal type: 2 = 2
-/
example (H1 : 1 = 1): 2 = 2 := by
  custom_assump_0

  -- unsolved goals
  -- H1 : 1 = 1
  -- ⊢ 2 = 2
  guard_hyp H1 :ₛ 1 = 1
  guard_target =ₛ 2 = 2

  sorry

Next, we access the list of hypotheses, which are stored in a data structure called LocalContext. This is accessed via Lean.MonadLCtx.getLCtx. The LocalContext contains LocalDeclarations, from which we can extract information such as the name that is given to declarations (.userName), the expression of the declaration (.toExpr). Let's write a tactic called list_local_decls that prints the local declarations:

open Lean Elab Tactic Meta in

elab "list_local_decls_1" : tactic => withMainContext do
  let ctx ← Lean.MonadLCtx.getLCtx -- get the local context.
  for decl in ctx do
    let declExpr := decl.toExpr -- Find the expression of the declaration.
    let declName := decl.userName -- Find the name of the declaration.

    -- we drop the number suffix for printing
    let displayDeclExpr : Expr → Name := fun expr =>
      match expr.fvarId!.name with
      | .num parent _ => parent
      | name => name

    Lean.logInfo <|
      f!"local decl:\n" ++
      f!"  name: {declName}\n" ++
      f!"  expr: {displayDeclExpr declExpr}"

/-
info: local decl:
  name: _example
  expr: _uniq
---
info: local decl:
  name: _H1
  expr: _uniq
---
info: local decl:
  name: _H2
  expr: _uniq
-/
example (_H1 : 1 = 1) (_H2 : 2 = 2): 1 = 1 := by
  list_local_decls_1
  rfl

Recall that we are looking for a local declaration that has the same type as the hypothesis. We get the type of LocalDecl by calling Lean.Meta.inferType on the local declaration's expression.

open Lean Elab Tactic Meta in

elab "list_local_decls_2" : tactic => withMainContext do
  let ctx ← MonadLCtx.getLCtx -- get the local context.
  for decl in ctx do
    let declExpr := decl.toExpr -- Find the expression of the declaration.
    let declName := decl.userName -- Find the name of the declaration.
    let declType ← inferType declExpr -- **NEW:** Find the type.

    -- we drop the number suffix for printing
    let displayDeclExpr : Expr → Name := fun expr =>
      match expr.fvarId!.name with
      | .num parent _ => parent
      | name => name

    Lean.logInfo <|
      f!"local decl:\n" ++
      f!"  name: {declName}\n" ++
      f!"  expr: {displayDeclExpr declExpr}\n" ++
      f!"  type: {← ppExpr declType}"

/-
info: local decl:
  name: _example
  expr: _uniq
  type: 1 = 1 → 2 = 2 → 1 = 1
---
info: local decl:
  name: _H1
  expr: _uniq
  type: 1 = 1
---
info: local decl:
  name: _H2
  expr: _uniq
  type: 2 = 2
-/
example (_H1 : 1 = 1) (_H2 : 2 = 2): 1 = 1 := by
  list_local_decls_2
  rfl

We check if the type of the LocalDecl is equal to the goal type with Lean.Meta.isExprDefEq. See that we check if the types are equal at eq?, and we print that H1 has the same type as the goal (local decl[EQUAL? true]: name: H1), and we print that H2 does not have the same type (local decl[EQUAL? false]: name: H2 ):

open Lean Elab Tactic Meta in

elab "list_local_decls_3" : tactic => withMainContext do
  let goalType ← getMainTarget
  let ctx ← MonadLCtx.getLCtx -- get the local context.
  for decl in ctx do
    let declExpr := decl.toExpr -- Find the expression of the declaration.
    let declName := decl.userName -- Find the name of the declaration.
    let declType ← inferType declExpr -- Find the type.
    let eq? ← isExprDefEq declType goalType -- **NEW** Check if type equals goal type.
    Lean.logInfo f!"local decl[EQUAL? {eq?}]: name: {declName}"

/-
info: local decl[EQUAL? false]: name: _example
---
info: local decl[EQUAL? true]: name: _H1
---
info: local decl[EQUAL? false]: name: _H2
-/
example (_H1 : 1 = 1) (_H2 : 2 = 2): 1 = 1 := by
  list_local_decls_3
  rfl

Finally, we put all of these parts together to write a tactic that loops over all declarations and finds one with the correct type. We loop over declarations with lctx.findDeclM?. We infer the type of declarations with Lean.Meta.inferType. We check that the declaration has the same type as the goal with Lean.Meta.isExprDefEq:

open Lean Elab Tactic Meta in

elab "custom_assump_1" : tactic => withMainContext do
  let goalType ← getMainTarget
  let lctx ← MonadLCtx.getLCtx
  -- Iterate over the local declarations...
  let matching_expr? ← lctx.findDeclM? fun ldecl: Lean.LocalDecl => do
    let declExpr := ldecl.toExpr -- Find the expression of the declaration.
    let declType ← inferType declExpr -- Find the type.
    -- Check if type equals goal type.
    if (← isExprDefEq declType goalType) then
      -- If equal, success!
      return some declExpr
    else
      -- Not found.
      return none
  match matching_expr? with
  | some matching_expr => Lean.logInfo f!"matching_expr: {← ppExpr matching_expr}"
  | none => Lean.logInfo f!"matching_expr: none"

/- info: matching_expr: _H2 -/
example (_H1 : 1 = 1) (_H2 : 2 = 2) : 2 = 2 := by
  custom_assump_1
  rfl

/- info: matching_expr: none -/
example (_H1 : 1 = 1) : 2 = 2 := by
  custom_assump_1
  rfl

Now that we are able to find the matching expression, we need to close the theorem by using the match. We do this with Lean.Elab.Tactic.closeMainGoal. When we do not have a matching expression, we throw an error with Lean.Meta.throwTacticEx, which allows us to report an error corresponding to a given goal. When throwing this error, we format the error using m!"..." which builds a MessageData. This provides nicer error messages than using f!"..." which builds a Format. This is because MessageData also runs delaboration, which allows it to convert raw Lean terms like (Eq.{1} Nat (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)) (OfNat.ofNat.{0} Nat 2 (instOfNatNat 2))) into readable strings like(2 = 2). The full code listing given below shows how to do this:

open Lean Elab Tactic Meta in

elab "custom_assump_2" : tactic => withMainContext do
  let goal ← getMainGoal
  let goalType ← getMainTarget
  let ctx ← Lean.MonadLCtx.getLCtx
  let option_matching_expr ← ctx.findDeclM? fun decl: Lean.LocalDecl => do
    let declExpr := decl.toExpr
    let declType ← inferType declExpr
    if ← isExprDefEq declType goalType then
      return Option.some declExpr
    else
      return Option.none
  match option_matching_expr with
  | some e => closeMainGoal `custom_assump_2 e
  | none =>
    throwTacticEx `custom_assump_2 goal
      (m!"unable to find matching hypothesis of type ({goalType})")

example (_H1 : 1 = 1) (H2 : 2 = 2) : 2 = 2 := by
  custom_assump_2

/-
error: Tactic `custom_assump_2` failed: unable to find matching hypothesis of type (2 = 2)

H1 : 1 = 1
⊢ 2 = 2
-/
example (H1 : 1 = 1) : 2 = 2 := by
  custom_assump_2

Tweaking the context

Until now, we've only performed read-like operations with the context. But what if we want to change it? In this section we will see how to change the order of goals and how to add content to it (new hypotheses).

Then, after elaborating our terms, we will need to use the helper function Lean.Elab.Tactic.liftMetaTactic, which allows us to run computations in MetaM while also giving us the goal MVarId for us to play with. In the end of our computation, liftMetaTactic expects us to return a List MVarId as the resulting list of goals.

The only substantial difference between custom_let and custom_have is that the former uses Lean.MVarId.define and the later uses Lean.MVarId.assert:

open Lean.Elab.Tactic in

elab "custom_let " n:ident " : " t:term " := " v:term : tactic => withMainContext do
  let t ← elabTerm t none
  let v ← elabTermEnsuringType v t
  liftMetaTactic fun mvarId => do
    let mvarIdNew ← mvarId.define n.getId t v
    let (_, mvarIdNew) ← mvarIdNew.intro1P
    return [mvarIdNew]

open Lean.Elab.Tactic in

elab "custom_have " n:ident " : " t:term " := " v:term : tactic => withMainContext do
  let t ← elabTerm t none
  let v ← elabTermEnsuringType v t
  liftMetaTactic fun mvarId => do
    let mvarIdNew ← mvarId.assert n.getId t v
    let (_, mvarIdNew) ← mvarIdNew.intro1P
    return [mvarIdNew]

theorem test_faq_have : True := by
  custom_let n : Nat := 5
  custom_have h : n = n := rfl

  -- n : Nat := 5
  -- h : n = n
  -- ⊢ True
  guard_hyp n :ₛ Nat := 5
  guard_hyp h :ₛ n = n
  guard_target =ₛ True

  trivial

"Getting" and "Setting" the list of goals

To illustrate these, let's build a tactic that can reverse the list of goals. We can use Lean.Elab.Tactic.getGoals and Lean.Elab.Tactic.setGoals:

elab "reverse_goals" : tactic =>
  Lean.Elab.Tactic.withMainContext do
    let goals : List Lean.MVarId ← Lean.Elab.Tactic.getGoals
    Lean.Elab.Tactic.setGoals goals.reverse


theorem test_reverse_goals : (1 = 2 ∧ 3 = 4) ∧ 5 = 6 := by
  constructor
  constructor
  -- case left.left
  -- ⊢ 1 = 2
  -- case left.right
  -- ⊢ 3 = 4
  -- case right
  -- ⊢ 5 = 6

  reverse_goals
  next =>
    guard_target =ₛ 5 = 6
    sorry
  next =>
    guard_target =ₛ 3 = 4
    sorry
  next =>
    guard_target =ₛ 1 = 2
    sorry

FAQ

In this section, we collect common patterns that are used during writing tactics, to make it easy to find common patterns.

Q: How do I use goals?

A: Goals are represented as metavariables. The module Lean.Elab.Tactic.Basic has many functions to add new goals, switch goals, etc.

Q: How do I get the main goal?

A: Use Lean.Elab.Tactic.getMainGoal.

open Lean Elab Tactic Meta in

elab "faq_main_goal" : tactic => withMainContext do
  let goal ← getMainGoal
  let goalType ← goal.getType
  Lean.logInfo f!"goal: {← ppExpr goalType}"

/- info: goal: 1 = 1 -/
example : 1 = 1 := by
  faq_main_goal
  rfl

Q: How do I get the list of goals?

A: Use getGoals.

open Lean Elab Tactic Meta in

elab "faq_get_goals" : tactic => withMainContext do
  let goals ← getGoals
  for goal in goals do
    let goalType ← goal.getType
    Lean.logInfo f!"goal type: {← ppExpr goalType}"


/-
info: goal type: false = true
---
info: goal type: true = true
-/
example (b : Bool) : b = true := by
  cases b
  faq_get_goals
  · sorry
  · rfl

Q: How do I get the current hypotheses for a goal?

A: Use Lean.MonadLCtx.getLCtx which provides the local context, and then iterate on the LocalDeclarations of the LocalContext.

open Lean Elab Tactic Meta in

elab "faq_get_hypotheses" : tactic => withMainContext do
  let ctx ← MonadLCtx.getLCtx -- get the local context.
  for decl in ctx do
    let declExpr := decl.toExpr -- Find the expression of the declaration.
    let declType := decl.type -- Find the type of the declaration.
    let declName := decl.userName -- Find the name of the declaration.

    -- we drop the number suffix for printing
    let displayDeclExpr : Expr → Name := fun expr =>
      match expr.fvarId!.name with
      | .num parent _ => parent
      | name => name

    Lean.logInfo <|
      f!"local decl:\n" ++
      f!"  name: {declName}\n" ++
      f!"  expr: {displayDeclExpr declExpr}\n" ++
      f!"  type: {← ppExpr declType}"

/-
info: local decl:
  name: _example
  expr: _uniq
  type: 1 = 1 → 2 = 2 → 3 = 3
---
info: local decl:
  name: _H1
  expr: _uniq
  type: 1 = 1
---
info: local decl:
  name: _H2
  expr: _uniq
  type: 2 = 2
-/
example (_H1 : 1 = 1) (_H2 : 2 = 2): 3 = 3 := by
  faq_get_hypotheses
  rfl

Q: How do I evaluate a tactic?

A: Use Lean.Elab.Tactic.evalTactic: Syntax → TacticM Unit which evaluates a given tactic syntax. One can create tactic syntax using the macro `(tactic| ⋯).

For example, one could call try rfl with the piece of code:

Lean.Elab.Tactic.evalTactic (← `(tactic| try rfl))

Q: How do I check if two expressions are equal?

A: Use Lean.Meta.isExprDefEq <expr-1> <expr-2>.

/- info: Lean.Meta.isExprDefEq (t s : Lean.Expr) : Lean.MetaM Bool -/
#check Lean.Meta.isExprDefEq

Q: How do I throw an error from a tactic?

A: Use throwTacticEx <tactic-name> <goal-mvar> <error>.

elab "faq_throw_error" : tactic =>
  Lean.Elab.Tactic.withMainContext do
    let goal ← Lean.Elab.Tactic.getMainGoal
    Lean.Meta.throwTacticEx `faq_throw_error goal "throwing an error at the current goal"

/-
error: Tactic `faq_throw_error` failed: throwing an error at the current goal

b : Bool
⊢ b = true
-/
example (b : Bool) : b = true := by
  faq_throw_error

Q: What is the difference between Lean.Elab.Tactic.* and Lean.Meta.Tactic.*?

A: Lean.Meta.Tactic.* contains low level code that uses the Meta monad to implement basic features such as rewriting. Lean.Elab.Tactic.* contains high-level code that connects the low level development in Lean.Meta to the tactic infrastructure and the parsing front-end.

Exercises

1. Consider the theorem p ∧ q ↔ q ∧ p. We could either write its proof as a proof term, or construct it using the tactics. When we are writing the proof of this theorem as a proof term, we're gradually filling up _s with certain expressions, step by step. Each such step corresponds to a tactic.

   There are many combinations of steps in which we could write this proof term - but consider the sequence of steps we wrote below. Please write each step as a tactic. The tactic step_1 is filled in, please do the same for the remaining tactics (for the sake of the exercise, try to use lower-level apis, such as mkFreshExprMVar, mvarId.assign and modify fun _ => { goals := ~).

   -- [this is the initial goal]
   example : p ∧ q ↔ q ∧ p :=
     _
   
   -- step_1
   example : p ∧ q ↔ q ∧ p :=
     Iff.intro _ _
   
   -- step_2
   example : p ∧ q ↔ q ∧ p :=
     Iff.intro
       (
         fun hA =>
         _
       )
       (
         fun hB =>
         (And.intro hB.right hB.left)
       )
   
   -- step_3
   example : p ∧ q ↔ q ∧ p :=
     Iff.intro
       (
         fun hA =>
         (And.intro _ _)
       )
       (
         fun hB =>
         (And.intro hB.right hB.left)
       )
   
   -- step_4
   example : p ∧ q ↔ q ∧ p :=
     Iff.intro
       (
         fun hA =>
         (And.intro hA.right hA.left)
       )
       (
         fun hB =>
         (And.intro hB.right hB.left)
       )
   

   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!] }
   

   theorem gradual (p q : Prop) : p ∧ q ↔ q ∧ p := by
     step_1
     step_2
     step_3
     step_4
   

2. In the first exercise, we used lower-level modify api to update our goals. liftMetaTactic, setGoals, appendGoals, replaceMainGoal, closeMainGoal, etc. are all syntax sugars on top of modify fun s : State => { s with goals := myMvarIds }. Please rewrite the forker tactic with:

   a) liftMetaTactic b) setGoals c) replaceMainGoal

   elab "forker" : tactic => do
     let mvarId ← getMainGoal
     let goalType ← getMainTarget
   
     let (Expr.app (Expr.app (Expr.const `And _) p) q) := goalType | Lean.Meta.throwTacticEx `forker mvarId (m!"Goal is not of the form P ∧ Q")
   
     mvarId.withContext do
       let mvarIdP ← mkFreshExprMVar p (userName := "red")
       let mvarIdQ ← mkFreshExprMVar q (userName := "blue")
   
       let proofTerm := mkAppN (Expr.const `And.intro []) #[p, q, mvarIdP, mvarIdQ]
       mvarId.assign proofTerm
   
       modify fun state => { goals := [mvarIdP.mvarId!, mvarIdQ.mvarId!] ++ state.goals.drop 1 }
   

   example (A B C : Prop) : A → B → C → (A ∧ B) ∧ C := by
     intro hA hB hC
     forker
     forker
     assumption
     assumption
     assumption
   

3. In the first exercise, you created your own intro in step_2 (with a hardcoded hypothesis name, but the basics are the same). When writing tactics, we usually want to use functions such as intro, intro1, intro1P, introN or introNP.

   For each of the points below, create a tactic introductor (one per each point), that turns the goal (ab: a = b) → (bc: b = c) → (a = c):

   a) into the goal (a = c) with hypotheses (ab✝: a = b) and (bc✝: b = c). b) into the goal (bc: b = c) → (a = c) with hypothesis (ab: a = b). c) into the goal (bc: b = c) → (a = c) with hypothesis (hello: a = b).

   example (a b c : Nat) : (ab: a = b) → (bc: b = c) → (a = c) := by
     introductor
     sorry
   

   Hint: "P" in intro1P and introNP stands for "Preserve".