feat: type of theorems must be propositions

RELEASES.md

@@ -11,6 +11,8 @@ of each version.
 v4.8.0 (development in progress)
 ---------
 
+* Lean now generates an error if the type of a theorem is **not** a proposition.
+
 * New command `derive_functinal_induction`:
 
   Derived from the definition of a (possibly mutually) recursive function

src/Lean/Elab/MutualDef.lean

@@ -644,6 +644,9 @@ def pushMain (preDefs : Array PreDefinition) (sectionVars : Array Expr) (mainHea
     let termination := termination.rememberExtraParams header.numParams mainVals[i]!
     let value ← mkLambdaFVars sectionVars mainVals[i]!
     let type ← mkForallFVars sectionVars header.type
+    if header.kind.isTheorem then
+      unless (← isProp type) do
+        throwErrorAt header.ref "type of theorem '{header.declName}' is not a proposition{indentExpr type}"
     return preDefs.push {
       ref         := getDeclarationSelectionRef header.ref
       kind        := header.kind

src/Lean/Environment.lean

@@ -230,6 +230,7 @@ inductive KernelException where
   | exprTypeMismatch (env : Environment) (lctx : LocalContext) (expr : Expr) (expectedType : Expr)
   | appTypeMismatch  (env : Environment) (lctx : LocalContext) (app : Expr) (funType : Expr) (argType : Expr)
   | invalidProj      (env : Environment) (lctx : LocalContext) (proj : Expr)
+  | thmTypeIsNotProp (env : Environment) (name : Name) (type : Expr)
   | other            (msg : String)
   | deterministicTimeout
   | excessiveMemory

src/Lean/Message.lean

@@ -366,6 +366,7 @@ def toMessageData (e : KernelException) (opts : Options) : MessageData :=
   | appTypeMismatch  env lctx e fnType argType =>
     mkCtx env lctx opts m!"application type mismatch{indentExpr e}\nargument has type{indentExpr argType}\nbut function has type{indentExpr fnType}"
   | invalidProj env lctx e              => mkCtx env lctx opts m!"(kernel) invalid projection{indentExpr e}"
+  | thmTypeIsNotProp env constName type => mkCtx env {} opts m!"(kernel) type of theorem '{constName}' is not a proposition{indentExpr type}"
   | other msg                           => m!"(kernel) {msg}"
   | deterministicTimeout                => "(kernel) deterministic timeout"
   | excessiveMemory                     => "(kernel) excessive memory consumption detected"

src/kernel/environment.cpp

@@ -178,6 +178,8 @@ environment environment::add_theorem(declaration const & d, bool check) const {
     if (check) {
         // TODO(Leo): we must add support for handling tasks here
         type_checker checker(*this);
+        if (!checker.is_prop(v.get_type()))
+            throw theorem_type_is_not_prop(*this, v.get_name(), v.get_type());
         check_constant_val(*this, v.to_constant_val(), checker);
         check_no_metavar_no_fvar(*this, v.get_name(), v.get_value());
         expr val_type = checker.check(v.get_value(), v.get_lparams());

src/kernel/kernel_exception.h

@@ -66,6 +66,16 @@ public:
     expr const & get_expr() const { return m_expr; }
 };
 
+class theorem_type_is_not_prop : public kernel_exception {
+    name m_name;
+    expr m_type;
+public:
+    theorem_type_is_not_prop(environment const & env, name const & n, expr const & type):
+        kernel_exception(env), m_name(n), m_type(type) {}
+    name const & get_decl_name() const { return m_name; }
+    expr const & get_type() const { return m_type; }
+};
+
 class kernel_exception_with_lctx : public kernel_exception {
     local_ctx m_lctx;
 public:
@@ -185,21 +195,24 @@ object * catch_kernel_exceptions(std::function<A()> const & f) {
     } catch (invalid_proj_exception & ex) {
         // 10 | invalidProj      (env : Environment) (lctx : LocalContext) (proj : Expr)
         return mk_cnstr(0, mk_cnstr(10, ex.env(), ex.get_local_ctx(), ex.get_proj())).steal();
+    } catch (theorem_type_is_not_prop & ex) {
+        // 11 | thmTypeIsNotProp (env : Environment) (name : Name) (type : Expr)
+        return mk_cnstr(0, mk_cnstr(11, ex.env(), ex.get_decl_name(), ex.get_type())).steal();
     } catch (exception & ex) {
-        // 11 | other            (msg : String)
-        return mk_cnstr(0, mk_cnstr(11, string_ref(ex.what()))).steal();
+        // 12 | other            (msg : String)
+        return mk_cnstr(0, mk_cnstr(12, string_ref(ex.what()))).steal();
     } catch (heartbeat_exception & ex) {
-        // 12 | deterministicTimeout
-        return mk_cnstr(0, box(12)).steal();
-    } catch (memory_exception & ex) {
-        // 13 | excessiveMemory
+        // 13 | deterministicTimeout
         return mk_cnstr(0, box(13)).steal();
-    } catch (stack_space_exception & ex) {
-        // 14 | deepRecursion
+    } catch (memory_exception & ex) {
+        // 14 | excessiveMemory
         return mk_cnstr(0, box(14)).steal();
-    } catch (interrupted & ex) {
-        // 15 | interrupted
+    } catch (stack_space_exception & ex) {
+        // 15 | deepRecursion
         return mk_cnstr(0, box(15)).steal();
+    } catch (interrupted & ex) {
+        // 16 | interrupted
+        return mk_cnstr(0, box(16)).steal();
     }
 }
 }

tests/lean/caseSuggestions.lean

@@ -7,7 +7,7 @@
 
 /-!
   This example tests what happens when no cases are available. -/
-theorem noCases : Nat := by
+def noCases : Nat := by
   case nonexistent =>
     skip
 
@@ -15,7 +15,7 @@ theorem noCases : Nat := by
   This example tests what happens when just one case is available, but
   it wasn't picked. -/
 
-theorem oneCase : Nat := by
+def oneCase : Nat := by
   cases ()
   case nonexistent =>
     skip
@@ -24,22 +24,22 @@ theorem oneCase : Nat := by
   Check varying numbers of cases to make sure the pretty-print setup for
   the list is correct. -/
 
-theorem twoCases : Nat := by
+def twoCases : Nat := by
   cases true
   case nonexistent =>
     skip
 
-theorem fourCases : Nat := by
+def fourCases : Nat := by
   cases true <;> cases true
   case nonexistent =>
     skip
 
-theorem eightCases : Nat := by
+def eightCases : Nat := by
   cases true <;> cases true <;> cases true
   case nonexistent =>
     skip
 
-theorem sixteenCases : Nat := by
+def sixteenCases : Nat := by
   cases true <;> cases true <;> cases true <;> cases true
   case nonexistent =>
     skip

tests/lean/levelNGen.lean

@@ -1,6 +0,0 @@
-opaque test1 {α : Sort _} : α → Sort u_1
-#check test1
-def test2 {α : Sort _} : α → Sort u_1 := sorry
-#check test2
-variable {α : Sort _} in theorem test3 : α → Sort _ := sorry
-#check test3

tests/lean/levelNGen.lean.expected.out

@@ -1,5 +0,0 @@
-test1.{u_1, u_2} {α : Sort u_2} : α → Sort u_1
-levelNGen.lean:3:4-3:9: warning: declaration uses 'sorry'
-test2.{u_1, u_2} {α : Sort u_2} : α → Sort u_1
-levelNGen.lean:5:33-5:38: warning: declaration uses 'sorry'
-test3.{u_1, u_2} {α : Sort u_2} : α → Sort u_1

tests/lean/run/contra.lean

@@ -1,46 +1,46 @@
-theorem ex1 (p : Prop) (h1 : p) (h2 : p → False) : α := by
+def ex1 (p : Prop) (h1 : p) (h2 : p → False) : α := by
   contradiction
 
-theorem ex2 (p : Prop) (h1 : p) (h2 : ¬ p) : α := by
+def ex2 (p : Prop) (h1 : p) (h2 : ¬ p) : α := by
   contradiction
 
-theorem ex3 (p : Prop) (h1 : id p) (h2 : ¬ p) : α := by
+def ex3 (p : Prop) (h1 : id p) (h2 : ¬ p) : α := by
   contradiction
 
-theorem ex4 (p : Prop) (h1 : id p) (h2 : id (Not p)) : α := by
+def ex4 (p : Prop) (h1 : id p) (h2 : id (Not p)) : α := by
   contradiction
 
-theorem ex5 (h : x+1 = 0) : α := by
+def ex5 (h : x+1 = 0) : α := by
   contradiction
 
-theorem ex6 (h : 0+0 ≠ 0) : α := by
+def ex6 (h : 0+0 ≠ 0) : α := by
   contradiction
 
-theorem ex7 (x : α) (h : Not (x = x)) : α := by
+def ex7 (x : α) (h : Not (x = x)) : α := by
   contradiction
 
-theorem ex8 (h : 0+0 = 0 → False) : α := by
+def ex8 (h : 0+0 = 0 → False) : α := by
   contradiction
 
-theorem ex9 (h : 10 = 20) : α := by
+def ex9 (h : 10 = 20) : α := by
   contradiction
 
-theorem ex10 (h : [] = [1, 2, 3]) : α := by
+def ex10 (h : [] = [1, 2, 3]) : α := by
   contradiction
 
-theorem ex11 (h : id [] = [1, 2, 3]) : α := by
+def ex11 (h : id [] = [1, 2, 3]) : α := by
   contradiction
 
-theorem ex12 (h : False) : α := by
+def ex12 (h : False) : α := by
   contradiction
 
-theorem ex13 (h : id False) : α := by
+def ex13 (h : id False) : α := by
   contradiction
 
-theorem ex14 (h : 100000000 ≤ 20) : α := by
+def ex14 (h : 100000000 ≤ 20) : α := by
   contradiction
 
-theorem ex15 (x : α) (h : x = x → False) : α := by
+def ex15 (x : α) (h : x = x → False) : α := by
   contradiction
 
 theorem ex16 (xs : List α) (h : xs = [] → False) : Nonempty α := by

tests/lean/run/discrRefinement2.lean

@@ -3,11 +3,11 @@ theorem ex1 {α : Sort u} {a b : α} (h : a ≅ b) : a = b :=
   match h with
   | HEq.refl _ => rfl
 
-theorem ex2 {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} (m : motive a) {β : Sort u2} {b : β} (h : a ≅ b) : motive b :=
+def ex2 {α : Sort u2} {a : α} {motive : {β : Sort u2} → β → Sort u1} (m : motive a) {β : Sort u2} {b : β} (h : a ≅ b) : motive b :=
   match h, m with
   | HEq.refl _, m => m
 
-theorem ex3 {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : a ≅ b) (h₂ : p a) : p b :=
+def ex3 {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : a ≅ b) (h₂ : p a) : p b :=
   match h₁, h₂ with
   | HEq.refl _, h₂ => h₂
 

tests/lean/run/inj2.lean

@@ -24,7 +24,7 @@ by {
   rw [h4]
 }
 
-theorem test4 {α} (v : Fin2 0) : α :=
+def test4 {α} (v : Fin2 0) : α :=
 by cases v
 
 def test5 {α β} {n} (v : Vec2 α β (n+1)) : α := by

tests/lean/run/lazyListRotateUnfoldProof.lean

@@ -30,7 +30,7 @@ theorem rotate_inv {F : LazyList τ} {R : List τ} : (h : F.length + 1 = R.lengt
   | LazyList.cons Fh Ft => sorry
   | LazyList.delayed Ft => sorry
 
-theorem LazyList.ind {α : Type u} {motive : LazyList α → Sort v}
+def LazyList.ind {α : Type u} {motive : LazyList α → Sort v}
         (nil : motive LazyList.nil)
         (cons : (hd : α) → (tl : LazyList α) → motive tl → motive (LazyList.cons hd tl))
         (delayed : (t : Thunk (LazyList α)) → motive t.get → motive (LazyList.delayed t))

tests/lean/run/lemma.lean

@@ -1,8 +1,14 @@
 macro mods:declModifiers "lemma" n:declId sig:declSig val:declVal : command => `($mods:declModifiers theorem $n $sig $val)
 
-lemma fooSimple (n : Nat) : Prop :=
+def fooSimple (n : Nat) : Prop :=
   if n = 0 then True else False
 
-lemma fooPat : Nat → Prop
+lemma fooSimple' : fooSimple 0 :=
+  by constructor
+
+def fooPat : Nat → Prop
   | 0   => True
-  | n+1 => False
+  | _+1 => False
+
+lemma fooPat' : (x : Nat) → fooPat x → x = 0
+  | 0, _ => rfl

tests/lean/run/levelNGen.lean

@@ -0,0 +1,14 @@
+opaque test1 {α : Sort _} : α → Sort u_1
+/-- info: test1.{u_1, u_2} {α : Sort u_2} : α → Sort u_1 -/
+#guard_msgs in
+#check test1
+
+def test2 {α : Sort _} : α → Sort u_1 := sorry
+/-- info: test2.{u_1, u_2} {α : Sort u_2} : α → Sort u_1 -/
+#guard_msgs in
+#check test2
+
+variable {α : Sort _} in def test3 : α → Sort _ := sorry
+/-- info: test3.{u_1, u_2} {α : Sort u_1} : α → Sort u_2 -/
+#guard_msgs in
+#check test3

tests/lean/run/newfrontend3.lean

@@ -9,7 +9,7 @@ def f (h : Nat → ({α : Type} → α → α) × Bool) : Nat :=
 def tst : Nat :=
 f fun n => (fun x => x, true)
 
-theorem ex : id (Nat → Nat) :=
+def ex : id (Nat → Nat) :=
 by {
   intro;
   assumption

tests/lean/run/structuralRec1.lean

@@ -35,7 +35,7 @@ loop as
 
 def pmap2 {α β} (f : α → β) (as : PList α) : PList β :=
 let rec loop : PList α → PList β
- | PList.nil    => PList.nil 
+ | PList.nil    => PList.nil
  | a:::as => f a ::: loop as;
 loop as
 
@@ -58,7 +58,7 @@ match xs with
 | x:::xs =>
   let y := 2 * x;
   match xs with
-  | PList.nil    => PList.nil 
+  | PList.nil    => PList.nil
   | x:::xs => (y + x) ::: pfoo xs
 
 #eval foo [1, 2, 3, 4]
@@ -79,11 +79,11 @@ else
 def pbla (x : Nat) (ys : PList Nat) : PList Nat :=
 if x % 2 == 0 then
   match ys with
-  | PList.nil    => PList.nil 
+  | PList.nil    => PList.nil
   | y:::ys => (y + x/2) ::: pbla (x/2) ys
 else
   match ys with
-  | PList.nil    => PList.nil 
+  | PList.nil    => PList.nil
   | y:::ys => (y + x/2 + 1) ::: pbla (x/2) ys
 
 theorem blaEq (y : Nat) (ys : List Nat) : bla 4 (y::ys) = (y+2) :: bla 2 ys :=
@@ -121,7 +121,7 @@ def pg (xs : PList Nat) : True :=
   | y:::ys =>
     match ys with
     | PList.nil => True.intro
-    | _ => pg ys 
+    | _ => pg ys
 
 def aux : Nat → Nat → Nat
  | 0, y   => y
@@ -157,7 +157,7 @@ axiom F0 : P 0
 axiom F1 : P (F 0)
 axiom FS {n : Nat} : P n → P (F (F n))
 
-axiom T : Nat → Type
+axiom T : Nat → Prop
 axiom TF0 : T 0
 axiom TF1 : T (F 0)
 axiom TFS {n : Nat} : T n → T (F (F n))
@@ -175,13 +175,13 @@ theorem «nested recursion» : ∀ {n}, is_nat n → P n
 -- | _, is_nat.S .(is_nat.Z) => F1
 -- | _, is_nat.S (is_nat.S h) => FS («nested recursion, inaccessible» h)
 
-theorem «reordered discriminants, type» : ∀ n, is_nat_T n → Nat → T n := fun n hn m => 
+theorem «reordered discriminants, type» : ∀ n, is_nat_T n → Nat → T n := fun n hn m =>
 match n, m, hn with
 | _, _, is_nat_T.Z => TF0
 | _, _, is_nat_T.S is_nat_T.Z => TF1
 | _, m, is_nat_T.S (is_nat_T.S h) => TFS («reordered discriminants, type» _ h m)
 
-theorem «reordered discriminants» : ∀ n, is_nat n → Nat → P n := fun n hn m => 
+theorem «reordered discriminants» : ∀ n, is_nat n → Nat → P n := fun n hn m =>
 match n, m, hn with
 | _, _, is_nat.Z => F0
 | _, _, is_nat.S is_nat.Z => F1
@@ -194,8 +194,8 @@ match n, m, hn with
 --   | y::ys =>
 --     match ys with
 --     | List.nil      => True.intro
---     | _::_::zs      => «unsupported nesting» zs 
---     | zs            => «unsupported nesting» ys 
+--     | _::_::zs      => «unsupported nesting» zs
+--     | zs            => «unsupported nesting» ys
 
 def «unsupported nesting, predicate» (xs : PList Nat) : True :=
   match xs with
@@ -203,8 +203,8 @@ def «unsupported nesting, predicate» (xs : PList Nat) : True :=
   | y:::ys =>
     match ys with
     | PList.nil      => True.intro
-    | _:::_:::zs     => «unsupported nesting, predicate» zs 
-    | zs             => «unsupported nesting, predicate» ys 
+    | _:::_:::zs     => «unsupported nesting, predicate» zs
+    | zs             => «unsupported nesting, predicate» ys
 
 
 def f1 (xs : List Nat) : Nat :=
@@ -221,4 +221,4 @@ match xs with
 | x:::xs =>
   match xs with
   | PList.nil  => True.intro
-  | _ => pf1 xs 
+  | _ => pf1 xs

tests/lean/run/tactic1.lean

@@ -1,10 +1,10 @@
-theorem ex1 (x : Nat) (y : { v // v > x }) (z : Nat) : Nat :=
+def ex1 (x : Nat) (y : { v // v > x }) (z : Nat) : Nat :=
 by {
   clear y x;
   exact z
 }
 
-theorem ex2 (x : Nat) (y : { v // v > x }) (z : Nat) : Nat :=
+def ex2 (x : Nat) (y : { v // v > x }) (z : Nat) : Nat :=
 by {
   clear x y;
   exact z

tests/lean/run/thmIsProp.lean

@@ -0,0 +1,57 @@
+import Lean
+
+open Lean
+
+/--
+error: (kernel) type of theorem 'bad' is not a proposition
+  Nat
+-/
+#guard_msgs (error) in
+run_meta do
+  addDecl <| .thmDecl {
+    name        := `bad
+    levelParams := []
+    type        := mkConst ``Nat
+    value       := toExpr 10
+  }
+
+theorem foo : 10 = 10 := rfl
+where aux : Nat := 20
+
+/--
+info: def foo.aux : Nat :=
+20
+-/
+#guard_msgs in
+#print foo.aux
+
+
+theorem foo2 : 10 = 10 :=
+  let rec aux (x : Nat) : Nat := x + 1
+  rfl
+
+/--
+info: def foo2.aux : Nat → Nat :=
+fun x => x + 1
+-/
+#guard_msgs in
+#print foo2.aux
+
+
+/--
+error: type of theorem 'ugly' is not a proposition
+  Nat
+-/
+#guard_msgs (error) in
+theorem ugly : Nat := 10
+
+/--
+error: type of theorem 'g' is not a proposition
+  Nat → Nat
+-/
+#guard_msgs (error) in
+mutual
+theorem f (x : Nat) : x = x := rfl
+
+theorem g (x : Nat) : Nat := x + 1
+end