Creating Expr objects

Stream: lean4

[Calle Sönne]

I'm trying to learn some basic metaprogramming, and I'm currently trying to understand the implementation of the tacticcancel_denoms in mathlib. I want to experiment a bit with its helper functions, such as findCancelFactor, which takes e : Expr as an argument. Is there a way to conveniently write down non-trivial expressions to test this function, such as for example 5x/10 + 23y/2, without having to manually write down the corresponding Expr object?

[Adam Topaz]

This is what Qq is for.

[Adam Topaz]

import Lean
import Qq

open Lean Qq

open Qq in
example (x y : Q(Rat)) : Q(Rat) :=
  q(5 * $x / 10 + 23 * $y / 3)

example : Q(Rat) = Expr := rfl

[Calle Sönne]

Adam Topaz said:

import Lean
import Qq

open Lean Qq

open Qq in
example (x y : Q(Rat)) : Q(Rat) :=
  q(5 * $x / 10 + 23 * $y / 3)

example : Q(Rat) = Expr := rfl

Amazing, thanks a lot!

[Adam Topaz]

But beware that Qq is unfortunately still difficult to use.

[Calle Sönne]

Yeah, I was just going to ask if there was any place I could read more about it. I came across it before in cancel_denoms but I struggled to find documentation about it then

[Eric Wieser]

I promised at some point to write some tutorial-like documentation for it, but that hasn't happened yet...

[Kyle Miller]

If you want to see how to generate an Expr, you could use the Mathlib ToExpr Expr instance:

import Mathlib.Tactic

open Lean Elab Command Term in
elab "#expr " t:term : command => do
  let e ← liftTermElabM do elabTermAndSynthesize t none
  logInfo m!"{toExpr e}"

#expr fun (x : Rat) => 5*x/10
/-
Lean.Expr.lam `x (Lean.Expr.const `Rat [])
  (((((((Lean.Expr.const `HDiv.hDiv [Lean.Level.zero, Lean.Level.zero, Lean.Level.zero]).app
                        (Lean.Expr.const `Rat [])).app
                    (Lean.Expr.const `Rat [])).app
                (Lean.Expr.const `Rat [])).app
            (((Lean.Expr.const `instHDiv [Lean.Level.zero]).app (Lean.Expr.const `Rat [])).app
              (Lean.Expr.const `Rat.instDiv []))).app
        (((((((Lean.Expr.const `HMul.hMul [Lean.Level.zero, Lean.Level.zero, Lean.Level.zero]).app
                              (Lean.Expr.const `Rat [])).app
                          (Lean.Expr.const `Rat [])).app
                      (Lean.Expr.const `Rat [])).app
                  (((Lean.Expr.const `instHMul [Lean.Level.zero]).app (Lean.Expr.const `Rat [])).app
                    (Lean.Expr.const `Rat.instMul []))).app
              ((((Lean.Expr.const `OfNat.ofNat [Lean.Level.zero]).app (Lean.Expr.const `Rat [])).app
                    (Lean.Expr.lit (Lean.Literal.natVal 5))).app
                ((Lean.Expr.const `Rat.instOfNat []).app (Lean.Expr.lit (Lean.Literal.natVal 5))))).app
          (Lean.Expr.bvar 0))).app
    ((((Lean.Expr.const `OfNat.ofNat [Lean.Level.zero]).app (Lean.Expr.const `Rat [])).app
          (Lean.Expr.lit (Lean.Literal.natVal 10))).app
      ((Lean.Expr.const `Rat.instOfNat []).app (Lean.Expr.lit (Lean.Literal.natVal 10)))))
  Lean.BinderInfo.default
-/

[Yaël Dillies]

Eric Wieser said:

I promised at some point to write some tutorial-like documentation for it, but that hasn't happened yet...

I think this was a shared promise and I'm not out of exams before a month, so...