[Metaprogramming in Lean 4](https://leanprover-community.github.io/lean4-metaprogramming-book/main/04_metam.html#exercises) の MetaM の章の演習問題

Metaprogramming_Ch04.lean

import Lean

open Lean Meta

-- メタ変数関連
#check mkFreshExprMVar
#check MVarId.assign
#check getExprMVarAssignment?
#check instantiateMVars -- eの中のアサイン済みメタ変数をその値で置換する

-- コンテキスト関連
#check getLCtx
#check MVarId.withContext

-- 評価
#check withTransparency
#check whnf
#check isDefEq

-- 参考用

def doubleExpr₂ : MetaM Expr :=
  withLocalDecl `x BinderInfo.default (.const ``Nat []) λ x => do
    let body ← mkAppM ``Nat.add #[x, x]
    mkLambdaFVars #[x] body
#eval show MetaM _ from do
  ppExpr (← doubleExpr₂)

def somePropExpr : MetaM Expr := do
  let funcType ← mkArrow (.const ``Nat []) (.const ``Nat [])
  withLocalDecl `f BinderInfo.default funcType fun f => do
    let feqn ← withLocalDecl `n BinderInfo.default (.const ``Nat []) fun n => do
      let lhs := .app f n
      let rhs := .app f (← mkAppM ``Nat.succ #[n])
      let eqn ← mkEq lhs rhs
      mkForallFVars #[n] eqn
    mkLambdaFVars #[f] feqn
elab "someProp" : term => somePropExpr
#check someProp
#reduce someProp Nat.succ

def myAssumption (mvarId : MVarId) : MetaM Bool := do
  -- Check that `mvarId` is not already assigned.
  mvarId.checkNotAssigned `myAssumption
  -- Use the local context of `mvarId`.
  mvarId.withContext do
    -- The target is the type of `mvarId`.
    let target ← mvarId.getType
    -- For each hypothesis in the local context:
    for ldecl in ← getLCtx do
      -- If the hypothesis is an implementation detail, skip it.
      if ldecl.isImplementationDetail then
        continue
      -- If the type of the hypothesis is definitionally equal to the target
      -- type:
      if ← isDefEq ldecl.type target then
        -- Use the local hypothesis to prove the goal.
        mvarId.assign ldecl.toExpr
        -- Stop and return true.
        return true
    -- If we have not found any suitable local hypothesis, return false.
    return false

def myApply (goal : MVarId) (e : Expr) : MetaM (List MVarId) := do
  -- Check that the goal is not yet assigned.
  goal.checkNotAssigned `myApply
  -- Operate in the local context of the goal.
  goal.withContext do
    -- Get the goal's target type.
    let target ← goal.getType
    -- Get the type of the given expression.
    let type ← inferType e
    -- If `type` has the form `∀ (x₁ : T₁) ... (xₙ : Tₙ), U`, introduce new
    -- metavariables for the `xᵢ` and obtain the conclusion `U`. (If `type` does
    -- not have this form, `args` is empty and `conclusion = type`.)
    let (args, _, conclusion) ← forallMetaTelescopeReducing type
    -- If the conclusion unifies with the target:
    if ← isDefEq target conclusion then
      -- Assign the goal to `e x₁ ... xₙ`, where the `xᵢ` are the fresh
      -- metavariables in `args`.
      goal.assign (mkAppN e args)
      -- `isDefEq` may have assigned some of the `args`. Report the rest as new
      -- goals.
      let newGoals ← args.filterMapM λ mvar => do
        let mvarId := mvar.mvarId!
        if ! (← mvarId.isAssigned) && ! (← mvarId.isDelayedAssigned) then
          return some mvarId
        else
          return none
      return newGoals.toList
    -- If the conclusion does not unify with the target, throw an error.
    else
      throwTacticEx `myApply goal m!"{e} is not applicable to goal with target {target}"

def tryM (x : MetaM Unit) : MetaM Unit := do
  let s ← saveState
  try
    x
  catch _ =>
    restoreState s

-- 問題1
#eval show MetaM Unit from do
  let mvar1 ← mkFreshExprMVar (Expr.const ``Nat []) (userName := `mvar1)
  mvar1.mvarId!.assign (mkNatLit 3)

  let printMVars : MetaM Unit := do
    IO.println s!" {← mvar1.mvarId!.getTag} : {← mvar1.mvarId!.getType} := {← instantiateMVars mvar1}"
  printMVars

-- 問題2
-- 予想: 何も変化せず、入力の式がそのまま出力されるのでは？
#eval show MetaM Unit from do
  let expr ← instantiateMVars (Lean.mkAppN (Expr.const `Nat.add []) #[mkNatLit 1, mkNatLit 2])
  IO.println expr

-- 問題3
#eval show MetaM Unit from do
  let oneExpr := Expr.app (Expr.const `Nat.succ []) (Expr.const ``Nat.zero [])
  let twoExpr := Expr.app (Expr.const `Nat.succ []) oneExpr

  -- Create `mvar1` with type `Nat`
  let mvar1 ← mkFreshExprMVar (Expr.const ``Nat []) (userName := `mvar1)
  -- Create `mvar2` with type `Nat`
  let mvar2 ← mkFreshExprMVar (Expr.const ``Nat []) (userName := `mvar2)
  -- Create `mvar3` with type `Nat`
  let mvar3 ← mkFreshExprMVar (Expr.const ``Nat []) (userName := `mvar3)

  -- Assign `mvar1` to `2 + ?mvar2 + ?mvar3`
  mvar1.mvarId!.assign <| mkAppN (Expr.const `Nat.add []) #[(mkAppN (Expr.const `Nat.add []) #[twoExpr, mvar2]), mvar3]

  -- Assign `mvar3` to `1`
  mvar3.mvarId!.assign <| oneExpr

  -- Instantiate `mvar1`, which should result in expression `2 + ?mvar2 + 1`
  IO.println s!"{← instantiateMVars mvar1}"

-- 問題4
elab "explore" : tactic => do
  let mvarId : MVarId ← Lean.Elab.Tactic.getMainGoal
  let metavarDecl : MetavarDecl ← mvarId.getDecl

  IO.println "Our metavariable"
  -- type and userNameを出す
  IO.println s!"{← mvarId.getTag} : {← mvarId.getType}"

  IO.println "All of its local declarations"
  mvarId.withContext do
    let lctx ← getLCtx
    for ldecl in lctx do
      IO.println s!"{ldecl.userName} : {ldecl.type}"

elab "solve" : tactic => do
  let goal ← Elab.Tactic.getMainGoal
  let _result ← myAssumption goal

theorem red (hA : 1 = 1) (hB : 2 = 2) : 2 = 2 := by
  explore
  solve

-- 問題6
-- What is the normal form of the following expressions:
--   a) fun x => x of type Bool → Bool
--   b) (fun x => x) ((true && false) || true) of type Bool
--   c) 800 + 2 of type Nat

def sixA : Bool → Bool := fun x => x
-- .lam `x (.const `Bool []) (.bvar 0) (Lean.BinderInfo.default)
#eval Lean.Meta.reduce (Expr.const `sixA [])

def sixB : Bool := (fun x => x) ((true && false) || true)
-- .const `Bool.true []
#eval Lean.Meta.reduce (Expr.const `sixB [])

def sixC : Nat := 800 + 2
-- .lit (Lean.Literal.natVal 802)
#eval Lean.Meta.reduce (Expr.const `sixC [])

-- 問題7
-- Show that 1 created with Expr.lit (Lean.Literal.natVal 1) is definitionally equal to
--  an expression created with Expr.app (Expr.const ``Nat.succ []) (Expr.const ``Nat.zero []).
#check isDefEq
#eval show MetaM Unit from do
  let lhs : Expr := Expr.lit (Lean.Literal.natVal 1)
  let rhs : Expr := Expr.app (Expr.const ``Nat.succ []) (Expr.const ``Nat.zero [])
  let result ← isDefEq lhs rhs
  IO.println result

-- 問題8
-- Determine whether the following expressions are definitionally equal.
-- If Lean.Meta.isDefEq succeeds, and it leads to metavariable assignment,
-- write down the assignments.
-- a) 5 =?= (fun x => 5) ((fun y : Nat → Nat => y) (fun z : Nat => z))
--   DefEq で メタ変数のアサインはなし
-- b) 2 + 1 =?= 1 + 2
--   DefEq で メタ変数のアサインはなし
-- c) ?a =?= 2, where ?a has a type String
--   not DefEq で メタ変数のアサインはなし
-- d) ?a + Int =?= "hi" + ?b, where ?a and ?b don't have a type
--   DefEq で メタ変数のアサインあり ?a => "hi", ?b => Int
-- e) 2 + ?a =?= 3
--   not DefEq でメタ変数のアサインはなし
-- f) 2 + ?a =?= 2 + 1
--   DefEq で メタ変数のアサインあり ?a => 1

def a_l := 5
def a_r := (fun x => 5) ((fun y : Nat → Nat => y) (fun z : Nat => z))
#eval show MetaM Unit from do
  let mvar1 ← mkFreshExprMVar (Expr.const `String []) (userName := `a)
  let mvar2 ← mkFreshExprMVar none (userName := `b)
  let lhs : Expr := mkAppN (Expr.const `Nat.add []) #[mkNatLit 2, mvar1]
  let rhs : Expr := mkAppN (Expr.const `Nat.add []) #[mkNatLit 2, mkNatLit 1]
  let result ← isDefEq lhs rhs
  IO.println result
  IO.println s!" {← mvar1.mvarId!.getTag} : {← mvar1.mvarId!.getType} := {← instantiateMVars mvar1}"
  IO.println s!" {← mvar2.mvarId!.getTag} : {← mvar2.mvarId!.getType} := {← instantiateMVars mvar2}"

-- 問題9. Write down what you expect the following code to output.

@[reducible] def reducibleDef     : Nat := 1 -- same as `abbrev`
@[instance] def instanceDef       : Nat := 2 -- same as `instance`
def defaultDef                    : Nat := 3
@[irreducible] def irreducibleDef : Nat := 4

@[reducible] def sum := [reducibleDef, instanceDef, defaultDef, irreducibleDef]

#eval show MetaM Unit from do
  let constantExpr := Expr.const `sum []

  Meta.withTransparency Meta.TransparencyMode.reducible do
    let reducedExpr ← Meta.reduce constantExpr
    dbg_trace (← ppExpr reducedExpr) -- ...[1, instanceDef, defaultDef, irerducibleDef]

  Meta.withTransparency Meta.TransparencyMode.instances do
    let reducedExpr ← Meta.reduce constantExpr
    dbg_trace (← ppExpr reducedExpr) -- ...[1, 2, defaultDef, irerducibleDef]

  Meta.withTransparency Meta.TransparencyMode.default do
    let reducedExpr ← Meta.reduce constantExpr
    dbg_trace (← ppExpr reducedExpr) -- ...[1, 2, 3, irerducibleDef]

  Meta.withTransparency Meta.TransparencyMode.all do
    let reducedExpr ← Meta.reduce constantExpr
    dbg_trace (← ppExpr reducedExpr) -- ...[1, 2, 3, 4]

  let reducedExpr ← Meta.reduce constantExpr
  dbg_trace (← ppExpr reducedExpr) -- ...[1, 2, 3, 4]

-- 問題10
-- Create expression fun x, 1 + x in two ways:
#check fun x => 1 + x -- こういうこと？
-- a) not idiomatically, with loose bound variables
-- b) idiomatically.
-- In what version can you use Lean.mkAppN?
-- In what version can you use Lean.Meta.mkAppM
set_option pp.universes true in
set_option pp.explicit true in
#check fun x => 1 + x
def ex10_a : Expr := .lam `x (.const `Nat []) (mkAppN (.const ``HAdd.hAdd [0, 0, 0]) #[.const `Nat [], .const `Nat [], .const `Nat [], (mkAppN (.const `instHAdd [0]) #[.const `Nat [], .const `instNatAdd []]), mkNatLit 1, .bvar 0]) .default
def ex10_b : MetaM Expr := do
  withLocalDecl `x .default (.const ``Nat []) λ x => do
    let body ← mkAppM ``Nat.add #[mkNatLit 1, x]
    mkLambdaFVars #[x] body
#eval ppExpr ex10_a
#check HAdd.hAdd
#synth HAdd Nat Nat Nat
#eval do ppExpr (← ex10_b)

-- 問題11
-- Create expression ∀ (yellow: Nat), yellow.
-- example : 
#check_failure (∀ (yellow: Nat), yellow)
def ex11 : Expr := .forallE `yellow (.const `Nat []) (.bvar 0) .default
#eval ppExpr ex11

-- 問題12
-- Create expression ∀ (n : Nat), n = n + 1 in two ways:
-- a) not idiomatically, with loose bound variables
-- b) idiomatically.
-- In what version can you use Lean.mkApp3?
-- In what version can you use Lean.Meta.mkEq?
def ex12_a : MetaM Expr := do
  let nat := .const `Nat.add []
  let «n+1» := mkAppN nat #[.bvar 0, mkNatLit 1]
  let body := mkAppN (.const `Eq [1]) #[nat, .bvar 0, «n+1»]
  return .forallE `n (.const `Nat []) body .default
#eval do (ppExpr (← ex12_a))
def ex12_b : MetaM Expr := do
  withLocalDecl `n .default (.const ``Nat []) λ n => do
    let body ← do
      let rhs ← mkAppM ``Nat.add #[n, mkNatLit 1]
      mkEq n rhs
    let result ← mkLambdaFVars #[n] body
    dbg_trace result
    return result
#eval do (ppExpr (← ex12_b))

-- 問題13
-- Create expression fun (f : Nat → Nat), ∀ (n : Nat), f n = f (n + 1) idiomatically.

#check fun (f : Nat → Nat) => ∀ (n : Nat), f n = f (n + 1)
def nat : Expr := .const ``Nat []
def Nat2Nat : Expr := .forallE `_ nat nat .default
def ex13 : MetaM Expr := do
  withLocalDecl `f .default Nat2Nat λ f => do
    withLocalDecl `n .default nat λ n => do
      let lhs := mkAppN f #[n]
      let «n+1» ← mkAppM `Nat.add #[n, mkNatLit 1]
      let rhs := mkAppN f #[«n+1»]
      let prop := ← mkForallFVars #[n] (← mkEq lhs rhs)
      let result ← mkLambdaFVars #[f] prop
      return result
#eval do (ppExpr (← ex13))
def ex13' : Elab.Term.TermElabM Expr := do
  let stx : Syntax ← `(fun (f : Nat → Nat) => ∀ (n : Nat), f n = f (n + 1))
  let expr ← Elab.Term.elabTermAndSynthesize stx none
  return expr
#eval do (ppExpr (← ex13'))

-- 依存関数型(Expr.forallE) と 関数(Expr.lam) の違いが気になったので確認
#check Expr.forallE -- 依存関数型
#check Expr.lam -- 関数
#check ∀ (a b : Prop), a ∨ b
#check fun (a b : Prop) => a ∨ b
#check_failure (∀ (a b : Prop), a ∨ b) (1 = 1) (2 = 2)
#check (fun (a b : Prop) => a ∨ b) (1 = 1) (2 = 2)

-- 問題14
-- What would you expect the output of the following code to be?
#eval show Lean.Elab.Term.TermElabM _ from do
  let stx : Syntax ← `(∀ (a : Prop) (b : Prop), a ∨ b → b → a ∧ a)
  let expr ← Elab.Term.elabTermAndSynthesize stx none

  let (_, _, conclusion) ← forallMetaTelescope expr
  dbg_trace ← ppExpr conclusion -- ... `a ∧ a`

  let (_, _, conclusion) ← forallMetaBoundedTelescope expr 2
  dbg_trace ← ppExpr conclusion -- ... `a ∨ b → b → a ∧ a`

  let (_, _, conclusion) ← lambdaMetaTelescope expr
  dbg_trace ← ppExpr conclusion -- ... `∀ (a : Prop) (b : Prop), a ∨ b → b → a ∧ a`


-- 問題15
-- Check that the expressions ?a + Int and "hi" + ?b are definitionally equal
-- with isDefEq (make sure to use the proper types or Option.none for the types of your metavariables!).
-- Use saveState and restoreState to revert metavariable assignments.

#eval show MetaM Unit from do
  let mvar1 ← mkFreshExprMVar none (userName := `a)
  let mvar2 ← mkFreshExprMVar none (userName := `b)
  let lhs : Expr := mkAppN (Expr.const `Nat.add []) #[mvar1, .const ``Int []]
  let rhs : Expr := mkAppN (Expr.const `Nat.add []) #[mkStrLit "hi", mvar2]
  
  let state ← saveState

  let result ← isDefEq lhs rhs
  IO.println result
  IO.println s!" {← mvar1.mvarId!.getTag} : {← mvar1.mvarId!.getType} := {← instantiateMVars mvar1}"
  IO.println s!" {← mvar2.mvarId!.getTag} : {← mvar2.mvarId!.getType} := {← instantiateMVars mvar2}"

  restoreState state
  mvar1.mvarId!.setType (Expr.sort 1)
  mvar2.mvarId!.setType (Expr.const ``String [])
  let result ← isDefEq lhs rhs
  IO.println result
  IO.println s!" {← mvar1.mvarId!.getTag} : {← mvar1.mvarId!.getType} := {← instantiateMVars mvar1}"
  IO.println s!" {← mvar2.mvarId!.getTag} : {← mvar2.mvarId!.getType} := {← instantiateMVars mvar2}"