easy metaprogramming questions

Stream: lean4

[Kevin Buzzard]

As well as not being very good at programming, I'm also not very good at knowing how to learn a programming language; I am always amazed by people who say "I read the source code" -- I just don't know where to start. Forgive me then for the basic question.

I've been reading the metaprogramming tutorial by Arthur and others and I've just about muddled through to the end.

The code just above this URL https://github.com/arthurpaulino/lean4-metaprogramming-book/blob/master/md/main/tactics.md#tweaking-the-context (i.e. the end of the section before that one) is

elab "custom_assump_2" : tactic =>
  Lean.Elab.Tactic.withMainContext do
    let goal ← Lean.Elab.Tactic.getMainGoal
    let goalType ← Lean.Elab.Tactic.getMainTarget
    let ctx ← Lean.MonadLCtx.getLCtx
    let option_matching_expr ← ctx.findDeclM? fun decl: Lean.LocalDecl => do
      let declExpr := decl.toExpr
      let declType ← Lean.Meta.inferType declExpr
      if ← Lean.Meta.isExprDefEq declType goalType
        then return Option.some declExpr
        else return Option.none
    match option_matching_expr with
    | some e => Lean.Elab.Tactic.closeMainGoal e
    | none =>
      Lean.Meta.throwTacticEx `custom_assump_2 goal
        (m!"unable to find matching hypothesis of type ({goalType})")

(this is a walkthrough of building an assumption tactic) and right now I understand the code well enough to just about see what it does (although even that I'm not too clear on -- for example I don't really understand why the program is looping through all the local declarations and not just testing the first one and letting option_matching_expr be none if its type is not equal to the goal type). But I don't understand what's going on well enough to modify it. For example I am being told how to write "if hypothesis type = goal type then close goal" but I do not know how to write "if hypothesis type is a <= _ and goal type is a <= _ then do refine le_trans <hypothesis> _ ". How do I learn about how to ask specific more refined questions about expressions?

[Yakov Pechersky]

Kevin, regarding looping on all of them, I think findDeclM? does exit early on the first match. If it can't find any, you get the none value.

[Arthur Paulino]

So, this involves a trade-off. Let me try to express my thoughts.

First, it's important to say that the current implementation of custom_assump_2 is quite more complicated than it could be (see this version by Sebastian). While it's more complicated, it also exposes more of the API, motivating the reader to do some digging.

Now, the harsh part is that it contains some not-so-simple functional programming monadic tricks, which makes me feel like I'm betraying my own words from the intro chapter. And this makes me feel like simply sticking to Sebastian's implementation.

The trick I'm referring to is exactly what Yakov pointed out. findDeclM does the iteration on the declarations available in the context, moving on while none is being returned by fun decl: Lean.LocalDecl => ... and stopping on the first occurrence of some _.

A more refined question on the iterating expression declType could be made by replacing the if ← Lean.Meta.isExprDefEq declType goalType ... block by the check you want to perform

[Arthur Paulino]

I'd love to have input from more people on the didactic of this part. It takes the reader to a walk and slowly introduces new mechanisms

[Damiano Testa]

I find that an inefficient tactic for a tutorial is not necessarily a bad idea. I really enjoyed Rob Lewis' video where he implements the assumption tactic, by going through the "first attempt everyone would try" and then golfing it. It would be very instructive to have something similar, but I do not know how to do that in a book...

[Arthur Paulino]

Ah, I just realized that I didn't really address Kevin's question.
As far as I know, we don't have pretty syntax sugar for matching expressions in Lean 4 as we do in Lean 3 yet. Gabriel wrote quote4, which does make things easier for that purpose but I don't know if there's a plan to make something like that available from Lean 4 core out of the box.

The easiest answer I know is that we can use matches like in this example from the MetaM chapter:

def matchAndReducing (e : Expr) : MetaM (Option (Expr × Expr)) := do
  let e ← whnf e
  match e with
  | (.app (.app (.const ``And _) P) Q) => return some (P, Q)
  | _ => return none

[Henrik Böving]

To also answer the question about operating more precisely on Exprs here is my take that would work right now...given some patience:

The easiest way for this would of course be to pattern match on expressions... Gabriel has been working on a library that could enable this in the future and there was at least an idea to have it in a usable state by now but I don't think he got there yet (?)

Either way, my approach for figuring out how things that I don't have an idea how they work are is: Try to think where someone might have implemented something similar already and dig in their stuff a bit. For example in this case we want to know how to ask more precise questions about Expr. My first thought would be to either:

1. Check the API docs for Expr for a function that sounds like it might help you (either the docs4#Lean.Expr documentation page and search or just your editors autocompletion). In a fully developed programming language this should work out in the majority of cases but as we know Lean 4 isn't fully there yet so this requires a little more precise idea of what you want to do for now.
2. I know that the ring tactic is already implemented in mathlib4 and that it somehow turns Expr into Horner form and operates on them so they must definitely figure out how the expressions look. And if we go to the source code here: https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/Ring.lean we see that they have a type HornerExpr https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/Ring.lean#L84 quite far up, now I would suspect that they have some function that turns an Expr into a HornerExpr (probably a monadic one because it can fail and what not but never the less such a function does probably exist) so we can grep for a line that contains these words: grep "def .*Expr.*HornerExpr" Ring.lean (of course one could also manually dig the file) and we'll find (among a few others): https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/Ring.lean#L382 and at the core of the translation here we have docs4#Lean.Expr.getAppFnArgs which: Return the function (name) and arguments of an application.

So what we have to do if we want to know whether we have a hyp of the fitting form is:

1. Run the getAppFnArgs on the goal type, check whether the function name is LE.le and remember the first argument (the a in your example)
2. Iterate over our hypothesis, run getAppFnArgs on them as well, check if the function name is LE.le and if their left hand side isExprDefEq to the a we remembered from step 1
3. Apply the hypothesis with refine (where how to apply refine is again found by grepping and searching docs)

And thus I end up with:

import Mathlib
import Lean

open Lean Elab Tactic Meta

elab "kevin_refine_assump" : tactic =>
  -- familiar
  withMainContext do
    let goal ← getMainGoal
    let goalType ← getMainTarget
    -- step 1
    let a ← match Expr.getAppFnArgs goalType with
      | (``LE.le, #[_, _, a, _]) => pure a -- 4 arguments because of implicits
      | _ => throwTacticEx `kevin_refine_assump goal "Goal doesn't match!"
    -- familiar
    let ctx ← Lean.MonadLCtx.getLCtx
    let hyp? ← ctx.findDeclM? fun decl: Lean.LocalDecl => do
      let declType ← Lean.Meta.inferType decl.toExpr
      -- step 2
      match Expr.getAppFnArgs declType with
      | (``LE.le, #[_, _, a_hyp, _]) =>
        if ←isExprDefEq a a_hyp then
          return some decl
        else
          return none
      | _ => return none
    match hyp? with
    | some hyp =>
      -- step 3
      let name := mkIdent hyp.userName
      let stx ← `(le_trans $name _)
      refineCore stx `kevin_refine_assump false -- I found refineCore by looking for "refine" on the docs page
    | none => throwTacticEx `kevin_refine_assump goal "No matching hypothesis found!"

So the general approach to learn something in Lean (and generally in software world) that is not documented and you dont want to ask somebody about how it works is: Try to think of a thing that most likely already does the part you are stuck on and attempt to figure out how they did that.

[Siddhartha Gadgil]

I don't exactly understand what is being sought, but if one wants to match expressions, one powerful way in lean 4 is to create metavariables as holes and use isDefEq. In case this is of the nature intended, below is some code to match an expression for a natural number.

/-- natural number from expression built from `Nat.zero` and `Nat.succ` -/
partial def exprNat : Expr → TermElabM Nat := fun expr =>
  do
    let mvar ←  mkFreshExprMVar (some (mkConst ``Nat))
    let sExp ←  mkAppM ``Nat.succ #[mvar]
    let expr ← reduce expr
    Term.synthesizeSyntheticMVarsNoPostponing
    if ← isDefEq sExp expr then
      Term.synthesizeSyntheticMVarsNoPostponing
      let prev ← exprNat (← whnf mvar)
      return Nat.succ prev
    else
    if ← isDefEq (mkConst `Nat.zero) expr then
      return Nat.zero
    else
      throwError m!"{expr} not a Nat expression"

-- test
elab "nat!" t:term : term => do
  let e ← elabTerm t none
  let n ← exprNat e
  return ToExpr.toExpr n

#eval nat! (123 + 4)  -- 127

[Siddhartha Gadgil]

I should clarify the above is defensive to handle various cases. The line Term.synthesizeSyntheticMVarsNoPostponing can be ignored.

[Kevin Buzzard]

What is being sought is basic understanding! Thanks so much for all these pointers!