michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(frontends/lean): replace '[private]' modifier with 'private

Browse source 
definition' and 'private theorem', '[private]' is not a hint.
This commit is contained in:
Leonardo de Moura 2014-09-19 14:30:02 -07:00
parent 97b1998def
commit 5d8c7fbdf1
7 changed files with 38 additions and 30 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
library/data/vector.lean
View file

@ -35,7 +35,7 @@ namespace vec
(λa, inhabited.destruct iH
(λv, inhabited.mk (vec.cons a v))))
theorem case_zero_lem [private] {C : vec T 0 → Type} {n : ℕ} (v : vec T n) (Hnil : C nil) :
private theorem case_zero_lem {C : vec T 0 → Type} {n : ℕ} (v : vec T n) (Hnil : C nil) :
∀ H : n = 0, C (cast (congr_arg (vec T) H) v) :=
rec_on v (take H : 0 = 0, (eq.rec Hnil (cast_eq _ nil⁻¹)))
(take (x : T) (n : ℕ) (w : vec T n) IH (H : succ n = 0),
@ -44,7 +44,7 @@ namespace vec
theorem case_zero {C : vec T 0 → Type} (v : vec T 0) (Hnil : C nil) : C v :=
eq.rec (case_zero_lem v Hnil (eq.refl 0)) (cast_eq _ v)
theorem rec_nonempty_lem [private] {C : Π{n}, vec T (succ n) → Type} {n : ℕ} (v : vec T n)
private theorem rec_nonempty_lem {C : Π{n}, vec T (succ n) → Type} {n : ℕ} (v : vec T n)
(Hone : Πa, C [a]) (Hcons : Πa {n} (v : vec T (succ n)), C v → C (a :: v))
: ∀{m} (H : n = succ m), C (cast (congr_arg (vec T) H) v) :=
case_on v (take m (H : 0 = succ m), false.rec_type _ (absurd (H⁻¹) succ_ne_zero))
@ -62,7 +62,7 @@ namespace vec
(Hone : Πa, C [a]) (Hcons : Πa {n} (v : vec T (succ n)), C v → C (a :: v)) : C v :=
sorry
theorem case_succ_lem [private] {C : Π{n}, vec T (succ n) → Type} {n : ℕ} (v : vec T n)
private theorem case_succ_lem {C : Π{n}, vec T (succ n) → Type} {n : ℕ} (v : vec T n)
(H : Πa {n} (v : vec T n), C (a :: v))
: ∀{m} (H : n = succ m), C (cast (congr_arg (vec T) H) v) :=
sorry

12
library/logic/axioms/examples/diaconescu.lean
View file

@ -13,17 +13,17 @@ hypothesis propext {a b : Prop} : (a → b) → (b → a) → a = b
parameter p : Prop
definition u [private] := epsilon (λx, x = true ∨ p)
private definition u := epsilon (λx, x = true ∨ p)
definition v [private] := epsilon (λx, x = false ∨ p)
private definition v := epsilon (λx, x = false ∨ p)
lemma u_def [private] : u = true ∨ p :=
private lemma u_def : u = true ∨ p :=
epsilon_spec (exists_intro true (or.inl rfl))
lemma v_def [private] : v = false ∨ p :=
private lemma v_def : v = false ∨ p :=
epsilon_spec (exists_intro false (or.inl rfl))
lemma uv_implies_p [private] : ¬(u = v) ∨ p :=
private lemma uv_implies_p : ¬(u = v) ∨ p :=
or.elim u_def
(assume Hut : u = true, or.elim v_def
(assume Hvf : v = false,
@ -32,7 +32,7 @@ or.elim u_def
(assume Hp : p, or.inr Hp))
(assume Hp : p, or.inr Hp)
lemma p_implies_uv [private] : p → u = v :=
private lemma p_implies_uv : p → u = v :=
assume Hp : p,
have Hpred : (λ x, x = true ∨ p) = (λ x, x = false ∨ p), from
funext (take x : Prop,

6
src/emacs/lean-syntax.el
View file

@ -8,13 +8,13 @@
(require 'rx)
(defconst lean-keywords
'("import" "reducible" "tactic_hint" "opaque" "definition" "renaming"
'("import" "reducible" "tactic_hint" "private" "opaque" "definition" "renaming"
"inline" "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"
"private" "using" "namespace" "builtin" "including" "instance" "class" "section"
"using" "namespace" "builtin" "including" "instance" "class" "section"
"set_option" "add_rewrite" "extends")
"lean keywords")
@ -70,7 +70,7 @@
;; place holder
(,(rx symbol-start "_" symbol-end) . 'font-lock-preprocessor-face)
;; modifiers
(,(rx (or "\[persistent\]" "\[notation\]" "\[visible\]" "\[protected\]" "\[private\]"
(,(rx (or "\[persistent\]" "\[notation\]" "\[visible\]" "\[protected\]"
"\[instance\]" "\[class\]" "\[coercion\]" "\[off\]" "\[none\]" "\[on\]")) . 'font-lock-doc-face)
;; tactics
(,(rx symbol-start

36
src/frontends/lean/decl_cmds.cpp
View file

@ -27,7 +27,7 @@ static name g_rcurly("}");
static name g_colon(":");
static name g_assign(":=");
static name g_definition("definition");
static name g_private("[private]");
static name g_theorem("theorem");
static name g_protected("[protected]");
static name g_instance("[instance]");
static name g_coercion("[coercion]");
@ -162,13 +162,11 @@ environment axiom_cmd(parser & p) {
}
struct decl_modifiers {
bool m_is_private;
bool m_is_protected;
bool m_is_instance;
bool m_is_coercion;
bool m_is_reducible;
decl_modifiers() {
m_is_private = false;
m_is_protected = false;
m_is_instance = false;
m_is_coercion = false;
@ -177,10 +175,7 @@ struct decl_modifiers {
void parse(parser & p) {
while (true) {
if (p.curr_is_token(g_private)) {
m_is_private = true;
p.next();
} else if (p.curr_is_token(g_protected)) {
if (p.curr_is_token(g_protected)) {
m_is_protected = true;
p.next();
} else if (p.curr_is_token(g_instance)) {
@ -209,7 +204,7 @@ static void erase_local_binder_info(buffer<expr> & ps) {
p = update_local(p, binder_info());
}
environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque) {
environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque, bool is_private) {
auto n_pos = p.pos();
unsigned start_line = n_pos.first;
name n = p.check_id_next("invalid declaration, identifier expected");
@ -278,7 +273,7 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque) {
p.declare_sorry();
environment env = p.env();
if (modifiers.m_is_private) {
if (is_private) {
auto env_n = add_private_name(env, n, optional<unsigned>(hash(p.pos().first, p.pos().second)));
env = env_n.first;
real_n = env_n.second;
@ -316,7 +311,7 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque) {
cd = check(env, mk_theorem(real_n, c_ls, c_type, c_value));
else
cd = check(env, mk_definition(env, real_n, c_ls, c_type, c_value, is_opaque));
if (!modifiers.m_is_private)
if (!is_private)
p.add_decl_index(real_n, n_pos, p.get_cmd_token(), c_type);
env = module::add(env, *cd);
found_cached = true;
@ -348,7 +343,7 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque) {
env = module::add(env, check(env, mk_definition(env, real_n, new_ls, type, value, is_opaque)));
p.cache_definition(real_n, pre_type, pre_value, new_ls, type, value);
}
if (!modifiers.m_is_private)
if (!is_private)
p.add_decl_index(real_n, n_pos, p.get_cmd_token(), type);
}
@ -365,14 +360,26 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque) {
return env;
}
environment definition_cmd(parser & p) {
return definition_cmd_core(p, false, false);
return definition_cmd_core(p, false, false, false);
}
environment opaque_definition_cmd(parser & p) {
p.check_token_next(g_definition, "invalid 'opaque' definition, 'definition' expected");
return definition_cmd_core(p, false, true);
return definition_cmd_core(p, false, true, false);
}
environment theorem_cmd(parser & p) {
return definition_cmd_core(p, true, true);
return definition_cmd_core(p, true, true, false);
}
environment private_definition_cmd(parser & p) {
bool is_theorem = false;
if (p.curr_is_token_or_id(g_definition)) {
p.next();
} else if (p.curr_is_token_or_id(g_theorem)) {
p.next();
is_theorem = true;
} else {
throw parser_error("invalid 'private' definition/theorem, 'definition' or 'theorem' expected", p.pos());
}
return definition_cmd_core(p, is_theorem, true, true);
}
static name g_lparen("("), g_lcurly("{"), g_ldcurly("⦃"), g_lbracket("[");
@ -418,6 +425,7 @@ void register_decl_cmds(cmd_table & r) {
add_cmd(r, cmd_info("axiom", "declare a new axiom", axiom_cmd));
add_cmd(r, cmd_info("definition", "add new definition", definition_cmd));
add_cmd(r, cmd_info("opaque", "add new opaque definition", opaque_definition_cmd));
add_cmd(r, cmd_info("private", "add new private definition/theorem", private_definition_cmd));
add_cmd(r, cmd_info("theorem", "add new theorem", theorem_cmd));
add_cmd(r, cmd_info("variables", "declare new parameters", variables_cmd));
}

4
src/frontends/lean/token_table.cpp
View file

@ -77,8 +77,8 @@ token_table init_token_table() {
{"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec}, {"including", 0}, {"sorry", g_max_prec},
{"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec}, {nullptr, 0}};
char const * commands[] = {"theorem", "axiom", "variable", "opaque", "definition", "coercion",
"variables", "[persistent]", "[private]", "[protected]", "[visible]", "[instance]",
char const * commands[] = {"theorem", "axiom", "variable", "private", "opaque", "definition", "coercion",
"variables", "[persistent]", "[protected]", "[visible]", "[instance]",
"[off]", "[on]", "[none]", "[class]", "[coercion]", "[reducible]", "reducible",
"evaluate", "check", "print", "end", "namespace", "section", "import",
"inductive", "record", "renaming", "extends", "structure", "module", "universe",

2
tests/lean/t5.lean
View file

@ -6,7 +6,7 @@ check g
namespace foo
definition h : N := f a
check h
definition q [private] : N := f a
private definition q : N := f a
check q
end foo
check foo.h

2
tests/lean/t7.lean
View file

@ -5,7 +5,7 @@ section
parameter R : A → A → Prop
parameter B : Type
definition id (a : A) : A := a
definition refl [private] : Prop := ∀ (a : A), R a a
private definition refl : Prop := ∀ (a : A), R a a
definition symm : Prop := ∀ (a b : A), R a b → R b a
definition trans : Prop := ∀ (a b c : A), R a b → R b c → R a c
definition equivalence : Prop := and (and refl symm) trans