feat(frontends/lean): add 'irreducible' as syntax sugar for 'reducible [off]'

library/data/int/basic.lean

@@ -206,7 +206,7 @@ exists_intro (pr1 (rep a))
 protected theorem has_decidable_eq [instance] : decidable_eq ℤ :=
 take a b : ℤ, _
 
-reducible [off] int
+irreducible int
 definition of_nat [coercion] (n : ℕ) : ℤ := psub (pair n 0)
 
 theorem eq_zero_intro (n : ℕ) : psub (pair n n) = 0 :=
@@ -323,7 +323,7 @@ or.imp_or (or.swap (proj_zero_or (rep a)))
           ... = -(psub (pair (pr2 (rep a)) 0)) : by simp
           ... = -(of_nat (pr2 (rep a))) : rfl))
 
-reducible [off] int
+irreducible int
 
 ---rename to by_cases in Lean 0.2 (for now using this to avoid name clash)
 theorem int_by_cases {P : ℤ → Prop} (a : ℤ) (H1 : ∀n : ℕ, P (of_nat n)) (H2 : ∀n : ℕ, P (-n)) :
@@ -372,7 +372,7 @@ have H4 : n + m = 0, from
 add_eq_zero H4
 
 --some of these had to be transparent for theorem cases
-reducible [off] psub proj
+irreducible psub proj
 
 -- ## add
 

library/data/nat/basic.lean

@@ -72,7 +72,7 @@ theorem pred_zero : pred 0 = 0
 
 theorem pred_succ {n : ℕ} : pred (succ n) = n
 
-reducible [off] pred
+irreducible pred
 
 theorem zero_or_succ_pred (n : ℕ) : n = 0 ∨ n = succ (pred n) :=
 induction_on n
@@ -154,7 +154,7 @@ theorem add_zero_right {n : ℕ} : n + 0 = n
 
 theorem add_succ_right {n m : ℕ} : n + succ m = succ (n + m)
 
-reducible [off] add
+irreducible add
 
 theorem add_zero_left {n : ℕ} : 0 + n = n :=
 induction_on n
@@ -265,7 +265,7 @@ theorem mul_zero_right {n : ℕ} : n * 0 = 0
 
 theorem mul_succ_right {n m : ℕ} : n * succ m = n * m + n
 
-reducible [off] mul
+irreducible mul
 
 -- ### commutativity, distributivity, associativity, identity
 

library/data/nat/order.lean

@@ -30,7 +30,7 @@ exists_intro k H
 theorem le_elim {n m : ℕ} (H : n ≤ m) : ∃k, n + k = m :=
 H
 
-reducible [off] le
+irreducible le
 
 -- ### partial order (totality is part of less than)
 

library/data/nat/sub.lean

@@ -26,7 +26,7 @@ theorem sub_zero_right {n : ℕ} : n - 0 = n
 
 theorem sub_succ_right {n m : ℕ} : n - succ m = pred (n - m)
 
-reducible [off] sub
+irreducible sub
 
 theorem sub_zero_left {n : ℕ} : 0 - n = 0 :=
 induction_on n sub_zero_right

src/emacs/lean-syntax.el

@@ -8,13 +8,13 @@
 (require 'rx)
 
 (defconst lean-keywords
-  '("import" "reducible" "tactic_hint" "protected" "private" "opaque" "definition" "renaming"
-    "inline" "hiding" "exposing" "parameter" "parameters" "begin" "proof" "qed" "conjecture"
+  '("import" "reducible" "irreducible" "tactic_hint" "protected" "private" "opaque" "definition" "renaming"
+    "hiding" "exposing" "parameter" "parameters" "begin" "proof" "qed" "conjecture"
     "hypothesis" "lemma" "corollary" "variable" "variables" "print" "theorem"
     "context" "open" "as" "export" "axiom" "inductive" "with" "structure" "universe" "alias" "help" "environment"
     "options" "precedence" "postfix" "prefix" "calc_trans" "calc_subst" "calc_refl"
     "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end"
-    "using" "namespace" "builtin" "including" "instance" "class" "section"
+    "using" "namespace" "including" "instance" "class" "section"
     "set_option" "add_rewrite" "extends")
   "lean keywords")
 

src/frontends/lean/builtin_cmds.cpp

@@ -344,6 +344,22 @@ environment reducible_cmd(parser & p) {
     return env;
 }
 
+environment irreducible_cmd(parser & p) {
+    environment env         = p.env();
+    reducible_status status = reducible_status::Off;
+    bool persistent         = false;
+    parse_persistent(p, persistent);
+    bool found = false;
+    while (p.curr_is_identifier()) {
+        name c = p.check_constant_next("invalid 'irreducible' command, constant expected");
+        found   = true;
+        env = set_reducible(env, c, status, persistent);
+    }
+    if (!found)
+        throw exception("invalid empty 'irreducible' command");
+    return env;
+}
+
 environment erase_cache_cmd(parser & p) {
     name n = p.check_id_next("invalid #erase_cache command, identifier expected");
     p.erase_cached_definition(n);
@@ -364,6 +380,7 @@ cmd_table init_cmd_table() {
     add_cmd(r, cmd_info("check",        "type check given expression, and display its type", check_cmd));
     add_cmd(r, cmd_info("coercion",     "add a new coercion", coercion_cmd));
     add_cmd(r, cmd_info("reducible",    "mark definitions as reducible/irreducible for automation", reducible_cmd));
+    add_cmd(r, cmd_info("irreducible",  "mark definitions as irreducible for automation", irreducible_cmd));
     add_cmd(r, cmd_info("#erase_cache", "erase cached definition (for debugging purposes)", erase_cache_cmd));
 
     register_decl_cmds(r);

src/frontends/lean/token_table.cpp

@@ -79,7 +79,7 @@ token_table init_token_table() {
 
     char const * commands[] = {"theorem", "axiom", "variable", "protected", "private", "opaque", "definition", "coercion",
                                "variables", "[persistent]", "[visible]", "[instance]",
-                               "[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "reducible",
+                               "[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "reducible", "irreducible",
                                "evaluate", "check", "print", "end", "namespace", "section", "import",
                                "inductive", "record", "renaming", "extends", "structure", "module", "universe",
                                "precedence", "infixl", "infixr", "infix", "postfix", "prefix", "notation", "context",