feat(frontends/lean): check for noncomputability when moving theorems from theorem_queue to environment

library/data/real/division.lean

@@ -641,7 +641,7 @@ theorem lt_or_eq_of_le (x y : ℝ) : x ≤ y → x < y ∨ x = y :=
 theorem le_iff_lt_or_eq (x y : ℝ) : x ≤ y ↔ x < y ∨ x = y :=
   iff.intro (lt_or_eq_of_le x y) (le_of_lt_or_eq x y)
 
-theorem dec_lt : decidable_rel lt :=
+noncomputable definition dec_lt : decidable_rel lt :=
   begin
     rewrite ↑decidable_rel,
     intros,

library/logic/axioms/hilbert.lean

@@ -19,11 +19,11 @@ axiom strong_indefinite_description {A : Type} (P : A → Prop) (H : nonempty A)
 theorem exists_true_of_nonempty {A : Type} (H : nonempty A) : ∃x : A, true :=
 nonempty.elim H (take x, exists.intro x trivial)
 
-theorem inhabited_of_nonempty {A : Type} (H : nonempty A) : inhabited A :=
+noncomputable definition inhabited_of_nonempty {A : Type} (H : nonempty A) : inhabited A :=
 let u : {x | (∃y : A, true) → true} := strong_indefinite_description (λa, true) H in
 inhabited.mk (elt_of u)
 
-theorem inhabited_of_exists {A : Type} {P : A → Prop} (H : ∃x, P x) : inhabited A :=
+noncomputable definition inhabited_of_exists {A : Type} {P : A → Prop} (H : ∃x, P x) : inhabited A :=
 inhabited_of_nonempty (obtain w Hw, from H, nonempty.intro w)
 
 /- the Hilbert epsilon function -/

library/logic/axioms/prop_decidable.lean

@@ -8,16 +8,16 @@ Excluded middle + Hilbert implies every proposition is decidable.
 import logic.axioms.prop_complete logic.axioms.hilbert data.sum
 open decidable inhabited nonempty sum
 
-theorem decidable_inhabited [instance] [priority 0] (a : Prop) : inhabited (decidable a) :=
+noncomputable definition decidable_inhabited [instance] [priority 0] (a : Prop) : inhabited (decidable a) :=
 inhabited_of_nonempty
   (or.elim (em a)
     (assume Ha, nonempty.intro (inl Ha))
     (assume Hna, nonempty.intro (inr Hna)))
 
-theorem prop_decidable [instance] [priority 0] (a : Prop) : decidable a :=
+noncomputable definition prop_decidable [instance] [priority 0] (a : Prop) : decidable a :=
 arbitrary (decidable a)
 
-theorem type_decidable (A : Type) : A + (A → false) :=
+noncomputable definition type_decidable (A : Type) : A + (A → false) :=
 match prop_decidable (nonempty A) with
 | inl Hp := sum.inl (inhabited.value (inhabited_of_nonempty Hp))
 | inr Hn := sum.inr (λ a, absurd (nonempty.intro a) Hn)

src/frontends/lean/parser.cpp

@@ -38,6 +38,7 @@ Author: Leonardo de Moura
 #include "library/sorry.h"
 #include "library/flycheck.h"
 #include "library/pp_options.h"
+#include "library/noncomputable.h"
 #include "library/error_handling/error_handling.h"
 #include "library/tactic/expr_to_tactic.h"
 #include "frontends/lean/tokens.h"
@@ -1898,13 +1899,17 @@ bool parser::parse_commands() {
     }
     commit_info(m_scanner.get_line()+1, 0);
 
-    m_theorem_queue.for_each([&](certified_declaration const & thm) {
-            if (keep_new_thms()) {
-                name const & thm_name = thm.get_declaration().get_name();
-                if (m_env.get(thm_name).is_axiom())
-                    m_env = m_env.replace(thm);
-            }
-        });
+    protected_call(
+        [&]() {
+            m_theorem_queue.for_each([&](certified_declaration const & thm) {
+                    if (keep_new_thms()) {
+                        name const & thm_name = thm.get_declaration().get_name();
+                        if (m_env.get(thm_name).is_axiom())
+                            replace_theorem(thm);
+                    }
+                });
+        },
+        []() {});
     return !m_found_errors;
 }
 
@@ -1934,13 +1939,22 @@ void parser::add_delayed_theorem(certified_declaration const & cd) {
     m_theorem_queue.add(cd);
 }
 
+void parser::replace_theorem(certified_declaration const & thm) {
+    m_env = m_env.replace(thm);
+    name const & thm_name = thm.get_declaration().get_name();
+    if (!check_computable(m_env, thm_name)) {
+        throw exception(sstream() << "declaration '" << thm_name
+                        << "' was marked as a theorem, but it is a noncomputable definition");
+    }
+}
+
 environment parser::reveal_theorems(buffer<name> const & ds) {
     m_theorem_queue.for_each([&](certified_declaration const & thm) {
             if (keep_new_thms()) {
                 name const & thm_name = thm.get_declaration().get_name();
                 if (m_env.get(thm_name).is_axiom() &&
                     std::any_of(ds.begin(), ds.end(), [&](name const & n) { return n == thm_name; })) {
-                    m_env = m_env.replace(thm);
+                    replace_theorem(thm);
                     m_theorem_queue_set.erase(thm_name);
                 }
             }

src/frontends/lean/parser.h

@@ -254,6 +254,8 @@ class parser {
 
     void init_stop_at(options const & opts);
 
+    void replace_theorem(certified_declaration const & thm);
+
 public:
     parser(environment const & env, io_state const & ios,
            std::istream & strm, char const * str_name,

tests/lean/congr_error_msg.lean.expected.out

@@ -7,4 +7,4 @@ congr_error_msg.lean:24:0: error: invalid congruence rule, 'C₆' left-hand-side
 congr_error_msg.lean:27:0: error: invalid congruence rule, 'C₇' argument #2 of parameter #5 contains unresolved parameters
 congr_error_msg.lean:30:0: error: invalid congruence rule, 'C₈' argument #5 is not a valid hypothesis, the left-hand-side contains unresolved parameters
 congr_error_msg.lean:33:0: error: invalid congruence rule, 'C₉' argument #6 is not a valid hypothesis, the right-hand-side must be of the form (m l_1 ... l_n) where m is parameter that was not 'assigned/resolved' yet and l_i's are locals
-congr_error_msg.lean: error: unknown declaration 'C₁'
+congr_error_msg.lean:33:0: error: unknown declaration 'C₁'