Synthesize a type from instance binder in tactic

Stream: metaprogramming / tactics

[Riyaz Ahuja]

Hi all, I'm working on making a Macaulay2 interface in lean, and one thing I need to do is represent the "real numbers" as defined in M2 (i.e. rationals with a bunch of trancendental functions and constants - pi, exp(), log(), etc.) as a subset of the reals in Lean (and similarly for many other types). I've got all of this working by using Scilean's data_synth, and there's no real hiccups there. Using that, I've been able to define:

class M2Type (T : Type*) (M2T : outParam Type*) where
  toLean : M2T → T
  repr : String

With things like the following to instance it:

noncomputable
instance : M2Type ℝ M2Real where
  toLean e := e.toReal
  repr := "RR"

Now, just as a test, I was able to easily make a function that given the type in lean, returns the corresponding M2Type:

def getM2R {M2R} (R : Type) [M2Type R M2R] : Type :=
  M2R

-- Outputs "M2Real"
#reduce (types := true) getM2R ℝ

Again, no problems just yet. Now, I want to use this in a tactic, where for a MWE I want to be able to run mwe (fun (x:ℝ) => x), and get a Lean.Expr logged with the underlying expression being the type M2Real (and obviously extended for any M2Type R M2R). However, I'm at a loss of how to construct and evaluate this kind of function like getM2R that implicitly depends on being able to synthesize the metavariable, and breaks when it cannot (this failure is fine, as i want the tactic to fail when you feed it something that isn't an M2Type. I have a very naive attempt, but any help on how to approach something like this would be greatly appreciated!

[Riyaz Ahuja]

Here's a MWE:

import SciLean


class M2Type (T : Type*) (M2T : outParam Type*) where
  toLean : M2T → T
  repr : String

namespace RatM2

alias M2Rat := Rat


instance : M2Type ℚ M2Rat where
  toLean e := e
  repr := "QQ"

instance : ToString M2Rat where
  toString r := @toString ℚ instToStringRat r

end RatM2

namespace RealM2

inductive M2Real
| rat (q : ℚ)
| sqrt (x : M2Real)
| log (arg : M2Real)
| exp (x : M2Real)
| pi : M2Real
| add (x y : M2Real) : M2Real
| mul (x y : M2Real) : M2Real
| pow (x y : M2Real) : M2Real
| sub (x y : M2Real) : M2Real
| div (x y : M2Real) : M2Real
  deriving Inhabited, Repr

instance : Inhabited M2Real where
  default := M2Real.rat 0

def toString' (r : M2Real) : String :=
  match r with
  | .rat q => toString q
  | .sqrt x => "sqrt(" ++ toString' x ++ ")"
  | .log arg => "log(" ++ toString' arg ++ ")"
  | .exp x => "exp(" ++ toString' x ++ ")"
  | .pi => "π"
  | .add x y => "(" ++ toString' x ++ " + " ++ toString' y ++ ")"
  | .mul x y => "(" ++ toString' x ++ " * " ++ toString' y ++ ")"
  | .pow x y => "(" ++ toString' x ++ "^" ++ toString' y ++ ")"
  | .sub x y => "(" ++ toString' x ++ " - " ++ toString' y ++ ")"
  | .div x y => "(" ++ toString' x ++ "/" ++ toString' y ++ ")"

instance : ToString M2Real where
  toString r :=  toString' r


noncomputable def M2Real.toReal (r : M2Real)  : ℝ :=
  match r with
  | .rat q => (q : ℝ)
  | .sqrt x => x.toReal.sqrt
  | .log arg => arg.toReal.log
  | .exp x => x.toReal.exp
  | .pi => Real.pi
  | .add x y => x.toReal + y.toReal
  | .mul x y => x.toReal * y.toReal
  | .pow x y => x.toReal ^ y.toReal
  | .sub x y => x.toReal - y.toReal
  | .div x y => x.toReal / y.toReal



noncomputable
instance : M2Type ℝ M2Real where
  toLean e := e.toReal
  repr := "RR"


end RealM2




open RatM2 RealM2 M2Type

@[data_synth out m]
structure LiftM2 {R M2R} [M2Type R M2R] (x : R) (m : M2R) : Prop where
  to_lean : toLean m = x




namespace RatSynthThms

@[data_synth]
theorem lift_rat (q : ℚ) : LiftM2 (q : ℚ) (q : ℚ) where
  to_lean := by simp[M2Type.toLean]

end RatSynthThms


namespace RealSynthThms

@[data_synth]
theorem lift_rat (q : ℚ) : LiftM2 (q : ℝ) (.rat q) where
  to_lean := by simp[M2Real.toReal,M2Type.toLean]

@[data_synth]
theorem lift_sqrt (x : ℝ) (hx : LiftM2 x xe) : LiftM2 (Real.sqrt x : ℝ) (.sqrt xe) where
  to_lean := by have := hx.to_lean; simp_all[M2Real.toReal,hx.to_lean,M2Type.toLean]


@[data_synth]
theorem lift_log (x : ℝ) (hx : LiftM2 x xe) : LiftM2 (Real.log x : ℝ) (.log xe) where
  to_lean := by have := hx.to_lean; simp_all[M2Real.toReal,hx.to_lean,M2Type.toLean]

@[data_synth]
theorem lift_exp (x : ℝ) (hx : LiftM2 x xe) : LiftM2 (Real.exp x : ℝ) (.exp xe) where
  to_lean := by have := hx.to_lean; simp_all[M2Real.toReal,hx.to_lean,M2Type.toLean]

@[data_synth]
theorem lift_pi : LiftM2 (Real.pi : ℝ) (.pi) where
  to_lean := by simp[M2Real.toReal,M2Type.toLean]

@[data_synth]
theorem lift_add (x y : ℝ) (hx : LiftM2 x xe) (hy : LiftM2 y ye) :
  LiftM2 (x + y : ℝ) (.add xe ye) where
  to_lean := by
    have := hx.to_lean
    have := hy.to_lean
    simp_all [M2Real.toReal, hx.to_lean, hy.to_lean,M2Type.toLean]


@[data_synth]
theorem lift_mul (x y : ℝ) (hx : LiftM2 x xe) (hy : LiftM2 y ye) :
  LiftM2 (x * y : ℝ) (.mul xe ye) where
  to_lean := by
    have := hx.to_lean
    have := hy.to_lean
    simp_all [M2Real.toReal, hx.to_lean, hy.to_lean,M2Type.toLean]

@[data_synth]
theorem lift_pow (x y : ℝ) (hx : LiftM2 x xe) (hy : LiftM2 y ye) :
  LiftM2 (x ^ y : ℝ) (.pow xe ye) where
  to_lean := by
    have := hx.to_lean
    have := hy.to_lean
    simp_all [M2Real.toReal, hx.to_lean, hy.to_lean,M2Type.toLean]

@[data_synth]
theorem lift_sub (x y : ℝ) (hx : LiftM2 x xe) (hy : LiftM2 y ye) :
  LiftM2 (x - y : ℝ) (.sub xe ye) where
  to_lean := by
    have := hx.to_lean
    have := hy.to_lean
    simp_all [M2Real.toReal, hx.to_lean, hy.to_lean,M2Type.toLean]

@[data_synth]
theorem lift_div (x y : ℝ) (hx : LiftM2 x xe) (hy : LiftM2 y ye):
  LiftM2 (x / y : ℝ) (.div xe ye) where
  to_lean := by
    have := hx.to_lean
    have := hy.to_lean
    simp_all [M2Real.toReal, hx.to_lean, hy.to_lean,M2Type.toLean]

end RealSynthThms



section Examples

def getM2R {M2R} (R : Type) [M2Type R M2R] : Type :=
  M2R

#reduce (types := true) getM2R ℝ

end Examples



syntax (name:=mweStx) "mwe" term : tactic


open Lean Meta
def checkNoFVars (e : Lean.Expr) (errMsg : Array Lean.Expr → MessageData) : MetaM Unit := do
  let fvarIds := (← e.collectFVars.run {}).2.fvarIds
  if ¬fvarIds.isEmpty then
    throwError (errMsg (fvarIds.map Lean.Expr.fvar))
  pure ()


open Lean Meta in
def _root_.SciLean.Tactic.DataSynth.DataSynthM.runInMetaM (e : SciLean.Tactic.DataSynth.DataSynthM α) : MetaM α := do
  e.runInSimpM.run (← Simp.mkDefaultMethods).toMethodsRef (← Simp.mkContext) (← ST.mkRef {})


open Qq Rat



open Lean Meta Elab Tactic Conv Qq RatM2 in
@[tactic mweStx]
unsafe def mweTactic : Tactic
| `(tactic| mwe $lift:term) => do

  let lift ← elabTerm lift none

  let inputRing : Option Lean.Expr ← match lift with
    | .lam _ type _ _ => do
        let appExpr ← mkAppM ``getM2R #[type]
        let appExpr' ← inferType appExpr
        pure <| some appExpr'
    | _ => pure none


  logInfo s!"infer type of lift: {inputRing.get!.dbgToString}"


  pure ()
| _ =>
  throwUnsupportedSyntax




example (x y z: ℚ) : x^2+y^2 = z^2  := by
  mwe (fun (t:ℚ) => t)
  sorry

[Aaron Liu]

Just looking at this initially it seems like you want to use docs#Lean.Meta.lambdaBoundedTelescope instead of matching on the expression.

[Riyaz Ahuja]

Well, I'm matching on the expression lift in order to extract the type of its domain. So for fun (x:ℝ) => x, I want an expression representing ℝ. Then the idea is I want to run getM2R ℝ, which should return the type M2Real. Then I just want to keep that type as an expression.

[Aaron Liu]

You should still use the telescope, because lift could be an uninstantiated metavariable.

[Aaron Liu]

You want to docs#Lean.Meta.synthInstance the instance, not anything to do with evaluating it.

[Riyaz Ahuja]

Hm ok, and the telescoping would then be useful to get the Expr for the domain of lift? How would i do this, something like: Lean.Meta.lambdaBoundedTelescope lift 1 (fun xs f => ???)

In general, this lift function will always be a ring homomorphism, so I don't think the case of lift being an uninstantiated mvar is really that much of a concern in practice. Honestly for this MWE it would have the same purpose to make the tactic just take in $\mathbb R$ or $\mathbb Q$ as input and do it that way.

[Riyaz Ahuja]

oh that synthInstance looks useful, what expr do i put in as input though?

[Riyaz Ahuja]

Like do i put in the whole getM2R ℝ or?

[Aaron Liu]

It should be one representing M2Type type ?M2T

[Aaron Liu]

Then after the synthInstance finishes, your ?M2T should be assigned to the type you want.

[Riyaz Ahuja]

And i would construct this as mkAppM ``getM2R #[type, q(?M2T)] correct? Or mkAppM ``getM2R #[q(?M2T), type, q(?inst)]?

[Aaron Liu]

You would run docs#Lean.Meta.mkFreshExprMVar and then do the mkAppM with the resulting metavariable.

[Aaron Liu]

let M2T ← mkFreshExprMVar
let instType ← mkAppM ``M2Type #[type, M2T]
let inst ← synthInstance instType
logInfo M2T

[Aaron Liu]

Actually, you can probably just use docs#Lean.mkApp2

[Riyaz Ahuja]

Oh wonderful, that works, thanks!

[Riyaz Ahuja]

Also, one last thing, once i get this M2T as a Expr, is there an easy way to lift it back to a Type inside of the body of the tactic?

[Aaron Liu]

Why do you want is as a Type?

[Aaron Liu]

There is almost nothing useful you can do by having it as a Type.

[Riyaz Ahuja]

Originally when i had hard-coded the use of M2Rat, my tactic would then run:

let mut polynomial : Expr M2Rat := default
  let mut ideal : IdExpr M2Rat := default

  -- elem
  let e ← mkAppM ``LiftExpr #[lift, atoms, elem]
  let (xs,_,_) ← forallMetaTelescope (← inferType e)
  let e := e.beta xs


  let .some goal ← SciLean.Tactic.DataSynth.isDataSynthGoal? e | throwError "invalid goal"
  let .some r ← (SciLean.Tactic.DataSynth.dataSynth goal).runInMetaM
    | throwError m!"failed to lift expression {elem}"

  let result := r.xs[0]!
  checkNoFVars result (fun xs => m!"error: resulting expression contains fvars {xs}")

  try
    let expr ← evalExpr (_root_.Expr M2Rat) q(_root_.Expr M2Rat) result
    polynomial := expr
    logInfo s!"{expr.toString}"
  catch _ =>
    throwError m!"invalid expression {result}"

Where _root_.Expr is a similarly data_synth-defined version of polynomials, that allows for actual polynomial calculations over a certain subset of Polynomial Q (which is normally noncomputable). I need to convert this now to have polynomial be of type _root_.Expr M2T for the evalExpr lifting to work (i.e. converting an object of type Polynomial R into a _root_.Expr M2R).

[Aaron Liu]

What will you do with a _root_.Expr M2R?

[Riyaz Ahuja]

Convert it to a string and use it to send a command to Macaulay2

[Aaron Liu]

You're probably just better converting it to a string before evaluating then

[Aaron Liu]

Like, if you have result, do mkAppM ``toString #[result] and then evalExpr that as a string instead