Metaprogramming with Expr.isProp

Stream: lean4

[Josh Clune]

Hi! I'm pretty new to metaprogramming and recently realized that the way I was attempting to identify proofs of elements of Prop wasn't fully correct. But although I think that I now understand the issue, I'm still not sure how to actually fix it.

My current code takes a local declaration, looks at the type of its type, and passes it into Expr.isProp. The issue is that Expr.isProp just does a naive check to see whether the argument it was passed is a sort with the level Level.zero. This usually works, but doesn't seem to play nicely with terms that are built from other terms.

For example, in this sample code, hp and hpq are correctly identified by Expr.isProp as being proofs of elements of Prop. But although hq's type's type is printed as Prop, hq's type's type doesn't pass the Expr.isProp test because hq's type's type is listed as a sort with an mvar level.

IsPropExample.lean:

import Lean

open Lean Meta Elab Tactic Term

initialize registerTraceClass `myTactic

def get_level_from_sort (e : Expr) : Option Level :=
  match e with
  | Expr.sort lvl _ => some lvl
  | _ => none

elab "print_type_info" : tactic => do
  withMainContext do
  for fVarId in (← getLCtx).getFVarIds do
    let ldecl ← getLocalDecl fVarId
    trace[myTactic] "{ldecl.userName} type's type: {(← inferType ldecl.type)}"
    trace[myTactic] "{ldecl.userName} type's type is Prop: {(← inferType ldecl.type).isProp}"
    trace[myTactic] "{ldecl.userName} type's type level: {get_level_from_sort (← inferType ldecl.type)}"

Main.lean:

import IsPropExample

set_option trace.myTactic true

example (p q : Prop) (hp : p) (hpq : p → q) : True := by
  have hq := hpq hp
  print_type_info
  sorry

def main : IO Unit := return ()

I'm assuming that somewhere in this approach, I'm missing a step that would instantiate the metavariable in hq's type's type's level, but I don't know what that step should be. What would be the correct way to approach this problem?

[Sebastian Ullrich]

I'm missing a step that would instantiate the metavariable in hq's type's type's level

That step is called Lean.Meta.instantiateMVars :)