elaboration, inferType, mkExists

Stream: new members

[Mark Aagaard]

I am learning my around elaboration and type inference. As an exercise, I'm trying to write a macro and elaborator to convert foo 5 into ∃ x : Nat, x = 5. I'm having difficulty getting the monads to line up so that the elaborator typechecks.

import Lean
import Lean.Meta

open Lean
open Lean.Elab
open Lean.Elab.Term
open Command
open Meta

syntax (name := foox) "foo" term  : term

-- this returns the argument to `foo`
@[term_elab foox]
def elabFoo1 : TermElab := fun stx typ? => do
  -- throwError s!"entry point: 0={stx[0]} 1={stx[1]} 1.0={stx[1][0]} {typ?}"
  let val := stx[1]
  let mt  := elabTerm val none
  mt

#eval foo 5 -- returns 5

-- this doesn't typecheck, because the result is Expr when it should be TermElabM Expr
def elabFoo2 : Syntax → Option Expr → TermElabM Expr := fun stx typ? => do
  -- throwError s!"entry point: 0={stx[0]} 1={stx[1]} 1.0={stx[1][0]} {typ?}"
  let val := stx[1] -- get the argument to foo
  let mt  := elabTerm val none -- elaborate the argument to get a TermElabM Expr
  let bod ←  mt -- extract the Expr from the monad
  let ty  ←  inferType bod -- infer the type
  let res := Lean.mkForall `x Lean.BinderInfo.default ty bod  -- build the result Expr
  res -- type = Expr, expected type = TermElabM Expr

The second problem is that I haven't found a mkExists that works like mkForall or mkForallEx.

-mark

[Matt Diamond]

At the risk of giving you bad advice: have you considered doing pure res instead of just res?

I have no understanding of your code or metaprogramming in Lean in general, but when it comes to monads, whenever you have a term of type a and you need a term of type m a, often using pure (or return) will do the trick.

[Mark Aagaard]

Matt,
Thanks. Adding in pure led to some progress. The code below type checks, but throws an error.

@[term_elab foox]
def elabFoo1 : TermElab := fun stx typ? => do
  tryPostponeIfNoneOrMVar typ?
  let val := stx[1]
  let bod ← elabTerm val none -- setting expected type to none, bad idea?
  let ty  ← inferType bod
  let res := Lean.mkForall `x Lean.BinderInfo.default ty bod
  pure res

#eval foo 5
-- failed to synthesize instance
--  OfNat (Sort ?u.747) 5

-mark

[Kyle Miller]

The issue here is that you're constructing the expression forall x : ty, 5, and there's no instance that makes 5 : Sort _ make sense.

[Kyle Miller]

Maybe this helps?

syntax (name := foox) "foo" term  : term

@[term_elab foox]
def elabFoo1 : TermElab := fun stx typ? => do
  match stx with
  | `(foo $val) =>
    let bod ← elabTerm val none
    let ty ← inferType bod
    withLocalDeclD `x (mkConst ``Nat) fun x => do
      let eq ← mkEq x bod
      let res ← mkForallFVars #[x] eq
      return res
  | _ => throwUnsupportedSyntax

#check foo 5
-- ∀ (x : Nat), x = 5 : Prop

[Kyle Miller]

(Tip: use #check here instead of #eval, since you aren't wanting to evaluate the expression, just see what it elaborates to.)

[Matt Diamond]

@Kyle Miller would the code be similar to construct ∃ (x : Nat), x = 5? I think that was @Mark Aagaard's next question and tbh I'm kind of curious too

[Kyle Miller]

Yes, the first difference would be to use mkLambdaFVars instead of mkForallFVars, and then you pass that to the last argument of Exists

[Kyle Miller]

syntax (name := foox) "foo" term  : term

@[term_elab foox]
def elabFoo1 : TermElab := fun stx typ? => do
  match stx with
  | `(foo $val) =>
    let bod ← elabTerm val none
    let ty ← inferType bod
    withLocalDeclD `x ty fun x => do
      let eq ← mkEq x bod
      let res ← mkLambdaFVars #[x] eq
      mkAppM ``Exists #[res]
  | _ => throwUnsupportedSyntax

set_option pp.funBinderTypes true
#check foo 5
-- ∃ (x : Nat), x = 5 : Prop

[Mark Aagaard]

Kyle-
Thanks! Your solution is very informative.
-mark

[Michael Bucko]

So the core Elab is Generalize + Change + Rfl + Symm + Rewrite? Then it's the simplification layer - Simp / NormCast / SimpTrace ? Then some automation (like SolveByElim), some logical "features" like FalseOrByContra, induction and some transformation mechanisms (I see 4? Conv, Unfold, Split, Delta)

And then building an elab is essentially accessing the syntax tree, applying transformations, and updating the proof state? (one can also declare the custom syntax)