iff を分解できる iff_constructor

[Seasawher]

import Lean

open Lean Meta Elab Tactic Command

/-- 自作したコンストラクタ。ただし iff のみを分解できる -/
elab "iff_constructor" : tactic => do
  let mvarId ← getMainGoal
  let goalType ← getMainTarget

  let_expr 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 `x a b .default) (userName := `mp)
  let mvarId2 ← mkFreshExprMVar (Expr.forallE `y b a .default) (userName := `mpr)

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

example (p q : Prop) (h1 : p → q) (h2 : q → p) : p ↔ q := by
  iff_constructor

  case mp => assumption
  case mpr => assumption

[Seasawher]

Expr を作るところがややこい。Qq ライブラリで楽をしたい。

うまくいかないな？

Zulip: how to use Qq library

import Lean
import Qq

open Qq
open Lean Meta Elab Tactic Command

/-- 自作したコンストラクタ。ただし iff のみを分解できる -/
elab "iff_constructor" : tactic => do
  let mvarId ← getMainGoal
  let goalType ← getMainTarget

  let_expr Iff a b := goalType
    | throwError "Goal type is not of the form `a ↔ b`"

  -- a と b を quotation ライブラリで利用可能にする
  let a : Q(Prop) := a
  let b : Q(Prop) := b

  -- 1. Create new `_`s with appropriate types.
  let mvarId1 ← mkFreshExprMVar q($a → $b) (userName := `mp)
  let mvarId2 ← mkFreshExprMVar q($b → $a) (userName := `mpr)

  let mvarId1 : Q($a → $b) := mvarId1
  /-
  unquoteExpr: a✝ : Expr
  -/
  let mvarId2 : Q($b → $a) := mvarId2

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

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

example (p q : Prop) (h1 : p → q) (h2 : q → p) : p ↔ q := by
  iff_constructor

  case mp => assumption
  case mpr => assumption

[Seasawher]

Qq ライブラリで楽をする例

import Lean
import Qq

open Qq
open Lean Meta Elab Tactic Command

/-- 自作したコンストラクタ。ただし iff のみを分解できる -/
elab "iff_constructor" : tactic => do
  let mvarId ← getMainGoal
  let goalType ← getMainTarget

  let_expr Iff a b := goalType
    | throwError "Goal type is not of the form `a ↔ b`"

  -- a と b を quotation ライブラリで利用可能にする
  have a : Q(Prop) := a
  have b : Q(Prop) := b

  let mvarId1 ← mkFreshExprMVarQ q($a → $b) (userName := `mp)
  let mvarId2 ← mkFreshExprMVarQ q($b → $a) (userName := `mpr)

  mvarId.assign q(@Iff.intro $a $b $mvarId1 $mvarId2)

  modify fun _ => { goals := [mvarId1.mvarId!, mvarId2.mvarId!] }

example (p q : Prop) (h1 : p → q) (h2 : q → p) : p ↔ q := by
  iff_constructor

  case mp => assumption
  case mpr => assumption