diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index b5dc681e5..d4bec859b 100644 --- a/library/data/int/basic.lean +++ b/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 diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean index 269a87721..b38018af4 100644 --- a/library/data/nat/basic.lean +++ b/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 diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index 111308b6d..f700863d3 100644 --- a/library/data/nat/order.lean +++ b/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) diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean index 30ac0dc1c..b062d4e2b 100644 --- a/library/data/nat/sub.lean +++ b/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 diff --git a/src/emacs/lean-syntax.el b/src/emacs/lean-syntax.el index 93ad60f83..54876e275 100644 --- a/src/emacs/lean-syntax.el +++ b/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") diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 2f03fcebb..b3ca2c368 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/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); diff --git a/src/frontends/lean/token_table.cpp b/src/frontends/lean/token_table.cpp index a8e890012..a135d53da 100644 --- a/src/frontends/lean/token_table.cpp +++ b/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",