Metaprograming baby steps

Stream: lean4

[Cody Roux]

Basic question, as usual. Here's a simplified example of what I'm trying to do, which involves reflection of some non-computable things into syntax.:

import Lean

def MyNat := ℕ

noncomputable def toMyNat : ℕ → MyNat := λ x ↦ x

noncomputable def myPlus : MyNat → MyNat → MyNat := λ x y ↦ Nat.add x y

open Lean

partial def reify : Syntax → Option MyNat
  | `($n:num) => .some $ toMyNat n.getNat
  | `(Nat.add $t $u) => do
    let vt ← reify t
    let vu ← reify u
    .some $ myPlus vt vu
  | _ => .none


#check reify (Syntax.mkApp (mkIdent `Nat.add) #[Syntax.mkNumLit "0", Syntax.mkNumLit "1"])

lemma foo : myPlus (toMyNat 0) (toMyNat 1) = reify (Syntax.mkApp (mkIdent `Nat.add) #[Syntax.mkNumLit "0", Syntax.mkNumLit "1"]) :=
by rfl

Perhaps unsurprisingly, rfl fails. Additionally, the reify definition gives an error:

compiler IR check failed at 'reify', error: unknown declaration 'myPlus'

My high-level questions are:

• Am I going about this all wrong? Should I be using a different type instead of Syntax (maybe Lean.Expr)? Is there a worked example somewhere? I'm trying to stare at "Metaprogramming in Lean", but I'm not sure where to start.
• How would I go about debugging my code? The "guess the value and try rfl" technique is going to stop working pretty quickly I'd guess.

[Kyle Miller]

Here's a diagram that might help with understanding Syntax vs Expr.

I sort of think about this as

1. Lean has an algebraic textual language, but
2. it gets parsed to use a Lisp-like data structure (the Syntax type)
3. and this then gets elaborated into an actual Expr expression, with all the types all worked out.

I don't think anyone uses Syntax for reflection. There aren't really any computations you can do on Syntax directly that you can prove anything about -- the Syntax doesn't "mean" anything except for what it elaborates to. Most of the Lean system works on Exprs, which you can do various computations on.

[Kyle Miller]

Regarding your reify function, you marked myPlus as noncomputable, so in .some $ myPlus vt vu what is it supposed to compute? That "compiler IR check" is trying to say that it can't compile reify into executable code.

[Kyle Miller]

The reduce tactic can sometimes be useful for trying to figure out why rfl doesn't work. But, a big obstruction here is that reify is marked partial, which causes the function to not be something you can prove anything about.

[Cody Roux]

Thanks, this is quite helpful.

[Cody Roux]

Slightly more advanced question:

Suppose I want a tactic to

• Grab the "main" goal
• apply a reify_and_eval : Expr -> Prop function to it
• replace the goal with the result

How would I do this?

what I have:

elab "reify_goal_fol" : tactic =>
 Lean.Elab.Tactic.withMainContext do
  let goal ← Lean.Elab.Tactic.getMainGoal
  let goalDec ← goal.getDecl
  let goalTy := goalDec.type
  dbg_trace f!"goal: {goal.name}"
  let newRepr := reifySentence goalTy
  match newRepr with
  | .ok φ => -- here we want to replace the goal with `eval φ`, say `suffices eval φ by rfl`
  | .error s => Lean.Meta.throwTacticEx `reify_goal_fol goal m!{s}

[Anand Rao Tadipatri]

You could use docs#Lean.MVarId.replaceTargetDefEq to change the target to something that is definitionally equal.

[Cody Roux]

Yes! Now my "final" issue: the target is of type Prop, but it needs to be of type Lean.Expr. I suspect there's some function to get the syntax back out?

[Anand Rao Tadipatri]

If your term of type Prop was produced by applying your reify_and_eval function to the target, you can do mkApp (mkConst ``reify_and_eval []) goalTy to get the new target as an expression.

[Cody Roux]

I'm doing something wrong here: In reality I have a function reify : Expr -> Option MySyntax and a function eval : MySyntax -> Prop. If all goes well reify gType returns a .some syn and eval syn returns something definitionally equal to gType.

But I have to deal with that option type. Surely I'm doing something wrong?

The X/Y problem here: I have a theorem of the form eval Foo <-> Bar which I want to apply, but my goal is not of the form eval Foo.

[Anand Rao Tadipatri]

Maybe you could apply docs#Option.get! on the output of reify to avoid having to keep the Option type (this is probably not the most principled way to deal with it, but it may be good enough for this situation). This will require synthesizing an instance of docs#Inhabited for MySyntax.

[Cody Roux]

Ok, here's the X/Y problem, summarized conveniently with the Qq package:

import Qq

open Lean Qq


inductive BoolTree :=
| trueLeaf : BoolTree
| falseLeaf : BoolTree
| andNode : BoolTree → BoolTree → BoolTree
| orNode : BoolTree → BoolTree → BoolTree
| negNode : BoolTree → BoolTree
deriving Repr

def evalsToTrue (b : BoolTree) : Bool :=
match b with
| .trueLeaf => true
| .falseLeaf => false
| .andNode a b => (evalsToTrue a) && (evalsToTrue b)
| .orNode a b => (evalsToTrue a) || (evalsToTrue b)
| .negNode a => !(evalsToTrue a)

#eval evalsToTrue (.negNode (.andNode .trueLeaf .falseLeaf))

def interp (b : BoolTree) : Prop :=
match b with
| .trueLeaf => True
| .falseLeaf => False
| .andNode a b => (interp a) ∧ (interp b)
| .orNode a b => (interp a) ∨ (interp b)
| .negNode a => ¬ (interp a)

-- tedious but straightforward
theorem evalsToTrue_interp_aux : (evalsToTrue b → interp b) ∧ (evalsToTrue b = false → ¬ interp b) :=
by
  induction b <;> simp [interp, evalsToTrue]
  case andNode ih₁ ih₂ => sorry
  case orNode ih => sorry
  case negNode ih => sorry

theorem evalsToTrue_interp_true : evalsToTrue b → interp b := evalsToTrue_interp_aux.1

-- FIXME: find a better way to do this
def map₂ (f : α → β → γ) (a : Option α) (b : Option β) : Option γ :=
match a, b with
| .some av, .some bv => .some (f av bv)
| _, _ => .none

partial def toInterp (e : Q(Prop)) : MetaM (Option BoolTree) := do
match e with
| ~q(True) => return .some .trueLeaf
| ~q(False) => return .some .falseLeaf
| ~q($a ∧ $b) =>
  let av ← toInterp a
  let bv ← toInterp b
  return map₂ BoolTree.andNode av bv
| ~q($a ∨ $b) =>
  let av ← toInterp a
  let bv ← toInterp b
  return map₂ BoolTree.orNode av bv
| ~q(¬ $a) =>
  let av ← toInterp a
  return Option.map BoolTree.negNode av
| _ => return .none

#eval (toInterp q(True ∧ True ∨ False))

elab "reflect_tac" : tactic =>
 Lean.Elab.Tactic.withMainContext do
 Lean.Elab.Tactic.withMainContext do
  let goal ← Lean.Elab.Tactic.getMainGoal
  let goalDec ← goal.getDecl
  let goalTy := goalDec.type
  dbg_trace f!"goal: {goal.name}"
  match ← toInterp goalTy with
  | .none => dbg_trace f!"Failed to reify"
  | .some tree =>
    let qtree : Q(BoolTree) := q($tree) -- <-- this is the problematic line!
    let newGoal ← MVarId.replaceTargetDefEq goal q(interp $qtree)
    Elab.Tactic.replaceMainGoal [newGoal]

theorem bar : True ∧ True ∨ False := by
  reflect_tac
  apply evalsToTrue_interp_true
  rfl

The issue is that I reify from "meta land" into "object land" and want to be able to go back with a dynamically constructed value. IMHO this is how reflection is done in dependently typed languages, but maybe I'm working against the grain here.

The Option vs not Option is a red herring, I think. @Gabriel Ebner or @Eric Wieser any thoughts?

[Kyle Miller]

For BoolTree, change the deriving line to deriving Repr, ToExpr, assuming you are using Mathlib, which has a ToExpr deriver

[Kyle Miller]

That creates a docs#Lean.ToExpr instance for reifying a runtime value to an Expr

[Kyle Miller]

With that, the proof goes through as-is.

Here's some additional refinement of your tactic though:

elab "reflect_tac" : tactic =>
 Lean.Elab.Tactic.withMainContext do
  let goal ← Lean.Elab.Tactic.getMainGoal
  let goalTy ← goal.getType
  match ← toInterp goalTy with
  | .none => throwError "Failed to reify"
  | .some tree =>
    let qtree : Q(BoolTree) := q($tree)
    let newGoal ← MVarId.replaceTargetDefEq goal q(interp $qtree)
    let [newGoal] ← newGoal.applyConst ``evalsToTrue_interp_true | throwError "Failure applying lemma"
    newGoal.refl

theorem bar : True ∧ True ∨ False := by
  reflect_tac

[Cody Roux]

Thank you this was extraordinarily helpful!