induction in conv mode

Stream: lean4

[Tomas Skrivan]

I would like to inductively rewrite terms in conv mode. My application would be to compute derivatives of recursively defined functions.

I have a buggy prototype that can do induction over natural numbers. You can rewrite: n+n to Nat.recOn n 0 fun n' xₙ => xₙ + 2 using conv command induction n (simp) (rw[thm1,eq]).

Here is the full code:

code

import Lean
import Qq

open Lean Meta Qq Elab Tactic Conv

syntax (name:=conv_induction) "induction" ident conv conv : conv

@[tactic conv_induction] def convInduction : Tactic
| `(conv| induction $n $baseConv $succConv) => do
  let mvarId ← getMainGoal
  mvarId.withContext do
    let lhs ← getLhs
    let .some decl := (← getLCtx).findFromUserName? n.getId
      | throwError s!"local variable {n} not found"

    let n := Expr.fvar decl.fvarId
    let lhsFun ← mkLambdaFVars #[n] lhs

    let (x₀, eq₀) ← convert (lhsFun.beta #[(.const ``Nat.zero [])]) (Tactic.evalTactic baseConv)

    let (lhs',prf) ←
      withLocalDeclD `n' (.const ``Nat []) fun n' => do
      withLocalDeclD `xₙ (← inferType lhs) fun xₙ' => do
      withLocalDeclD `eq (← mkEq (lhsFun.beta #[n']) xₙ') fun eqₙ' => do

        let (xSucc, eqSucc) ← convert (lhsFun.beta #[(← mkAppM ``Nat.succ #[n'])]) (Tactic.evalTactic succConv)

        let motive := Expr.lam default q(Nat) (← inferType lhs) default
        let base := x₀
        let succ ← mkLambdaFVars #[n',xₙ'] xSucc
        let recDef ← mkLambdaFVars #[n'] (← mkAppOptM ``Nat.recOn #[motive, n', base, succ])

        let motive ← mkLambdaFVars #[n'] ((← inferType eqₙ').replaceFVar xₙ' (recDef.beta #[n']))
        withLocalDeclD `eq (motive.beta #[n']) fun eqₙ'' => do
        let base := eq₀
        let succ ← mkLambdaFVars #[n',eqₙ''] (eqSucc.replaceFVars #[xₙ',eqₙ''] #[recDef.beta #[n'], eqₙ''])
        let recProof ← mkAppOptM ``Nat.recOn #[motive,n,base,succ]

        return (recDef.beta #[n],recProof)

    updateLhs lhs' prf

| _ => throwUnsupportedSyntax

theorem thm1 {n} : n.succ + n.succ = n + n + 2 := sorry

example (n : Nat) : n + n = (Nat.recOn n 0 fun n' xₙ => xₙ + 2) := by
  conv =>
    lhs
    induction n (simp) (rw[thm1,eq])

Unfortunately it produces an error (kernel) declaration has free variables '_example'. What did I do wrong?

Also compiler can't work with Nat.recOn, what should I do to produce executable code? How can I generalize this to any inductive type?

[Kyle Miller]

Check out compile_inductive% in mathlib. It's used to autogenerate compiled definitions for recursors, and for example there's compile_inductive% Nat already in Mathlib.Util.CompileInductive

[Tomas Skrivan]

This is very nice! I just include that file and I can eval #eval (Nat.recOn (motive:=fun _ => Nat) 10 0 fun n' xₙ => xₙ + 2)

[Tomas Skrivan]

I found the mistake, instead of replaceFVars #[xₙ',eqₙ''] there should be replaceFVars #[xₙ',eqₙ'] and the kernel error is gone.