feat: add isPropQuick

It is used to speedup `isProp`.

library/Init/Lean/LBool.lean

@@ -22,6 +22,18 @@ def neg : LBool → LBool
 | false => true
 | undef => undef
 
+def and : LBool → LBool → LBool
+| true,  b  => b
+| a,     _  => a
+
+def beq : LBool → LBool → Bool
+| true,  true  => Bool.true
+| false, false => Bool.true
+| undef, undef => Bool.true
+| _,     _     => Bool.false
+
+instance : HasBeq LBool := ⟨beq⟩
+
 def toString : LBool → String
 | true  => "true"
 | false => "false"

library/Init/Lean/Meta/Default.lean

@@ -53,7 +53,7 @@ exprToBool <$> auxFixpoint isDefEqOp e₁ e₂
 /-          END OF BIG HACK                    -/
 /- =========================================== -/
 
-def isProp (e : Expr) : MetaM Bool :=
+def isProp (e : Expr) : MetaM LBool :=
 isPropAux whnf e
 
 def getFunInfo (fn : Expr) : MetaM FunInfo :=

library/Init/Lean/Meta/FunInfo.lean

@@ -68,7 +68,7 @@ checkFunInfoCache fn maxArgs? $ do
         let pinfo    := updateHasFwdDeps pinfo backDeps;
         pure $ pinfo.push {
           backDeps     := backDeps,
-          prop         := prop,
+          prop         := prop == LBool.true,
           implicit     := decl.binderInfo == BinderInfo.implicit,
           instImplicit := decl.binderInfo == BinderInfo.instImplicit })
       #[];

library/Init/Lean/Meta/InferType.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Init.Lean.LBool
 import Init.Lean.Meta.Basic
 
 namespace Lean
@@ -166,14 +167,75 @@ do s ← get;
     (e : Expr) : MetaM Expr :=
 inferTypeAuxAux (fun e => usingTransparency TransparencyMode.all $ whnf e) e
 
-@[specialize] def isPropAux
-    (whnf : Expr → MetaM Expr)
-    (e : Expr) : MetaM Bool :=
-do type ← inferTypeAux whnf e;
-   type ← whnf type;
-   match type with
-   | Expr.sort Level.zero => pure true
-   | _                    => pure false
+/--
+  Return `LBool.true` if given level is always equivalent to universe level zero.
+  If the given level contains a metavariable, the result may be `LBool.undef` since
+  it depends on metavariable assignment.
+
+  It is used to implement `isProp`. -/
+private def isAlwaysZero : Level → LBool
+| Level.zero     => LBool.true
+| Level.mvar _   => LBool.undef
+| Level.param _  => LBool.false
+| Level.succ _   => LBool.false
+| Level.max u v  => (isAlwaysZero u).and (isAlwaysZero v)
+| Level.imax _ u => isAlwaysZero u
+
+/--
+  `isArrowProp type n` is an "approximate" predicate which returns `LBool.true`
+   if `type` is of the form `A_1 -> ... -> A_n -> Prop`.
+   Remark: `type` can be a dependent arrow. -/
+@[specialize] private partial def isArrowProp : Expr → Nat → MetaM LBool
+| Expr.sort u,          0   => do u ← instantiateLevelMVars u; pure $ isAlwaysZero u
+| Expr.forallE _ _ _ _, 0   => pure LBool.false
+| Expr.forallE _ _ _ b, n+1 => isArrowProp b n
+| Expr.letE _ _ _ b,    n   => isArrowProp b n
+| Expr.mdata _ e,       n   => isArrowProp e n
+| _,                    _   => pure LBool.undef
+
+/--
+  `isPropQuickApp f n` is an "approximate" predicate which returns `LBool.true`
+   if `f` applied to `n` arguments is a proposition. -/
+@[specialize] private partial def isPropQuickApp : Expr → Nat → MetaM LBool
+| Expr.const c lvls, arity   => do constType ← inferConstType c lvls; isArrowProp constType arity
+| Expr.fvar fvarId,  arity   => do fvarType  ← inferFVarType fvarId;  isArrowProp fvarType arity
+| Expr.mvar mvarId,  arity   => do mvarType  ← inferMVarType mvarId;  isArrowProp mvarType arity
+| Expr.app f _,      arity   => isPropQuickApp f (arity+1)
+| Expr.mdata _ e,    arity   => isPropQuickApp e arity
+| Expr.letE _ _ _ b, arity   => isPropQuickApp b arity
+| Expr.lam _ _ _ _,  0       => pure LBool.false
+| Expr.lam _ _ _ b,  arity+1 => isPropQuickApp b arity
+| _,                 _       => pure LBool.undef
+
+/--
+  `isPropQuick e` is an "approximate" predicate which returns `LBool.true`
+  if `e` is a proposition. -/
+@[specialize] private partial def isPropQuick : Expr → MetaM LBool
+| Expr.bvar _           => pure LBool.undef
+| Expr.lit _            => pure LBool.false
+| Expr.sort _           => pure LBool.false
+| Expr.lam _ _ _ _      => pure LBool.false
+| Expr.letE _ _ _ b     => isPropQuick b
+| Expr.proj _ _ _       => pure LBool.undef
+| Expr.forallE _ _ _ b  => isPropQuick b
+| Expr.mdata _ e        => isPropQuick e
+| Expr.const c lvls     => do constType ← inferConstType c lvls; isArrowProp constType 0
+| Expr.fvar fvarId      => do fvarType  ← inferFVarType fvarId;  isArrowProp fvarType 0
+| Expr.mvar mvarId      => do mvarType  ← inferMVarType mvarId;  isArrowProp mvarType 0
+| Expr.app f _          => isPropQuickApp f 1
+
+@[specialize] def isPropAux (whnf : Expr → MetaM Expr) (e : Expr) : MetaM LBool :=
+do r ← isPropQuick e;
+   match r with
+   | LBool.true  => pure LBool.true
+   | LBool.false => pure LBool.false
+   | LBool.undef => do
+     -- dbgTrace ("PropQuick failed " ++ toString e);
+     type ← inferTypeAux whnf e;
+     type ← (fun e => usingTransparency TransparencyMode.all $ whnf e) type;
+     match type with
+     | Expr.sort u => do u ← instantiateLevelMVars u; pure $ isAlwaysZero u
+     | _           => pure LBool.false
 
 end Meta
 end Lean

tests/lean/run/meta1.lean

@@ -14,6 +14,12 @@ do env ← importModules mods;
    | EStateM.Result.ok type s   => IO.println (toString e ++ " ==> " ++ toString type)
    | EStateM.Result.error err _ => throw (IO.userError (toString err))
 
+def tstIsProp (mods : List Name) (e : Expr) : IO Unit :=
+do env ← importModules mods;
+   match isProp e {} { env := env } with
+   | EStateM.Result.ok b s      => IO.println (toString e ++ ", isProp: " ++ toString b)
+   | EStateM.Result.error err _ => throw (IO.userError (toString err))
+
 def t1 : Expr :=
 let map  := Expr.const `List.map [Level.one, Level.one];
 let nat  := Expr.const `Nat [];
@@ -105,3 +111,31 @@ Expr.letE `a (Expr.sort Level.one) nat (Expr.forallE `x BinderInfo.default (Expr
 #eval tstInferType [`Init.Lean.Trace] (Expr.proj `Lean.TraceState 0 (Expr.proj `Inhabited 0 (Expr.const `Lean.TraceState.Inhabited [])))
 #eval tstWHNF [`Init.Lean.Trace] (Expr.proj `Inhabited 0 (Expr.const `Lean.TraceState.Inhabited []))
 #eval tstWHNF [`Init.Lean.Trace] (Expr.proj `Lean.TraceState 0 (Expr.proj `Inhabited 0 (Expr.const `Lean.TraceState.Inhabited [])))
+
+def t10 : Expr :=
+let nat  := Expr.const `Nat [];
+let refl := Expr.app (Expr.const `Eq.refl [Level.one]) nat;
+Expr.lam `a BinderInfo.default nat (Expr.app refl (Expr.bvar 0))
+
+#eval tstInferType [`Init.Core] t10
+#eval tstIsProp [`Init.Core] t10
+
+#eval tstIsProp [`Init.Core] (mkApp (Expr.const `And []) #[Expr.const `True [], Expr.const `True []])
+
+#eval tstIsProp [`Init.Core] (Expr.const `And [])
+
+-- Example where isPropQuick fails
+#eval tstIsProp [`Init.Core] (mkApp (Expr.const `id [Level.zero]) #[Expr.sort Level.zero, mkApp (Expr.const `And []) #[Expr.const `True [], Expr.const
+ `True []]])
+
+#eval tstIsProp [`Init.Core] (mkApp (Expr.const `Eq [Level.one]) #[Expr.const `Nat [], Expr.lit (Literal.natVal 0), Expr.lit (Literal.natVal 1)])
+
+#eval tstIsProp [`Init.Core] $
+  Expr.forallE `x BinderInfo.default (Expr.const `Nat [])
+    (mkApp (Expr.const `Eq [Level.one]) #[Expr.const `Nat [], Expr.bvar 0, Expr.lit (Literal.natVal 1)])
+
+#eval tstIsProp [`Init.Core] $
+  Expr.app
+    (Expr.lam `x BinderInfo.default (Expr.const `Nat [])
+      (mkApp (Expr.const `Eq [Level.one]) #[Expr.const `Nat [], Expr.bvar 0, Expr.lit (Literal.natVal 1)]))
+    (Expr.lit (Literal.natVal 0))