Instantiating type parameters of a polymorphic inductive typ

Stream: metaprogramming / tactics

[Ernest Ng]

Hi! I was wondering how to instantiate type parameters of a polymorphic inductive Prop, e.g.

inductive Eq {α : Sort u_1} : α → α → Prop where ...

I've used getConstInfoInduct to obtain an InductiveVal containing the type of Eq, represented as an Expr. I was wondering if there's a way to "instantiate" α to a concrete type like Nat?

I've tried to use ConstantVal.instantiateTypeLevelParams by doing instantiateValueLevelParams constInfo [mkLevelParam ``Nat], although that ends up instantiating the Sort parameter u_1 as opposed to α.

Any advice on how to instantiate α would be much appreciated, thanks!

[Kyle Miller]

In the end, what you want is to construct the term Expr.app (Expr.const `Eq [levelOne]) (Expr.const `Nat []). There are a number of ways to do this, depending on the level of generality you're looking for.

For example, you could do mkAppOptM `Eq #[Expr.const `Nat []].

Another approach is to use forallMetaBoundedTelescope with the type of Eq and the number of parameters, then use isDefEq on those parameters with what you want them to be. This incidentally solves for the universe levels too, which is nice.

[Kyle Miller]

It'd help to know (1) whether you know which inductive type you want to use ahead of time, or whether you need it to be generic, (2) where are the parameters coming from and why are you instantiating with them, (3) what do you want to do with parameters vs indices (note that Eq has two parameters, not one! The first argument after the colon is promoted to be an index)

[Ernest Ng]

Thanks! (I didn't know about mkAppOptM so this is super helpful!)

For context, I'm working on extending Plausible with the ability to derive generators that only produce random values satisfying some inductively-defined Prop.

To do this, we provide a command #derive_generator to the user -- here's an example:

-- Derives a generator which only produces random lists beginning with 5
#derive_generator (fun (xs : List Nat) => xs = 5 :: tail)

Under the hood, the algorithm for deriving the generator needs to analyze the type of the inductive Prop. This works if the inductive Prop is something like BST below in which there are no polymorphic type parameters:

/-- `BST lo hi t` describes whether a tree `t` is a Binary Search Tree
        containing values strictly within `lo` and `hi` -/
inductive BST : Nat → Nat → Tree → Prop where

However, in the xs = 5 :: tail example above, the inductively-defined Prop is = (Eq), which contains a type parameter α. In the "call-site" of Eq, we know that α ought to be instantiated with List Nat, since we are applying Eq to two arguments of type List Nat in the expression xs = 5 :: tail (my command elaborator has access to the type of the arguments xs and 5::tail). Using this information, I'd like to instantiate α with List Nat. So to answer your questions:

(1) I'd like this approach to be generic (to work with any Prop which is defined as an inductive)
(2) The parameters are coming from user-provided arguments to the Prop

Hope this context helps!

[Kyle Miller]

If you have access to xs = 5 :: tail, then it seems to me that you don't need to instantiate anything: you already have @Eq (List Nat) at the head of the expression.

[Kyle Miller]

Is there a typo in the example? Should the body of the fun be ∃ tail, xs = 5 :: tail?

[Ernest Ng]

Yep, you're right, thanks! The version with ∃ tail is how it ought to be interpreted (tail is allowed to be any random List Nat). (Sidenote: this functionality is meant to be a port of Coq QuickChick, and in Coq, the concrete syntax is Derive Generator for (fun xs => xs = 5 :: tail), so we've replicated the Coq syntax directly, but perhaps this choice of concrete syntax isn't the best).

[Ernest Ng]

I'm using this function to parse the application of the Prop in the body of the fun, and it has trouble recognizing explicit type applications like @Eq (List Nat):

/-- Extracts the name of the induction relation and its arguments
    returning the name of the inductive relation as a `TSyntax term` instead of a `Name`,
    and the arguments to the `inductive` as an `Array` of `TSyntax term`s . -/
def deconstructInductiveApplication (body : Term) : CommandElabM (TSyntax `term × Array (TSyntax `term)) := do
  match body with
  | `($indRel:ident $args:term*) =>
    return (indRel, args)
  | `($indRel:ident) =>
    return (indRel, #[])
  | _ =>
    throwError "Expected inductive type application"

Perhaps this function isn't the most robust -- it has trouble recognizing notation like the = in 5 = x::tail.

[Kyle Miller]

Ah, you're making your own term elaboration system from scratch, and your question basically about how do you do that?

[Robin Arnez]

It seems to me like it would be easier to simply elaborate the term in your case though

[Kyle Miller]

How about you don't build a term elaboration system from scratch and instead make use of the main elaborator, since that way you get all the bells and whistles that it comes with, like hovers, completions, a well-tested system, etc.

It seems really not worth the engineering time not to use elabTerm.

[Robin Arnez]

I guess that won't give you terms though; the question is what are you using them then for?

[Kyle Miller]

Once you use elabTerm, you can then process the Expr you get.

[Kyle Miller]

This is what I meant by the head of the expression will have @Eq (List Nat) — it'll just be there already, so it's not a problem you need to solve.

[Ernest Ng]

Ah yes! I wonder if its better to just elaborate the = in 5 = x::tail into an explicit application Eq @(List Nat) 5 x::tail. If possible, I'd like to stick to manipulating TSyntax terms instead of Expr, since I'm constructing the code for the generator by building up TSyntax terms (via quotations). (I guess I could always delaborate the Expr back into a TSyntax term, but I wasn't sure if elaborating and subsequently delaborating is bad practice.)

[Kyle Miller]

If you need this kind of precise reasoning, then, even if you are constructing Syntax, it's much better to work with Exprs.

[Kyle Miller]

It's not delaboration — it's about using the Exprs and all the type inference that gives you to drive constructing whatever it is that you need.

[Kyle Miller]

Another reason not to make your own term elaboration system is that it's going to diverge in functionality from the normal one. Users won't be happy that these Lean-like terms aren't actually Lean.

[Robin Arnez]

If you want quotation, use Qq. It allows you to write Exprs pretty nicely. The syntax is like this:

import Qq

open Qq

def test (n : Q(Nat)) : Q(Nat) := q($n + 1)

where Q(x) is basically an Expr but with a type annotation.

[Ernest Ng]

Thanks both! Just to make sure I fully understand you @Kyle Miller , are you saying defining a top-level command #derive_generator (fun ... => ...) and elaborating the command is ill-advised, or are you saying the logic for the elaborator should take the argument supplied to #derive_generator and call elabTerm on it to get an Expr, and subsequently we use the information at the Expr-level to proceed?

[Ernest Ng]

Ah yes, we considered using Qq but decided to stick with constructing TSyntax terms since it seems better documented / is easier to construct monadic functions that use do-notation.

[Robin Arnez]

I think he means that you shouldn't try to match on term syntax and use elabTerm or variants instead

[Robin Arnez]

The thing about term quotations vs Qq quotations is that Qq is much more predictable

[Kyle Miller]

Yes, I mean use elabTerm on the expression provided to #derive_generator, and then analyze the Expr you get to drive however you construct the generator.

[Kyle Miller]

@Robin Arnez I don't think Qq helps in this context.

[Ernest Ng]

make sense, thanks!

[Robin Arnez]

Hmm yeah, maybe docs#Lean.Elab.Term.exprToSyntax might help though

[Robin Arnez]

It's basically Expr -> Term but without delaboration

[Robin Arnez]

(it uses metavariables under the hood to make this work)

[Robin Arnez]

But it doesn't work if you actually use it in a top-level command...

[Kyle Miller]

Using elabTerm does mean that implicit quantification is no longer part of it.

If somehow that's important, there are some alternatives. You could for example choose a different syntax that doesn't look like fun. Maybe

#derive_generator xs : List Nat => xs = 5 :: tail

and then you scan what's after => for constants that don't shadow global constants, then replace them with metavariables perhaps (like tail becomes ?tail), then elabTerm that, and then abstract the metavariables to get the quantification.

Or you could decide that

#derive_generator xs : List Nat => ∃ tail, xs = 5 :: tail

is OK and have special support for Exists.

[Kyle Miller]

Robin Arnez said:

It's basically Expr -> Term but without delaboration

It doesn't work with CommandElabM unfortunately. There's no metavariable context.

Something you might consider @Ernest Ng is to not have the logic be in CommandElabM, but in TermElabM, and then create a term elaborator that implements it.

E.g., have the command expand to

instance ... := derive_generator% xs : List Nat => xs = 5 ::tail

and then implement derive_generator%. It's more flexible being in TermElabM for this stuff.

[Kyle Miller]

Some mathlib deriving handlers define such things. One example is the Fintype handler.

[Robin Arnez]

I guess the question is also how you'd expect the derived generator to look like at the end and which parts of that would vary

[Ernest Ng]

Thanks for the suggestions! In the current implementation, the command derives an instance of a typeclass ArbitrarySuchThat -- this typeclass is defined as follows:

/-- Generators of `α` such that `P : α -> Prop` holds for all generated values.
    Note that these generators may fail, which is why they have type `OptionT Gen α`. -/
class ArbitrarySuchThat (α : Type) (P : α → Prop) where
  arbitraryST : OptionT Gen α

so using the current implementation, the command

#derive_generator (fun (t : Tree) => BST lo hi t)

(using the BST example from above) derives the following typeclass instance

instance : ArbitrarySuchThat Tree (fun t => BST lo hi t) where
  arbitraryST := ... -- body of generator emitted

Our desire to derive this typeclass instance was why we began with CommandElabM, but I think your suggestion of having the command expand to instance ... := derive_generator% t : tree => BST lo hi t and sticking to TermElabM for derive_generator% sounds like a better design decision.

[Kyle Miller]

It's common for deriving handlers to start in CommandElabM and switch to TermElabM

Using a term elaborator is just a convenient way to do it, since that way you get to use syntax quotations to make the declaration itself, but still get to create Exprs to build the body as needed.

[Kyle Miller]

Another design here is that you have

#derive_generator funExpression

expand to

instance : ArbitrarySuchThat _ funExpression := derive_arbitrary_such_that%

and then use the expected type to get the predicate.

[Kyle Miller]

That way you're not in the business of elaborating the predicate at all. You do lose a bit of control over elaboration order though doing it this way; if you have derive_arbitrary_such_that% postpone so long as the expected type still has metavariables, then you should be good.

[Ernest Ng]

Ah gotcha thanks! When you say "use the expected type to get the predicate", do you mean let type inference figure out the type of the hole in ArbitrarySuchThat _ funExpression or something else?

[Kyle Miller]

I mean that derive_arbitrary_such_that% can take the expected type, which is an Expr of the form ArbitrarySuchThat t p, and then extract the p argument.

[Ernest Ng]

Ah gotcha that makes sense -- thanks!

[Kyle Miller]

Here's some of the framework:

import Lean

class ArbitrarySuchThat (α : Type) (P : α → Prop) where

open Lean Elab Term

syntax (name := arbitrarySuchThatStx) "arbitrary_such_that%" : term

@[term_elab arbitrarySuchThatStx]
def elabArbitrarySuchThat : TermElab := fun stx expectedType? => do
  let expectedType ← tryPostponeIfHasMVars expectedType? "\
    Could not elaborate `arbitrary_such_that%`"
  let_expr ArbitrarySuchThat ty p ← expectedType
    | throwError "Expected type must be of the form `ArbitrarySuchThat _ _`"
  logInfo m!"\
    type is{indentExpr ty}\n\
    predicate is{indentExpr p}"
  throwError "implementation not finished"

instance : ArbitrarySuchThat _ (fun (xs : List Nat) => ∃ tail, xs = 3 :: tail) :=
  arbitrary_such_that%
/-
type is
  List Nat
predicate is
  fun xs ↦ ∃ tail, xs = 3 :: tail
-/

[Ernest Ng]

Thanks, this is very helpful! I'll summarize our discussion to our collaborators / my manager and let them decide if we ought to make this design change to our tool in the short term (my internship is ending soon, so I'm not sure whether I should undertake the command elaborator -> term elaborator refactor now or let my successor handle it).

[Kyle Miller]

Here's a bit more processing for illustration:

open Lean Elab Term Meta

@[term_elab arbitrarySuchThatStx]
def elabArbitrarySuchThat : TermElab := fun stx expectedType? => do
  let expectedType ← tryPostponeIfHasMVars expectedType? "\
    Could not elaborate `arbitrary_such_that%`"
  let_expr ArbitrarySuchThat ty p ← expectedType
    | throwError "Expected type must be of the form `ArbitrarySuchThat _ _`"
  Meta.withLocalDeclD `x ty fun x => do
    let p' := p.beta #[x]
    logInfo m!"\
      for x : {ty}\n\
      predicate is{indentExpr p'}"
    -- Put into WHNF to identify predicate
    let p' ← whnf p'
    let .const c _ := p'.getAppFn
      | throwError "expecting predicate to be a constant application"
    let ival ← getConstInfoInduct c
    let args := p'.getAppArgs
    let withParams := mkAppN p'.getAppFn args[0...ival.numParams]
    logInfo m!"predicate is {withParams}"
  throwError "implementation not finished"

set_option pp.explicit true
instance : ArbitrarySuchThat _ (fun (xs : List Nat) => xs = [3]) :=
  arbitrary_such_that%
/-
for x : List Nat
predicate is
  @Eq (List Nat) x
    (@List.cons Nat (@OfNat.ofNat Nat (nat_lit 3) (instOfNatNat (nat_lit 3))) (@List.nil Nat))

predicate is @Eq (List Nat) x
-/

[Kyle Miller]

Yeah, definitely you should consider the engineering effort and decide what will serve your needs now/later.

[Ernest Ng]

Thanks for the second example! Super helpful to see some of the term elaborator infrastructure fleshed-out