Distinguishing Type from Prop

Stream: metaprogramming / tactics

[Geoffrey Irving]

If I have a Lean.Expr representing a type, how do I tell what the sort is? I want to distinguish Prop types from Type types.

[Geoffrey Irving]

In particular, Lean.Expr.isProp doesn't do it, as that's for checking if the expr is literally Prop.

[Damiano Testa]

Is the issue that you want to pass ← inferType e to isProp, maybe?

[Geoffrey Irving]

Ah, yep, that seems right.

[Damiano Testa]

(Otherwise, if you could give a #mwe, it would help me understand what the problem is! :smile: )

[Patrick Massot]

That trap gets me every time.

[Damiano Testa]

Same here, which is why it was my first suggestion!

[Eric Wieser]

The docstring for docs#Lean.Expr.isProp is wrong, right?

[Eric Wieser]

There is a bogus "a" that changes the meaning to be the wrong thing

[Geoffrey Irving]

I mean, there can be many sort 0s if you interpret identity as being literal residency in memory. That might have been the thought process.

[Geoffrey Irving]

But yes, that was part of my confusion too.

[Geoffrey Irving]

On reflection, though, you can't tell without being in CoreM or MetaM, though, which is a clue.

[Damiano Testa]

Here is a self-contained example, in case it helps someone else who might stumble here:

import Mathlib.Tactic.RunCmd

open Lean Meta in
run_cmd Elab.Command.liftTermElabM do  -- `(false, true)`
  let tExpr   := .const ``True []
  let notProp := tExpr.isProp
  let isProp  := (← inferType tExpr).isProp
  logInfo m!"{(notProp, isProp)}"

[Eric Wieser]

lean4#3420 fixes the docstring

[Eric Wieser]

I think it's just a copy paste error where all the other functions are referring to families of values

[Eric Wieser]

(a constant, an element of the form $x, etc)

[Damiano Testa]

Eric Wieser said:

lean4#3420 fixes the docstring

I wonder if I should try to maintainer merge it...

[Kevin Buzzard]

I wouldn't bother cluttering up the PR :-)

[Adam Topaz]

FWIW, I quite like the following pattern:

import Lean

def foo : Prop := True

open Lean in
#eval show MetaM Unit from do
  let some c := (← getEnv).find? `foo | unreachable!
  let .sort .zero := c.type | throwError "Not a prop"
  IO.println <| ← Meta.ppExpr c.type

[Adam Topaz]

(no pun intended)

[Kyle Miller]

Generally, you should prefer docs#Lean.Meta.isProp, docs#Lean.Meta.isProof, and docs#Lean.Meta.isType over the ones in the Lean.Expr namespace, unless you know you don't have any metavariables or level parameter reductions to do.

[Adam Topaz]

Oh, I wasn't aware that Meta.isProp existed!

[Eric Wieser]

Should Expr.isProp be renamed, given it means something entirely unrelated to Meta.isProp ?

[Eric Wieser]

(does it even compile to something more useful than the clearer e == .sort .zero?)

[Kyle Miller]

I always get confused by both of them. I wonder if Meta.isProp could be renamed to something that makes it clear that Meta.isProp p is checking that p is a proposition, rather than being Prop itself.

It could be split into Meta.isProp as a parallel to Expr.isProp and perhaps Meta.isProposition, which would be equivalent to Meta.isProp (<- inferType p).

[Kyle Miller]

There's a strong precedent for is in the matching functions to mean that it really is, not is-a

[Kyle Miller]

An alternative name suggestion for Meta.isProposition is Meta.isAProp

[Jannis Limperg]

If you do this renaming (which I'm a fan of), please post a big fat warning somewhere when the behaviour of isProp changes.

[Eric Rodriguez]

Let me say quickly that this thread reminded me to take care on which one to use here - I think if stuff isn't renamed, then docstrings pointing both to each other would be a good idea.