Constructing a dependent product

Stream: metaprogramming / tactics

[Leni Aniva]

What is the programmatic way of making a dependent product, such as this one?

import Lean

open Lean

#check Σ' n : Nat, n ≠ 0

#eval do
  let e1 ← Elab.Term.elabTerm (← `(term|Nat)) .none
  Meta.withLocalDeclD `x e1 λ fvar => do
    let ident := mkIdent `x
    let e2 ← Elab.Term.elabTerm (← `(term|$(ident) ≠ 0)) (.some $ .sort 0)
    let z ← Meta.mkAppM `PSigma.mk #[e1, e2]
    IO.println s!"{← Meta.ppExpr z}"

In my use case, I have e1, e2 given, and e2 is a function of e1 (or it could just have a loose bvar), but the above process can't construct Σ' n : Nat, n ≠ 0.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

There are a few things going wrong here:

• you are using PSigma.mk, but if you want to construct the type, you should be using PSigma; the former constructs an element of PSigma, i.e., a pair
• Meta.mkAppM tries to fill in the implicit arguments for you, and it assumes that the ones you provided are the explicit args; to pass in the implicits manually, it's easier to use mkAppOptM
• finally, the second argument to PSigma must have arrow type, i.e., must be an abstraction; your e2 uses a free variable in the local context and is not an abstraction; you can use mkLambdaFVars to bind the fvar as a bvar inside an abstraction

Here is the corrected code:

#eval do
  let e1 ← Elab.Term.elabTerm (← `(term|Nat)) .none
  Meta.withLocalDeclD `x e1 λ fvar => do
    let ident := mkIdent `x
    let e2 ← Elab.Term.elabTerm (← `(term|$(ident) ≠ 0)) (.some $ .sort 0)
    let e2Abs ← Meta.mkLambdaFVars #[fvar] e2
    let z ← Meta.mkAppOptM ``PSigma #[e1, e2Abs]
    logInfo m!"{z}"

Btw, not that the terminology is consistent, but Sigmas are usually called dependent sums; the products are the Pis.

[Leni Aniva]

Thanks! I forgot that I can just pass in lambdas