Using Tactics to Generate `=` Theorems

Stream: lean4

[Markus Schmaus]

I've been looking into how to use tactics in order to generate theorems, rather than just proving them. This is primarily meant for simple theorems similar to docs#Function.comp_def or docs#List.map_eq_map.

Here is what I have come up with:

import Mathlib

macro "transform" f:term " => " cs:Lean.Parser.Tactic.Conv.convSeq : tactic => do
  `(tactic| (
      have eq : $f = $f := rfl
      conv at eq =>
        rhs
        ($cs)
      exact eq))

def f (n : Nat) : Nat :=
  n * 2

def g (n : Nat) : Nat :=
  2 * f n

@[simp]
def g_def := by
  transform g =>
    unfold g
    unfold f

#check g_def

example :  g = fun n => 2 * (n * 2) := by
  simp?


def h (n : Nat) : Nat :=
  3 * f n

def map_g_def (xs : List Nat) := by
  transform h <$> [1, 2, 3] =>
    simp only [Functor.map, List.map_eq_map]
    unfold h
    unfold f
    ring_nf

#check map_g_def

Writing transform term => puts me into conversation mode which allows me to use tactics to simplify the term. The most useful tactics for this is probably unfold, but other tactics like simp or ring work as well.

This is my first foray into meta programming, so any feedback would be highly welcomed. It only works with def and not with theorem, does this make any difference? Also, the goal only shows up once I write my first tactic, can this be fixed?

[Kyle Miller]

@Markus Schmaus This is a nice idea. I made a prototype for a full definition command for these, so for example

transform map_g_def : h <$> [1, 2, 3] =>
  simp only [Functor.map, List.map_eq_map, List.map]
  unfold h
  unfold f
  ring_nf

#check map_g_def
-- map_g_def : h <$> [1, 2, 3] = [6, 12, 18]

I didn't go as far as making this support binders like theorem would, and it might be buggy, but at least it lets you use variable to add extra binders.

[Kyle Miller]

Here's my implementation. I couldn't find a way to use the theorem command directly so I had to copy its implementation (and doubtless get some of it wrong).

import Mathlib

open Lean Meta Elab Tactic

syntax declModifiers "transform " ident " : " term " => " Parser.Tactic.Conv.convSeq : command

elab_rules : command
  | `($mods:declModifiers transform%$tk $id : $t =>%$arr $code) => do
    let mods ← elabModifiers mods
    Elab.Command.runTermElabM fun args => do
      let e ← Elab.Term.elabTermAndSynthesize t none
      withRef tk do
        let aux : TacticM (Expr × Expr) := withRef (mkNullNode #[tk, arr]) do
          let (e', proof) ← Elab.Tactic.Conv.convert e (withTacticInfoContext (← getRef) (evalTactic code))
          return (← mkEq e e', proof)
        let ((thm, pf), _) ← aux { elaborator := .anonymous } |>.run { goals := [] }
        let fvars := (collectFVars (collectFVars {} thm) pf).fvarIds
        let args := args.filter fun arg => fvars.contains arg.fvarId!
        let thm' ← mkForallFVars args thm
        let pf' ← mkLambdaFVars args pf
        let thm' ← Elab.Term.levelMVarToParam (← instantiateMVars thm')
        if thm'.hasMVar then
          throwError "Theorem has unassigned metavariables{indentD thm'}"
        let pf' ← instantiateMVars pf'
        if pf'.hasLevelMVar then
          throwError "Proof has universe level metavariables{indentD pf'}"
        if pf'.hasMVar then
          throwError "Proof has unassigned metavariables{indentD pf'}"
        let decl ← withRef id do
          Term.expandDeclId (← getCurrNamespace) (← Term.getLevelNames) id mods
        addAndCompile <| Declaration.thmDecl
          { name := decl.declName
            levelParams := decl.levelNames
            type := thm'
            value := pf' }
        -- For hovering on id:
        withSaveInfoContext do
          Term.addTermInfo' id (← mkConstWithLevelParams decl.declName) (isBinder := true)
        -- Process attributes:
        Term.applyAttributesAt decl.declName mods.attrs .afterTypeChecking
        -- Not sure if this is necessary for theorems:
        Term.applyAttributesAt decl.declName mods.attrs .afterCompilation

def f (n : Nat) : Nat :=
  n * 2

def g (n : Nat) : Nat :=
  2 * f n

variable (n : Nat)

@[simp]
transform g_def : g n =>
  unfold g
  unfold f

example : g 2 = 2 * (2 * 2) := by
  simp

#check g_def
-- g_def (n : Nat) : g n = 2 * (n * 2)

def h (n : Nat) : Nat :=
  3 * f n

transform map_g_def : h <$> [1, 2, 3] =>
  simp only [Functor.map, List.map_eq_map, List.map]
  unfold h
  unfold f
  ring_nf

#check map_g_def
-- map_g_def : h <$> [1, 2, 3] = [6, 12, 18]