sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 18:34:06 +00:00
Code Issues Packages Projects Releases Wiki Activity

feat(library): add check_constants.lean validation, cleanup unused names, minor stdlib fixes

Browse Source
This commit is contained in:
Leonardo de Moura
2017-02-21 10:45:31 -08:00
parent 9863755ae1
commit d1d5428808
15 changed files with 528 additions and 287 deletions
Download Patch File Download Diff File Expand all files Collapse all files

10
library/init/data/int/order.lean
View File

@@ -193,7 +193,7 @@ iff.mpr
(int.lt_iff_le_and_ne _ _)
(and.intro hac (assume heq, int.not_le_of_gt begin rw heq, exact hbc end hab))
instance : linear_ordered_ring int :=
instance : decidable_linear_ordered_comm_ring int :=
{ int.comm_ring with
le := int.le,
le_refl := int.le_refl,
@@ -211,7 +211,13 @@ instance : linear_ordered_ring int :=
mul_pos := @int.mul_pos,
le_iff_lt_or_eq := int.le_iff_lt_or_eq,
le_total := int.le_total,
zero_lt_one := int.zero_lt_one }
zero_lt_one := int.zero_lt_one,
decidable_eq := int.decidable_eq,
decidable_le := int.decidable_le,
decidable_lt := int.decidable_lt }
instance : decidable_linear_ordered_comm_group int :=
by apply_instance
end int

2
library/init/meta/environment.lean
View File

@@ -35,6 +35,8 @@ match env^.get d with
| exceptional.success _ := tt
| exceptional.exception ._ _ := ff
end
/- Return tt iff the given name is a namespace -/
meta constant is_namespace : environment → name → bool
/- Add a new inductive datatype to the environment
name, universe parameters, number of parameters, type, constructors (name and type), is_meta -/
meta constant add_inductive : environment → name → list name → nat → expr → list (name × expr) → bool →

28
library/smt/arith.lean
View File

@@ -1,17 +1,21 @@
-- TODO(Leo): remove after we port reals to new stdlib
-- Arithmetic
-- TODO(Leo): remove after we port reals to new stdlib and add int.has_div and int.has_mod
constants (int.has_div : has_div int)
constants (int.has_mod : has_mod int)
attribute [instance] int.has_div int.has_mod
constants (real : Type)
constants (real_has_zero : has_zero real)
constants (real_has_one : has_one real)
constants (real_has_add : has_add real)
constants (real_has_mul : has_mul real)
constants (real_has_sub : has_sub real)
constants (real_has_neg : has_neg real)
constants (real_has_div : has_div real)
constants (real_has_lt : has_lt real)
constants (real_has_le : has_le real)
constants (real.has_zero : has_zero real)
constants (real.has_one : has_one real)
constants (real.has_add : has_add real)
constants (real.has_mul : has_mul real)
constants (real.has_sub : has_sub real)
constants (real.has_neg : has_neg real)
constants (real.has_div : has_div real)
constants (real.has_lt : has_lt real)
constants (real.has_le : has_le real)
attribute [instance] real_has_zero real_has_one real_has_add real_has_mul real_has_sub real_has_neg real_has_div real_has_le real_has_lt
attribute [instance] real.has_zero real.has_one real.has_add real.has_mul real.has_sub real.has_neg real.has_div real.has_le real.has_lt
constants (real.of_int : int → real) (real.to_int : real → int) (real.is_int : real → Prop)

9
script/gen_constants_cpp.py
View File

@@ -36,6 +36,7 @@ def main(argv=None):
basename, ext = os.path.splitext(infile)
cppfile = basename + ".cpp"
hfile = basename + ".h"
tst_file = "../../tests/lean/run/check_" + basename + ".lean"
constants = []
with open(infile, 'r') as f:
for line in f:
@@ -82,6 +83,14 @@ def main(argv=None):
f.write('name const & get_%s_name() { return *g_%s; }\n' % (c[0], c[0]))
# end namespace
f.write('}\n')
with open(tst_file, 'w') as f:
f.write('-- DO NOT EDIT, automatically generated file, generator scripts/gen_constants_cpp.py\n')
f.write("import smt system.io\n")
f.write("open tactic\n");
f.write("meta def script_check_id (n : name) : tactic unit :=\n");
f.write("do env ← get_env, (env^.get n >> return ()) <|> (guard $ env^.is_namespace n) <|> (attribute.get_instances n >> return ()) <|> fail (\"identifier '\" ++ to_string n ++ \"' is not a constant, namespace nor attribute\")\n");
for c in constants:
f.write("run_command script_check_id `%s\n" % c[1])
print("done")
return 0

6
src/frontends/smt2/elaborator.cpp
View File

@@ -110,7 +110,6 @@ static expr mk_chainable_app(buffer<expr> const & args) {
// TODO(dhs): use a macro for this? It scales quadratically.
// At this stage in elaboration: ["@distinct A", arg1, ... ,argN]
static expr mk_distinct_app(buffer<expr> const & args) {
lean_assert(is_constant(app_fn(args[0])) && const_name(app_fn(args[0])) == get_distinct_name());
unsigned num_args = args.size() - 1;
if (num_args == 1)
return mk_constant(get_true_name());
@@ -158,9 +157,8 @@ private:
}
expr elaborate_distinct(buffer<expr> & args) {
lean_assert(is_constant(args[0]) && const_name(args[0]) == get_distinct_name());
expr ty = m_tctx.infer(args[1]);
args[0] = mk_app(mk_constant(get_distinct_name(), {l1()}), ty);
args[0] = mk_app(mk_constant(get_ne_name(), {l1()}), ty);
return mk_distinct_app(args);
}
@@ -182,7 +180,6 @@ private:
}
expr elaborate_select(buffer<expr> & args) {
lean_assert(is_constant(args[0]) && const_name(args[0]) == get_select_name());
expr ty = m_tctx.infer(args[1]);
buffer<expr> array_args;
expr array = get_app_args(ty, array_args);
@@ -192,7 +189,6 @@ private:
}
expr elaborate_store(buffer<expr> & args) {
lean_assert(is_constant(args[0]) && const_name(args[0]) == get_store_name());
expr ty = m_tctx.infer(args[1]);
buffer<expr> array_args;
expr array = get_app_args(ty, array_args);

200
src/library/constants.cpp
View File

@@ -23,7 +23,6 @@ name const * g_bool = nullptr;
name const * g_bool_ff = nullptr;
name const * g_bool_tt = nullptr;
name const * g_bind = nullptr;
name const * g_bv = nullptr;
name const * g_caching_user_attribute = nullptr;
name const * g_cast = nullptr;
name const * g_cast_eq = nullptr;
@@ -44,13 +43,10 @@ name const * g_comm_semiring = nullptr;
name const * g_congr = nullptr;
name const * g_congr_arg = nullptr;
name const * g_congr_fun = nullptr;
name const * g_cyclic_numerals = nullptr;
name const * g_cyclic_numerals_bound = nullptr;
name const * g_decidable = nullptr;
name const * g_decidable_by_contradiction = nullptr;
name const * g_decidable_to_bool = nullptr;
name const * g_discrete_field = nullptr;
name const * g_distinct = nullptr;
name const * g_distrib = nullptr;
name const * g_dite = nullptr;
name const * g_div = nullptr;
@@ -62,13 +58,9 @@ name const * g_Exists = nullptr;
name const * g_eq = nullptr;
name const * g_eq_cases_on = nullptr;
name const * g_eq_drec = nullptr;
name const * g_eq_elim_inv_inv = nullptr;
name const * g_eq_intro = nullptr;
name const * g_eq_mp = nullptr;
name const * g_eq_mpr = nullptr;
name const * g_eq_nrec = nullptr;
name const * g_eq_rec = nullptr;
name const * g_eq_rec_eq = nullptr;
name const * g_eq_refl = nullptr;
name const * g_eq_subst = nullptr;
name const * g_eq_symm = nullptr;
@@ -182,18 +174,11 @@ name const * g_is_associative = nullptr;
name const * g_is_associative_assoc = nullptr;
name const * g_is_commutative = nullptr;
name const * g_is_commutative_comm = nullptr;
name const * g_is_int = nullptr;
name const * g_is_trunc_is_prop = nullptr;
name const * g_is_trunc_is_prop_elim = nullptr;
name const * g_is_trunc_is_set = nullptr;
name const * g_ite = nullptr;
name const * g_left_distrib = nullptr;
name const * g_left_comm = nullptr;
name const * g_le = nullptr;
name const * g_le_refl = nullptr;
name const * g_lift = nullptr;
name const * g_lift_down = nullptr;
name const * g_lift_up = nullptr;
name const * g_linear_ordered_comm_ring = nullptr;
name const * g_linear_ordered_ring = nullptr;
name const * g_linear_ordered_semiring = nullptr;
@@ -201,11 +186,6 @@ name const * g_list = nullptr;
name const * g_list_nil = nullptr;
name const * g_list_cons = nullptr;
name const * g_lt = nullptr;
name const * g_map = nullptr;
name const * g_map_insert = nullptr;
name const * g_map_lookup = nullptr;
name const * g_map_select = nullptr;
name const * g_map_store = nullptr;
name const * g_match_failed = nullptr;
name const * g_mod = nullptr;
name const * g_monad = nullptr;
@@ -231,7 +211,6 @@ name const * g_nat_has_add = nullptr;
name const * g_nat_has_mul = nullptr;
name const * g_nat_has_div = nullptr;
name const * g_nat_has_sub = nullptr;
name const * g_nat_has_neg = nullptr;
name const * g_nat_has_lt = nullptr;
name const * g_nat_has_le = nullptr;
name const * g_nat_add = nullptr;
@@ -362,30 +341,23 @@ name const * g_put_nat = nullptr;
name const * g_to_pexpr = nullptr;
name const * g_quot_mk = nullptr;
name const * g_quot_lift = nullptr;
name const * g_rat_divide = nullptr;
name const * g_rat_of_num = nullptr;
name const * g_rat_of_int = nullptr;
name const * g_real = nullptr;
name const * g_real_has_zero = nullptr;
name const * g_real_has_one = nullptr;
name const * g_real_of_int = nullptr;
name const * g_real_to_int = nullptr;
name const * g_real_is_int = nullptr;
name const * g_real_has_neg = nullptr;
name const * g_real_has_div = nullptr;
name const * g_real_has_add = nullptr;
name const * g_real_has_mul = nullptr;
name const * g_real_has_sub = nullptr;
name const * g_real_has_div = nullptr;
name const * g_real_has_le = nullptr;
name const * g_real_has_lt = nullptr;
name const * g_real_has_neg = nullptr;
name const * g_real_is_int = nullptr;
name const * g_real_of_rat = nullptr;
name const * g_real_of_int = nullptr;
name const * g_real_to_int = nullptr;
name const * g_real_has_le = nullptr;
name const * g_rfl = nullptr;
name const * g_right_distrib = nullptr;
name const * g_ring = nullptr;
name const * g_scope_trace = nullptr;
name const * g_set_of = nullptr;
name const * g_sep = nullptr;
name const * g_select = nullptr;
name const * g_semiring = nullptr;
name const * g_sigma = nullptr;
name const * g_sigma_cases_on = nullptr;
@@ -398,18 +370,12 @@ name const * g_psigma_mk = nullptr;
name const * g_psigma_fst = nullptr;
name const * g_psigma_snd = nullptr;
name const * g_simp = nullptr;
name const * g_simplifier_assoc_subst = nullptr;
name const * g_simplifier_congr_bin_op = nullptr;
name const * g_simplifier_congr_bin_arg1 = nullptr;
name const * g_simplifier_congr_bin_arg2 = nullptr;
name const * g_simplifier_congr_bin_args = nullptr;
name const * g_singleton = nullptr;
name const * g_sizeof = nullptr;
name const * g_smt_array = nullptr;
name const * g_smt_select = nullptr;
name const * g_smt_store = nullptr;
name const * g_smt_prove = nullptr;
name const * g_store = nullptr;
name const * g_string = nullptr;
name const * g_string_empty = nullptr;
name const * g_string_str = nullptr;
@@ -433,7 +399,6 @@ name const * g_psum = nullptr;
name const * g_psum_cases_on = nullptr;
name const * g_psum_inl = nullptr;
name const * g_psum_inr = nullptr;
name const * g_default_smt_config = nullptr;
name const * g_smt_state_mk = nullptr;
name const * g_smt_tactic_execute = nullptr;
name const * g_smt_tactic_execute_with = nullptr;
@@ -450,9 +415,7 @@ name const * g_tactic_interactive_exact = nullptr;
name const * g_trivial = nullptr;
name const * g_thunk = nullptr;
name const * g_to_fmt = nullptr;
name const * g_to_int = nullptr;
name const * g_to_string = nullptr;
name const * g_to_real = nullptr;
name const * g_trans_rel_left = nullptr;
name const * g_trans_rel_right = nullptr;
name const * g_true = nullptr;
@@ -494,7 +457,6 @@ void initialize_constants() {
g_bool_ff = new name{"bool", "ff"};
g_bool_tt = new name{"bool", "tt"};
g_bind = new name{"bind"};
g_bv = new name{"bv"};
g_caching_user_attribute = new name{"caching_user_attribute"};
g_cast = new name{"cast"};
g_cast_eq = new name{"cast_eq"};
@@ -515,13 +477,10 @@ void initialize_constants() {
g_congr = new name{"congr"};
g_congr_arg = new name{"congr_arg"};
g_congr_fun = new name{"congr_fun"};
g_cyclic_numerals = new name{"cyclic_numerals"};
g_cyclic_numerals_bound = new name{"cyclic_numerals", "bound"};
g_decidable = new name{"decidable"};
g_decidable_by_contradiction = new name{"decidable", "by_contradiction"};
g_decidable_to_bool = new name{"decidable", "to_bool"};
g_discrete_field = new name{"discrete_field"};
g_distinct = new name{"distinct"};
g_distrib = new name{"distrib"};
g_dite = new name{"dite"};
g_div = new name{"div"};
@@ -533,13 +492,9 @@ void initialize_constants() {
g_eq = new name{"eq"};
g_eq_cases_on = new name{"eq", "cases_on"};
g_eq_drec = new name{"eq", "drec"};
g_eq_elim_inv_inv = new name{"eq", "elim_inv_inv"};
g_eq_intro = new name{"eq", "intro"};
g_eq_mp = new name{"eq", "mp"};
g_eq_mpr = new name{"eq", "mpr"};
g_eq_nrec = new name{"eq", "nrec"};
g_eq_rec = new name{"eq", "rec"};
g_eq_rec_eq = new name{"eq_rec_eq"};
g_eq_refl = new name{"eq", "refl"};
g_eq_subst = new name{"eq", "subst"};
g_eq_symm = new name{"eq", "symm"};
@@ -643,7 +598,7 @@ void initialize_constants() {
g_int_ne_neg_of_pos = new name{"int", "ne_neg_of_pos"};
g_int_neg_ne_zero_of_ne = new name{"int", "neg_ne_zero_of_ne"};
g_int_zero_ne_neg_of_ne = new name{"int", "zero_ne_neg_of_ne"};
g_int_decidable_linear_ordered_comm_group = new name{"int_decidable_linear_ordered_comm_group"};
g_int_decidable_linear_ordered_comm_group = new name{"int", "decidable_linear_ordered_comm_group"};
g_interactive_parse = new name{"interactive", "parse"};
g_inv = new name{"inv"};
g_io = new name{"io"};
@@ -653,18 +608,11 @@ void initialize_constants() {
g_is_associative_assoc = new name{"is_associative", "assoc"};
g_is_commutative = new name{"is_commutative"};
g_is_commutative_comm = new name{"is_commutative", "comm"};
g_is_int = new name{"is_int"};
g_is_trunc_is_prop = new name{"is_trunc", "is_prop"};
g_is_trunc_is_prop_elim = new name{"is_trunc", "is_prop", "elim"};
g_is_trunc_is_set = new name{"is_trunc", "is_set"};
g_ite = new name{"ite"};
g_left_distrib = new name{"left_distrib"};
g_left_comm = new name{"left_comm"};
g_le = new name{"le"};
g_le_refl = new name{"le", "refl"};
g_lift = new name{"lift"};
g_lift_down = new name{"lift", "down"};
g_lift_up = new name{"lift", "up"};
g_le_refl = new name{"le_refl"};
g_linear_ordered_comm_ring = new name{"linear_ordered_comm_ring"};
g_linear_ordered_ring = new name{"linear_ordered_ring"};
g_linear_ordered_semiring = new name{"linear_ordered_semiring"};
@@ -672,11 +620,6 @@ void initialize_constants() {
g_list_nil = new name{"list", "nil"};
g_list_cons = new name{"list", "cons"};
g_lt = new name{"lt"};
g_map = new name{"map"};
g_map_insert = new name{"map", "insert"};
g_map_lookup = new name{"map", "lookup"};
g_map_select = new name{"map", "select"};
g_map_store = new name{"map", "store"};
g_match_failed = new name{"match_failed"};
g_mod = new name{"mod"};
g_monad = new name{"monad"};
@@ -702,7 +645,6 @@ void initialize_constants() {
g_nat_has_mul = new name{"nat", "has_mul"};
g_nat_has_div = new name{"nat", "has_div"};
g_nat_has_sub = new name{"nat", "has_sub"};
g_nat_has_neg = new name{"nat", "has_neg"};
g_nat_has_lt = new name{"nat", "has_lt"};
g_nat_has_le = new name{"nat", "has_le"};
g_nat_add = new name{"nat", "add"};
@@ -833,30 +775,23 @@ void initialize_constants() {
g_to_pexpr = new name{"to_pexpr"};
g_quot_mk = new name{"quot", "mk"};
g_quot_lift = new name{"quot", "lift"};
g_rat_divide = new name{"rat", "divide"};
g_rat_of_num = new name{"rat", "of_num"};
g_rat_of_int = new name{"rat", "of_int"};
g_real = new name{"real"};
g_real_has_zero = new name{"real", "has_zero"};
g_real_has_one = new name{"real", "has_one"};
g_real_of_int = new name{"real", "of_int"};
g_real_to_int = new name{"real", "to_int"};
g_real_is_int = new name{"real", "is_int"};
g_real_has_neg = new name{"real", "has_neg"};
g_real_has_div = new name{"real", "has_div"};
g_real_has_add = new name{"real", "has_add"};
g_real_has_mul = new name{"real", "has_mul"};
g_real_has_sub = new name{"real", "has_sub"};
g_real_has_div = new name{"real", "has_div"};
g_real_has_le = new name{"real", "has_le"};
g_real_has_lt = new name{"real", "has_lt"};
g_real_has_neg = new name{"real", "has_neg"};
g_real_is_int = new name{"real", "is_int"};
g_real_of_rat = new name{"real", "of_rat"};
g_real_of_int = new name{"real", "of_int"};
g_real_to_int = new name{"real", "to_int"};
g_real_has_le = new name{"real", "has_le"};
g_rfl = new name{"rfl"};
g_right_distrib = new name{"right_distrib"};
g_ring = new name{"ring"};
g_scope_trace = new name{"scope_trace"};
g_set_of = new name{"set_of"};
g_sep = new name{"sep"};
g_select = new name{"select"};
g_semiring = new name{"semiring"};
g_sigma = new name{"sigma"};
g_sigma_cases_on = new name{"sigma", "cases_on"};
@@ -869,18 +804,12 @@ void initialize_constants() {
g_psigma_fst = new name{"psigma", "fst"};
g_psigma_snd = new name{"psigma", "snd"};
g_simp = new name{"simp"};
g_simplifier_assoc_subst = new name{"simplifier", "assoc_subst"};
g_simplifier_congr_bin_op = new name{"simplifier", "congr_bin_op"};
g_simplifier_congr_bin_arg1 = new name{"simplifier", "congr_bin_arg1"};
g_simplifier_congr_bin_arg2 = new name{"simplifier", "congr_bin_arg2"};
g_simplifier_congr_bin_args = new name{"simplifier", "congr_bin_args"};
g_singleton = new name{"singleton"};
g_sizeof = new name{"sizeof"};
g_smt_array = new name{"smt", "array"};
g_smt_select = new name{"smt", "select"};
g_smt_store = new name{"smt", "store"};
g_smt_prove = new name{"smt", "prove"};
g_store = new name{"store"};
g_string = new name{"string"};
g_string_empty = new name{"string", "empty"};
g_string_str = new name{"string", "str"};
@@ -904,7 +833,6 @@ void initialize_constants() {
g_psum_cases_on = new name{"psum", "cases_on"};
g_psum_inl = new name{"psum", "inl"};
g_psum_inr = new name{"psum", "inr"};
g_default_smt_config = new name{"default_smt_config"};
g_smt_state_mk = new name{"smt_state", "mk"};
g_smt_tactic_execute = new name{"smt_tactic", "execute"};
g_smt_tactic_execute_with = new name{"smt_tactic", "execute_with"};
@@ -921,9 +849,7 @@ void initialize_constants() {
g_trivial = new name{"trivial"};
g_thunk = new name{"thunk"};
g_to_fmt = new name{"to_fmt"};
g_to_int = new name{"to_int"};
g_to_string = new name{"to_string"};
g_to_real = new name{"to_real"};
g_trans_rel_left = new name{"trans_rel_left"};
g_trans_rel_right = new name{"trans_rel_right"};
g_true = new name{"true"};
@@ -966,7 +892,6 @@ void finalize_constants() {
delete g_bool_ff;
delete g_bool_tt;
delete g_bind;
delete g_bv;
delete g_caching_user_attribute;
delete g_cast;
delete g_cast_eq;
@@ -987,13 +912,10 @@ void finalize_constants() {
delete g_congr;
delete g_congr_arg;
delete g_congr_fun;
delete g_cyclic_numerals;
delete g_cyclic_numerals_bound;
delete g_decidable;
delete g_decidable_by_contradiction;
delete g_decidable_to_bool;
delete g_discrete_field;
delete g_distinct;
delete g_distrib;
delete g_dite;
delete g_div;
@@ -1005,13 +927,9 @@ void finalize_constants() {
delete g_eq;
delete g_eq_cases_on;
delete g_eq_drec;
delete g_eq_elim_inv_inv;
delete g_eq_intro;
delete g_eq_mp;
delete g_eq_mpr;
delete g_eq_nrec;
delete g_eq_rec;
delete g_eq_rec_eq;
delete g_eq_refl;
delete g_eq_subst;
delete g_eq_symm;
@@ -1125,18 +1043,11 @@ void finalize_constants() {
delete g_is_associative_assoc;
delete g_is_commutative;
delete g_is_commutative_comm;
delete g_is_int;
delete g_is_trunc_is_prop;
delete g_is_trunc_is_prop_elim;
delete g_is_trunc_is_set;
delete g_ite;
delete g_left_distrib;
delete g_left_comm;
delete g_le;
delete g_le_refl;
delete g_lift;
delete g_lift_down;
delete g_lift_up;
delete g_linear_ordered_comm_ring;
delete g_linear_ordered_ring;
delete g_linear_ordered_semiring;
@@ -1144,11 +1055,6 @@ void finalize_constants() {
delete g_list_nil;
delete g_list_cons;
delete g_lt;
delete g_map;
delete g_map_insert;
delete g_map_lookup;
delete g_map_select;
delete g_map_store;
delete g_match_failed;
delete g_mod;
delete g_monad;
@@ -1174,7 +1080,6 @@ void finalize_constants() {
delete g_nat_has_mul;
delete g_nat_has_div;
delete g_nat_has_sub;
delete g_nat_has_neg;
delete g_nat_has_lt;
delete g_nat_has_le;
delete g_nat_add;
@@ -1305,30 +1210,23 @@ void finalize_constants() {
delete g_to_pexpr;
delete g_quot_mk;
delete g_quot_lift;
delete g_rat_divide;
delete g_rat_of_num;
delete g_rat_of_int;
delete g_real;
delete g_real_has_zero;
delete g_real_has_one;
delete g_real_of_int;
delete g_real_to_int;
delete g_real_is_int;
delete g_real_has_neg;
delete g_real_has_div;
delete g_real_has_add;
delete g_real_has_mul;
delete g_real_has_sub;
delete g_real_has_div;
delete g_real_has_le;
delete g_real_has_lt;
delete g_real_has_neg;
delete g_real_is_int;
delete g_real_of_rat;
delete g_real_of_int;
delete g_real_to_int;
delete g_real_has_le;
delete g_rfl;
delete g_right_distrib;
delete g_ring;
delete g_scope_trace;
delete g_set_of;
delete g_sep;
delete g_select;
delete g_semiring;
delete g_sigma;
delete g_sigma_cases_on;
@@ -1341,18 +1239,12 @@ void finalize_constants() {
delete g_psigma_fst;
delete g_psigma_snd;
delete g_simp;
delete g_simplifier_assoc_subst;
delete g_simplifier_congr_bin_op;
delete g_simplifier_congr_bin_arg1;
delete g_simplifier_congr_bin_arg2;
delete g_simplifier_congr_bin_args;
delete g_singleton;
delete g_sizeof;
delete g_smt_array;
delete g_smt_select;
delete g_smt_store;
delete g_smt_prove;
delete g_store;
delete g_string;
delete g_string_empty;
delete g_string_str;
@@ -1376,7 +1268,6 @@ void finalize_constants() {
delete g_psum_cases_on;
delete g_psum_inl;
delete g_psum_inr;
delete g_default_smt_config;
delete g_smt_state_mk;
delete g_smt_tactic_execute;
delete g_smt_tactic_execute_with;
@@ -1393,9 +1284,7 @@ void finalize_constants() {
delete g_trivial;
delete g_thunk;
delete g_to_fmt;
delete g_to_int;
delete g_to_string;
delete g_to_real;
delete g_trans_rel_left;
delete g_trans_rel_right;
delete g_true;
@@ -1437,7 +1326,6 @@ name const & get_bool_name() { return *g_bool; }
name const & get_bool_ff_name() { return *g_bool_ff; }
name const & get_bool_tt_name() { return *g_bool_tt; }
name const & get_bind_name() { return *g_bind; }
name const & get_bv_name() { return *g_bv; }
name const & get_caching_user_attribute_name() { return *g_caching_user_attribute; }
name const & get_cast_name() { return *g_cast; }
name const & get_cast_eq_name() { return *g_cast_eq; }
@@ -1458,13 +1346,10 @@ name const & get_comm_semiring_name() { return *g_comm_semiring; }
name const & get_congr_name() { return *g_congr; }
name const & get_congr_arg_name() { return *g_congr_arg; }
name const & get_congr_fun_name() { return *g_congr_fun; }
name const & get_cyclic_numerals_name() { return *g_cyclic_numerals; }
name const & get_cyclic_numerals_bound_name() { return *g_cyclic_numerals_bound; }
name const & get_decidable_name() { return *g_decidable; }
name const & get_decidable_by_contradiction_name() { return *g_decidable_by_contradiction; }
name const & get_decidable_to_bool_name() { return *g_decidable_to_bool; }
name const & get_discrete_field_name() { return *g_discrete_field; }
name const & get_distinct_name() { return *g_distinct; }
name const & get_distrib_name() { return *g_distrib; }
name const & get_dite_name() { return *g_dite; }
name const & get_div_name() { return *g_div; }
@@ -1476,13 +1361,9 @@ name const & get_Exists_name() { return *g_Exists; }
name const & get_eq_name() { return *g_eq; }
name const & get_eq_cases_on_name() { return *g_eq_cases_on; }
name const & get_eq_drec_name() { return *g_eq_drec; }
name const & get_eq_elim_inv_inv_name() { return *g_eq_elim_inv_inv; }
name const & get_eq_intro_name() { return *g_eq_intro; }
name const & get_eq_mp_name() { return *g_eq_mp; }
name const & get_eq_mpr_name() { return *g_eq_mpr; }
name const & get_eq_nrec_name() { return *g_eq_nrec; }
name const & get_eq_rec_name() { return *g_eq_rec; }
name const & get_eq_rec_eq_name() { return *g_eq_rec_eq; }
name const & get_eq_refl_name() { return *g_eq_refl; }
name const & get_eq_subst_name() { return *g_eq_subst; }
name const & get_eq_symm_name() { return *g_eq_symm; }
@@ -1596,18 +1477,11 @@ name const & get_is_associative_name() { return *g_is_associative; }
name const & get_is_associative_assoc_name() { return *g_is_associative_assoc; }
name const & get_is_commutative_name() { return *g_is_commutative; }
name const & get_is_commutative_comm_name() { return *g_is_commutative_comm; }
name const & get_is_int_name() { return *g_is_int; }
name const & get_is_trunc_is_prop_name() { return *g_is_trunc_is_prop; }
name const & get_is_trunc_is_prop_elim_name() { return *g_is_trunc_is_prop_elim; }
name const & get_is_trunc_is_set_name() { return *g_is_trunc_is_set; }
name const & get_ite_name() { return *g_ite; }
name const & get_left_distrib_name() { return *g_left_distrib; }
name const & get_left_comm_name() { return *g_left_comm; }
name const & get_le_name() { return *g_le; }
name const & get_le_refl_name() { return *g_le_refl; }
name const & get_lift_name() { return *g_lift; }
name const & get_lift_down_name() { return *g_lift_down; }
name const & get_lift_up_name() { return *g_lift_up; }
name const & get_linear_ordered_comm_ring_name() { return *g_linear_ordered_comm_ring; }
name const & get_linear_ordered_ring_name() { return *g_linear_ordered_ring; }
name const & get_linear_ordered_semiring_name() { return *g_linear_ordered_semiring; }
@@ -1615,11 +1489,6 @@ name const & get_list_name() { return *g_list; }
name const & get_list_nil_name() { return *g_list_nil; }
name const & get_list_cons_name() { return *g_list_cons; }
name const & get_lt_name() { return *g_lt; }
name const & get_map_name() { return *g_map; }
name const & get_map_insert_name() { return *g_map_insert; }
name const & get_map_lookup_name() { return *g_map_lookup; }
name const & get_map_select_name() { return *g_map_select; }
name const & get_map_store_name() { return *g_map_store; }
name const & get_match_failed_name() { return *g_match_failed; }
name const & get_mod_name() { return *g_mod; }
name const & get_monad_name() { return *g_monad; }
@@ -1645,7 +1514,6 @@ name const & get_nat_has_add_name() { return *g_nat_has_add; }
name const & get_nat_has_mul_name() { return *g_nat_has_mul; }
name const & get_nat_has_div_name() { return *g_nat_has_div; }
name const & get_nat_has_sub_name() { return *g_nat_has_sub; }
name const & get_nat_has_neg_name() { return *g_nat_has_neg; }
name const & get_nat_has_lt_name() { return *g_nat_has_lt; }
name const & get_nat_has_le_name() { return *g_nat_has_le; }
name const & get_nat_add_name() { return *g_nat_add; }
@@ -1776,30 +1644,23 @@ name const & get_put_nat_name() { return *g_put_nat; }
name const & get_to_pexpr_name() { return *g_to_pexpr; }
name const & get_quot_mk_name() { return *g_quot_mk; }
name const & get_quot_lift_name() { return *g_quot_lift; }
name const & get_rat_divide_name() { return *g_rat_divide; }
name const & get_rat_of_num_name() { return *g_rat_of_num; }
name const & get_rat_of_int_name() { return *g_rat_of_int; }
name const & get_real_name() { return *g_real; }
name const & get_real_has_zero_name() { return *g_real_has_zero; }
name const & get_real_has_one_name() { return *g_real_has_one; }
name const & get_real_of_int_name() { return *g_real_of_int; }
name const & get_real_to_int_name() { return *g_real_to_int; }
name const & get_real_is_int_name() { return *g_real_is_int; }
name const & get_real_has_neg_name() { return *g_real_has_neg; }
name const & get_real_has_div_name() { return *g_real_has_div; }
name const & get_real_has_add_name() { return *g_real_has_add; }
name const & get_real_has_mul_name() { return *g_real_has_mul; }
name const & get_real_has_sub_name() { return *g_real_has_sub; }
name const & get_real_has_div_name() { return *g_real_has_div; }
name const & get_real_has_le_name() { return *g_real_has_le; }
name const & get_real_has_lt_name() { return *g_real_has_lt; }
name const & get_real_has_neg_name() { return *g_real_has_neg; }
name const & get_real_is_int_name() { return *g_real_is_int; }
name const & get_real_of_rat_name() { return *g_real_of_rat; }
name const & get_real_of_int_name() { return *g_real_of_int; }
name const & get_real_to_int_name() { return *g_real_to_int; }
name const & get_real_has_le_name() { return *g_real_has_le; }
name const & get_rfl_name() { return *g_rfl; }
name const & get_right_distrib_name() { return *g_right_distrib; }
name const & get_ring_name() { return *g_ring; }
name const & get_scope_trace_name() { return *g_scope_trace; }
name const & get_set_of_name() { return *g_set_of; }
name const & get_sep_name() { return *g_sep; }
name const & get_select_name() { return *g_select; }
name const & get_semiring_name() { return *g_semiring; }
name const & get_sigma_name() { return *g_sigma; }
name const & get_sigma_cases_on_name() { return *g_sigma_cases_on; }
@@ -1812,18 +1673,12 @@ name const & get_psigma_mk_name() { return *g_psigma_mk; }
name const & get_psigma_fst_name() { return *g_psigma_fst; }
name const & get_psigma_snd_name() { return *g_psigma_snd; }
name const & get_simp_name() { return *g_simp; }
name const & get_simplifier_assoc_subst_name() { return *g_simplifier_assoc_subst; }
name const & get_simplifier_congr_bin_op_name() { return *g_simplifier_congr_bin_op; }
name const & get_simplifier_congr_bin_arg1_name() { return *g_simplifier_congr_bin_arg1; }
name const & get_simplifier_congr_bin_arg2_name() { return *g_simplifier_congr_bin_arg2; }
name const & get_simplifier_congr_bin_args_name() { return *g_simplifier_congr_bin_args; }
name const & get_singleton_name() { return *g_singleton; }
name const & get_sizeof_name() { return *g_sizeof; }
name const & get_smt_array_name() { return *g_smt_array; }
name const & get_smt_select_name() { return *g_smt_select; }
name const & get_smt_store_name() { return *g_smt_store; }
name const & get_smt_prove_name() { return *g_smt_prove; }
name const & get_store_name() { return *g_store; }
name const & get_string_name() { return *g_string; }
name const & get_string_empty_name() { return *g_string_empty; }
name const & get_string_str_name() { return *g_string_str; }
@@ -1847,7 +1702,6 @@ name const & get_psum_name() { return *g_psum; }
name const & get_psum_cases_on_name() { return *g_psum_cases_on; }
name const & get_psum_inl_name() { return *g_psum_inl; }
name const & get_psum_inr_name() { return *g_psum_inr; }
name const & get_default_smt_config_name() { return *g_default_smt_config; }
name const & get_smt_state_mk_name() { return *g_smt_state_mk; }
name const & get_smt_tactic_execute_name() { return *g_smt_tactic_execute; }
name const & get_smt_tactic_execute_with_name() { return *g_smt_tactic_execute_with; }
@@ -1864,9 +1718,7 @@ name const & get_tactic_interactive_exact_name() { return *g_tactic_interactive_
name const & get_trivial_name() { return *g_trivial; }
name const & get_thunk_name() { return *g_thunk; }
name const & get_to_fmt_name() { return *g_to_fmt; }
name const & get_to_int_name() { return *g_to_int; }
name const & get_to_string_name() { return *g_to_string; }
name const & get_to_real_name() { return *g_to_real; }
name const & get_trans_rel_left_name() { return *g_trans_rel_left; }
name const & get_trans_rel_right_name() { return *g_trans_rel_right; }
name const & get_true_name() { return *g_true; }

49
src/library/constants.h
View File

@@ -25,7 +25,6 @@ name const & get_bool_name();
name const & get_bool_ff_name();
name const & get_bool_tt_name();
name const & get_bind_name();
name const & get_bv_name();
name const & get_caching_user_attribute_name();
name const & get_cast_name();
name const & get_cast_eq_name();
@@ -46,13 +45,10 @@ name const & get_comm_semiring_name();
name const & get_congr_name();
name const & get_congr_arg_name();
name const & get_congr_fun_name();
name const & get_cyclic_numerals_name();
name const & get_cyclic_numerals_bound_name();
name const & get_decidable_name();
name const & get_decidable_by_contradiction_name();
name const & get_decidable_to_bool_name();
name const & get_discrete_field_name();
name const & get_distinct_name();
name const & get_distrib_name();
name const & get_dite_name();
name const & get_div_name();
@@ -64,13 +60,9 @@ name const & get_Exists_name();
name const & get_eq_name();
name const & get_eq_cases_on_name();
name const & get_eq_drec_name();
name const & get_eq_elim_inv_inv_name();
name const & get_eq_intro_name();
name const & get_eq_mp_name();
name const & get_eq_mpr_name();
name const & get_eq_nrec_name();
name const & get_eq_rec_name();
name const & get_eq_rec_eq_name();
name const & get_eq_refl_name();
name const & get_eq_subst_name();
name const & get_eq_symm_name();
@@ -184,18 +176,11 @@ name const & get_is_associative_name();
name const & get_is_associative_assoc_name();
name const & get_is_commutative_name();
name const & get_is_commutative_comm_name();
name const & get_is_int_name();
name const & get_is_trunc_is_prop_name();
name const & get_is_trunc_is_prop_elim_name();
name const & get_is_trunc_is_set_name();
name const & get_ite_name();
name const & get_left_distrib_name();
name const & get_left_comm_name();
name const & get_le_name();
name const & get_le_refl_name();
name const & get_lift_name();
name const & get_lift_down_name();
name const & get_lift_up_name();
name const & get_linear_ordered_comm_ring_name();
name const & get_linear_ordered_ring_name();
name const & get_linear_ordered_semiring_name();
@@ -203,11 +188,6 @@ name const & get_list_name();
name const & get_list_nil_name();
name const & get_list_cons_name();
name const & get_lt_name();
name const & get_map_name();
name const & get_map_insert_name();
name const & get_map_lookup_name();
name const & get_map_select_name();
name const & get_map_store_name();
name const & get_match_failed_name();
name const & get_mod_name();
name const & get_monad_name();
@@ -233,7 +213,6 @@ name const & get_nat_has_add_name();
name const & get_nat_has_mul_name();
name const & get_nat_has_div_name();
name const & get_nat_has_sub_name();
name const & get_nat_has_neg_name();
name const & get_nat_has_lt_name();
name const & get_nat_has_le_name();
name const & get_nat_add_name();
@@ -364,30 +343,23 @@ name const & get_put_nat_name();
name const & get_to_pexpr_name();
name const & get_quot_mk_name();
name const & get_quot_lift_name();
name const & get_rat_divide_name();
name const & get_rat_of_num_name();
name const & get_rat_of_int_name();
name const & get_real_name();
name const & get_real_has_zero_name();
name const & get_real_has_one_name();
name const & get_real_of_int_name();
name const & get_real_to_int_name();
name const & get_real_is_int_name();
name const & get_real_has_neg_name();
name const & get_real_has_div_name();
name const & get_real_has_add_name();
name const & get_real_has_mul_name();
name const & get_real_has_sub_name();
name const & get_real_has_div_name();
name const & get_real_has_le_name();
name const & get_real_has_lt_name();
name const & get_real_has_neg_name();
name const & get_real_is_int_name();
name const & get_real_of_rat_name();
name const & get_real_of_int_name();
name const & get_real_to_int_name();
name const & get_real_has_le_name();
name const & get_rfl_name();
name const & get_right_distrib_name();
name const & get_ring_name();
name const & get_scope_trace_name();
name const & get_set_of_name();
name const & get_sep_name();
name const & get_select_name();
name const & get_semiring_name();
name const & get_sigma_name();
name const & get_sigma_cases_on_name();
@@ -400,18 +372,12 @@ name const & get_psigma_mk_name();
name const & get_psigma_fst_name();
name const & get_psigma_snd_name();
name const & get_simp_name();
name const & get_simplifier_assoc_subst_name();
name const & get_simplifier_congr_bin_op_name();
name const & get_simplifier_congr_bin_arg1_name();
name const & get_simplifier_congr_bin_arg2_name();
name const & get_simplifier_congr_bin_args_name();
name const & get_singleton_name();
name const & get_sizeof_name();
name const & get_smt_array_name();
name const & get_smt_select_name();
name const & get_smt_store_name();
name const & get_smt_prove_name();
name const & get_store_name();
name const & get_string_name();
name const & get_string_empty_name();
name const & get_string_str_name();
@@ -435,7 +401,6 @@ name const & get_psum_name();
name const & get_psum_cases_on_name();
name const & get_psum_inl_name();
name const & get_psum_inr_name();
name const & get_default_smt_config_name();
name const & get_smt_state_mk_name();
name const & get_smt_tactic_execute_name();
name const & get_smt_tactic_execute_with_name();
@@ -452,9 +417,7 @@ name const & get_tactic_interactive_exact_name();
name const & get_trivial_name();
name const & get_thunk_name();
name const & get_to_fmt_name();
name const & get_to_int_name();
name const & get_to_string_name();
name const & get_to_real_name();
name const & get_trans_rel_left_name();
name const & get_trans_rel_right_name();
name const & get_true_name();

53
src/library/constants.txt
View File

@@ -18,7 +18,6 @@ bool
bool.ff
bool.tt
bind
bv
caching_user_attribute
cast
cast_eq
@@ -39,13 +38,10 @@ comm_semiring
congr
congr_arg
congr_fun
cyclic_numerals
cyclic_numerals.bound
decidable
decidable.by_contradiction
decidable.to_bool
discrete_field
distinct
distrib
dite
div
@@ -57,13 +53,9 @@ Exists
eq
eq.cases_on
eq.drec
eq.elim_inv_inv
eq.intro
eq.mp
eq.mpr
eq.nrec
eq.rec
eq_rec_eq
eq.refl
eq.subst
eq.symm
@@ -167,7 +159,7 @@ int.neg_ne_of_pos
int.ne_neg_of_pos
int.neg_ne_zero_of_ne
int.zero_ne_neg_of_ne
int_decidable_linear_ordered_comm_group
int.decidable_linear_ordered_comm_group
interactive.parse
inv
io
@@ -177,18 +169,11 @@ is_associative
is_associative.assoc
is_commutative
is_commutative.comm
is_int
is_trunc.is_prop
is_trunc.is_prop.elim
is_trunc.is_set
ite
left_distrib
left_comm
le
le.refl
lift
lift.down
lift.up
le_refl
linear_ordered_comm_ring
linear_ordered_ring
linear_ordered_semiring
@@ -196,11 +181,6 @@ list
list.nil
list.cons
lt
map
map.insert
map.lookup
map.select
map.store
match_failed
mod
monad
@@ -226,7 +206,6 @@ nat.has_add
nat.has_mul
nat.has_div
nat.has_sub
nat.has_neg
nat.has_lt
nat.has_le
nat.add
@@ -357,30 +336,23 @@ put_nat
to_pexpr
quot.mk
quot.lift
rat.divide
rat.of_num
rat.of_int
real
real.has_zero
real.has_one
real.of_int
real.to_int
real.is_int
real.has_neg
real.has_div
real.has_add
real.has_mul
real.has_sub
real.has_div
real.has_le
real.has_lt
real.has_neg
real.is_int
real.of_rat
real.of_int
real.to_int
real.has_le
rfl
right_distrib
ring
scope_trace
set_of
sep
select
semiring
sigma
sigma.cases_on
@@ -393,18 +365,12 @@ psigma.mk
psigma.fst
psigma.snd
simp
simplifier.assoc_subst
simplifier.congr_bin_op
simplifier.congr_bin_arg1
simplifier.congr_bin_arg2
simplifier.congr_bin_args
singleton
sizeof
smt.array
smt.select
smt.store
smt.prove
store
string
string.empty
string.str
@@ -428,7 +394,6 @@ psum
psum.cases_on
psum.inl
psum.inr
default_smt_config
smt_state.mk
smt_tactic.execute
smt_tactic.execute_with
@@ -445,9 +410,7 @@ tactic.interactive.exact
trivial
thunk
to_fmt
to_int
to_string
to_real
trans_rel_left
trans_rel_right
true

4
src/library/scoped_ext.cpp
View File

@@ -65,6 +65,10 @@ name_set get_opened_namespaces(environment const & env) {
return get_extension(env).m_opened_namespaces;
}
bool is_namespace(environment const & env, name const & n) {
return get_extension(env).m_namespace_set.contains(n);
}
optional<name> to_valid_namespace_name(environment const & env, name const & n) {
scope_mng_ext const & ext = get_extension(env);
if (ext.m_namespace_set.contains(n))

3
src/library/scoped_ext.h
View File

@@ -67,6 +67,9 @@ environment mark_namespace_as_open(environment const & env, name const & n);
/** \brief Return the set of namespaces marked as "open" using \c mark_namespace_as_open. */
name_set get_opened_namespaces(environment const & env);
/** \brief Return true iff \c n is a namespace */
bool is_namespace(environment const & env, name const & n);
/** \brief Auxilary template used to simplify the creation of environment extensions that support
the scope */
template<typename Config>

2
src/library/tactic/simplify.cpp
View File

@@ -186,7 +186,7 @@ expr simplify_core_fn::remove_unnecessary_casts(expr const & e) {
buffer<expr> cast_args;
expr f_cast = get_app_args(args[i], cast_args);
name n_f = const_name(f_cast);
if (n_f == get_eq_rec_name() || n_f == get_eq_drec_name() || n_f == get_eq_nrec_name()) {
if (n_f == get_eq_rec_name() || n_f == get_eq_drec_name()) {
lean_assert(cast_args.size() == 6);
expr major_premise = cast_args[5];
expr f_major_premise = get_app_fn(major_premise);

4
src/library/util.cpp
View File

@@ -155,10 +155,6 @@ bool has_pprod_decls(environment const & env) {
return has_constructor(env, get_pprod_mk_name(), get_pprod_name(), 4);
}
bool has_lift_decls(environment const & env) {
return has_constructor(env, get_lift_up_name(), get_lift_name(), 2);
}
/* n is considered to be recursive if it is an inductive datatype and
1) It has a constructor that takes n as an argument
2) It is part of a mutually recursive declaration, and some constructor

1
src/library/util.h
View File

@@ -48,7 +48,6 @@ bool has_punit_decls(environment const & env);
bool has_pprod_decls(environment const & env);
bool has_eq_decls(environment const & env);
bool has_heq_decls(environment const & env);
bool has_lift_decls(environment const & env);
/** \brief Return true iff \c n is the name of a recursive datatype in \c env.
That is, it must be an inductive datatype AND contain a recursive constructor.

6
src/library/vm/vm_environment.cpp
View File

@@ -10,6 +10,7 @@ Author: Leonardo de Moura
#include "kernel/inductive/inductive.h"
#include "kernel/standard_kernel.h"
#include "library/module.h"
#include "library/scoped_ext.h"
#include "library/projection.h"
#include "library/util.h"
#include "library/relation_manager.h"
@@ -210,6 +211,10 @@ vm_obj environment_decl_pos_info(vm_obj const & env, vm_obj const & n) {
}
}
vm_obj environment_is_namespace(vm_obj const & env, vm_obj const & n) {
return mk_vm_bool(is_namespace(to_env(env), to_name(n)));
}
/*
structure projection_info :=
(cname : name)
@@ -247,6 +252,7 @@ void initialize_vm_environment() {
DECLARE_VM_BUILTIN(name({"environment", "inductive_num_params"}), environment_inductive_num_params);
DECLARE_VM_BUILTIN(name({"environment", "inductive_num_indices"}), environment_inductive_num_indices);
DECLARE_VM_BUILTIN(name({"environment", "inductive_dep_elim"}), environment_inductive_dep_elim);
DECLARE_VM_BUILTIN(name({"environment", "is_namespace"}), environment_is_namespace);
DECLARE_VM_BUILTIN(name({"environment", "is_ginductive"}), environment_is_ginductive);
DECLARE_VM_BUILTIN(name({"environment", "is_projection"}), environment_is_projection);
DECLARE_VM_BUILTIN(name({"environment", "relation_info"}), environment_relation_info);

438
tests/lean/run/check_constants.lean Normal file
View File

@@ -0,0 +1,438 @@
-- DO NOT EDIT, automatically generated file, generator scripts/gen_constants_cpp.py
import smt system.io
open tactic
meta def script_check_id (n : name) : tactic unit :=
do env ← get_env, (env^.get n >> return ()) <|> (guard $ env^.is_namespace n) <|> (attribute.get_instances n >> return ()) <|> fail ("identifier '" ++ to_string n ++ "' is not a constant, namespace nor attribute")
run_command script_check_id `abs
run_command script_check_id `absurd
run_command script_check_id `acc.cases_on
run_command script_check_id `add
run_command script_check_id `add_comm_group
run_command script_check_id `add_comm_semigroup
run_command script_check_id `add_group
run_command script_check_id `add_monoid
run_command script_check_id `and
run_command script_check_id `and.elim_left
run_command script_check_id `and.elim_right
run_command script_check_id `and.intro
run_command script_check_id `andthen
run_command script_check_id `auto_param
run_command script_check_id `bit0
run_command script_check_id `bit1
run_command script_check_id `bool
run_command script_check_id `bool.ff
run_command script_check_id `bool.tt
run_command script_check_id `bind
run_command script_check_id `caching_user_attribute
run_command script_check_id `cast
run_command script_check_id `cast_eq
run_command script_check_id `cast_heq
run_command script_check_id `char
run_command script_check_id `char.of_nat
run_command script_check_id `char.of_nat_ne_of_ne
run_command script_check_id `classical
run_command script_check_id `classical.prop_decidable
run_command script_check_id `classical.type_decidable_eq
run_command script_check_id `coe
run_command script_check_id `coe_fn
run_command script_check_id `coe_sort
run_command script_check_id `coe_to_lift
run_command script_check_id `combinator.K
run_command script_check_id `comm_ring
run_command script_check_id `comm_semiring
run_command script_check_id `congr
run_command script_check_id `congr_arg
run_command script_check_id `congr_fun
run_command script_check_id `decidable
run_command script_check_id `decidable.by_contradiction
run_command script_check_id `decidable.to_bool
run_command script_check_id `discrete_field
run_command script_check_id `distrib
run_command script_check_id `dite
run_command script_check_id `div
run_command script_check_id `id
run_command script_check_id `empty
run_command script_check_id `empty.rec
run_command script_check_id `emptyc
run_command script_check_id `Exists
run_command script_check_id `eq
run_command script_check_id `eq.cases_on
run_command script_check_id `eq.drec
run_command script_check_id `eq.mp
run_command script_check_id `eq.mpr
run_command script_check_id `eq.rec
run_command script_check_id `eq.refl
run_command script_check_id `eq.subst
run_command script_check_id `eq.symm
run_command script_check_id `eq.trans
run_command script_check_id `eq_of_heq
run_command script_check_id `eq_rec_heq
run_command script_check_id `eq_true_intro
run_command script_check_id `eq_false_intro
run_command script_check_id `eq_self_iff_true
run_command script_check_id `exists.elim
run_command script_check_id `format
run_command script_check_id `functor
run_command script_check_id `false
run_command script_check_id `false_of_true_iff_false
run_command script_check_id `false_of_true_eq_false
run_command script_check_id `true_eq_false_of_false
run_command script_check_id `false.rec
run_command script_check_id `field
run_command script_check_id `fin
run_command script_check_id `fin.mk
run_command script_check_id `fin.ne_of_vne
run_command script_check_id `forall_congr
run_command script_check_id `forall_congr_eq
run_command script_check_id `forall_not_of_not_exists
run_command script_check_id `funext
run_command script_check_id `ge
run_command script_check_id `get_line
run_command script_check_id `gt
run_command script_check_id `has_add
run_command script_check_id `has_div
run_command script_check_id `has_mul
run_command script_check_id `has_inv
run_command script_check_id `has_le
run_command script_check_id `has_lt
run_command script_check_id `has_neg
run_command script_check_id `has_one
run_command script_check_id `has_one.one
run_command script_check_id `has_sizeof
run_command script_check_id `has_sizeof.mk
run_command script_check_id `has_sizeof.sizeof
run_command script_check_id `has_sub
run_command script_check_id `has_to_format
run_command script_check_id `has_to_string
run_command script_check_id `has_zero
run_command script_check_id `has_zero.zero
run_command script_check_id `has_coe_t
run_command script_check_id `heq
run_command script_check_id `heq.refl
run_command script_check_id `heq.symm
run_command script_check_id `heq.trans
run_command script_check_id `heq_of_eq
run_command script_check_id `id_locked
run_command script_check_id `if_neg
run_command script_check_id `if_pos
run_command script_check_id `iff
run_command script_check_id `iff.elim_left
run_command script_check_id `iff.elim_right
run_command script_check_id `iff_false_intro
run_command script_check_id `iff.intro
run_command script_check_id `iff.mp
run_command script_check_id `iff.mpr
run_command script_check_id `iff.refl
run_command script_check_id `iff.symm
run_command script_check_id `iff.trans
run_command script_check_id `iff_true_intro
run_command script_check_id `imp_congr
run_command script_check_id `imp_congr_eq
run_command script_check_id `imp_congr_ctx
run_command script_check_id `imp_congr_ctx_eq
run_command script_check_id `implies
run_command script_check_id `implies_of_if_neg
run_command script_check_id `implies_of_if_pos
run_command script_check_id `implies.resolve
run_command script_check_id `insert
run_command script_check_id `int
run_command script_check_id `int.of_nat
run_command script_check_id `int.has_zero
run_command script_check_id `int.has_one
run_command script_check_id `int.has_add
run_command script_check_id `int.has_mul
run_command script_check_id `int.has_sub
run_command script_check_id `int.has_div
run_command script_check_id `int.has_le
run_command script_check_id `int.has_lt
run_command script_check_id `int.has_neg
run_command script_check_id `int.has_mod
run_command script_check_id `int.bit0_nonneg
run_command script_check_id `int.bit1_nonneg
run_command script_check_id `int.one_nonneg
run_command script_check_id `int.zero_nonneg
run_command script_check_id `int.bit0_pos
run_command script_check_id `int.bit1_pos
run_command script_check_id `int.one_pos
run_command script_check_id `int.nat_abs_zero
run_command script_check_id `int.nat_abs_one
run_command script_check_id `int.nat_abs_bit0_step
run_command script_check_id `int.nat_abs_bit1_nonneg_step
run_command script_check_id `int.ne_of_nat_ne_nonneg_case
run_command script_check_id `int.ne_neg_of_ne
run_command script_check_id `int.neg_ne_of_pos
run_command script_check_id `int.ne_neg_of_pos
run_command script_check_id `int.neg_ne_zero_of_ne
run_command script_check_id `int.zero_ne_neg_of_ne
run_command script_check_id `int.decidable_linear_ordered_comm_group
run_command script_check_id `interactive.parse
run_command script_check_id `inv
run_command script_check_id `io
run_command script_check_id `io.functor
run_command script_check_id `io.monad
run_command script_check_id `is_associative
run_command script_check_id `is_associative.assoc
run_command script_check_id `is_commutative
run_command script_check_id `is_commutative.comm
run_command script_check_id `ite
run_command script_check_id `left_distrib
run_command script_check_id `left_comm
run_command script_check_id `le
run_command script_check_id `le_refl
run_command script_check_id `linear_ordered_comm_ring
run_command script_check_id `linear_ordered_ring
run_command script_check_id `linear_ordered_semiring
run_command script_check_id `list
run_command script_check_id `list.nil
run_command script_check_id `list.cons
run_command script_check_id `lt
run_command script_check_id `match_failed
run_command script_check_id `mod
run_command script_check_id `monad
run_command script_check_id `monad.map
run_command script_check_id `monad.bind
run_command script_check_id `monad.ret
run_command script_check_id `monad_fail
run_command script_check_id `monoid
run_command script_check_id `mul
run_command script_check_id `mul_one
run_command script_check_id `mul_zero
run_command script_check_id `mul_zero_class
run_command script_check_id `name
run_command script_check_id `name.anonymous
run_command script_check_id `name.mk_string
run_command script_check_id `nat
run_command script_check_id `nat.of_num
run_command script_check_id `nat.succ
run_command script_check_id `nat.zero
run_command script_check_id `nat.has_zero
run_command script_check_id `nat.has_one
run_command script_check_id `nat.has_add
run_command script_check_id `nat.has_mul
run_command script_check_id `nat.has_div
run_command script_check_id `nat.has_sub
run_command script_check_id `nat.has_lt
run_command script_check_id `nat.has_le
run_command script_check_id `nat.add
run_command script_check_id `nat.no_confusion
run_command script_check_id `nat.cases_on
run_command script_check_id `nat.bit0_ne
run_command script_check_id `nat.bit0_ne_bit1
run_command script_check_id `nat.bit0_ne_zero
run_command script_check_id `nat.bit0_ne_one
run_command script_check_id `nat.bit1_ne
run_command script_check_id `nat.bit1_ne_bit0
run_command script_check_id `nat.bit1_ne_zero
run_command script_check_id `nat.bit1_ne_one
run_command script_check_id `nat.zero_ne_one
run_command script_check_id `nat.zero_ne_bit0
run_command script_check_id `nat.zero_ne_bit1
run_command script_check_id `nat.one_ne_zero
run_command script_check_id `nat.one_ne_bit0
run_command script_check_id `nat.one_ne_bit1
run_command script_check_id `nat.bit0_lt
run_command script_check_id `nat.bit1_lt
run_command script_check_id `nat.bit0_lt_bit1
run_command script_check_id `nat.bit1_lt_bit0
run_command script_check_id `nat.zero_lt_one
run_command script_check_id `nat.zero_lt_bit1
run_command script_check_id `nat.zero_lt_bit0
run_command script_check_id `nat.one_lt_bit0
run_command script_check_id `nat.one_lt_bit1
run_command script_check_id `nat.le_of_lt
run_command script_check_id `nat.le_refl
run_command script_check_id `ne
run_command script_check_id `neg
run_command script_check_id `neq_of_not_iff
run_command script_check_id `norm_num.add1
run_command script_check_id `norm_num.add1_bit0
run_command script_check_id `norm_num.add1_bit1_helper
run_command script_check_id `norm_num.add1_one
run_command script_check_id `norm_num.add1_zero
run_command script_check_id `norm_num.add_div_helper
run_command script_check_id `norm_num.bin_add_zero
run_command script_check_id `norm_num.bin_zero_add
run_command script_check_id `norm_num.bit0_add_bit0_helper
run_command script_check_id `norm_num.bit0_add_bit1_helper
run_command script_check_id `norm_num.bit0_add_one
run_command script_check_id `norm_num.bit1_add_bit0_helper
run_command script_check_id `norm_num.bit1_add_bit1_helper
run_command script_check_id `norm_num.bit1_add_one_helper
run_command script_check_id `norm_num.div_add_helper
run_command script_check_id `norm_num.div_eq_div_helper
run_command script_check_id `norm_num.div_helper
run_command script_check_id `norm_num.div_mul_helper
run_command script_check_id `norm_num.mk_cong
run_command script_check_id `norm_num.mul_bit0_helper
run_command script_check_id `norm_num.mul_bit1_helper
run_command script_check_id `norm_num.mul_div_helper
run_command script_check_id `norm_num.neg_add_neg_helper
run_command script_check_id `norm_num.neg_add_pos_helper1
run_command script_check_id `norm_num.neg_add_pos_helper2
run_command script_check_id `norm_num.neg_mul_neg_helper
run_command script_check_id `norm_num.neg_mul_pos_helper
run_command script_check_id `norm_num.neg_neg_helper
run_command script_check_id `norm_num.neg_zero_helper
run_command script_check_id `norm_num.nonneg_bit0_helper
run_command script_check_id `norm_num.nonneg_bit1_helper
run_command script_check_id `norm_num.nonzero_of_div_helper
run_command script_check_id `norm_num.nonzero_of_neg_helper
run_command script_check_id `norm_num.nonzero_of_pos_helper
run_command script_check_id `norm_num.one_add_bit0
run_command script_check_id `norm_num.one_add_bit1_helper
run_command script_check_id `norm_num.one_add_one
run_command script_check_id `norm_num.pos_add_neg_helper
run_command script_check_id `norm_num.pos_add_pos_helper
run_command script_check_id `norm_num.pos_bit0_helper
run_command script_check_id `norm_num.pos_bit1_helper
run_command script_check_id `norm_num.pos_mul_neg_helper
run_command script_check_id `norm_num.sub_eq_add_neg_helper
run_command script_check_id `norm_num.sub_nat_zero_helper
run_command script_check_id `norm_num.sub_nat_pos_helper
run_command script_check_id `norm_num.subst_into_div
run_command script_check_id `norm_num.subst_into_prod
run_command script_check_id `norm_num.subst_into_subtr
run_command script_check_id `norm_num.subst_into_sum
run_command script_check_id `not
run_command script_check_id `not_of_iff_false
run_command script_check_id `not_of_eq_false
run_command script_check_id `not_of_not_not_not
run_command script_check_id `num
run_command script_check_id `num.pos
run_command script_check_id `num.zero
run_command script_check_id `of_eq_true
run_command script_check_id `of_iff_true
run_command script_check_id `one
run_command script_check_id `one_mul
run_command script_check_id `option
run_command script_check_id `option.none
run_command script_check_id `option.some
run_command script_check_id `opt_param
run_command script_check_id `or
run_command script_check_id `or.elim
run_command script_check_id `or.intro_left
run_command script_check_id `or.intro_right
run_command script_check_id `or.neg_resolve_left
run_command script_check_id `or.neg_resolve_right
run_command script_check_id `or.rec
run_command script_check_id `or.resolve_left
run_command script_check_id `or.resolve_right
run_command script_check_id `orelse
run_command script_check_id `out_param
run_command script_check_id `punit
run_command script_check_id `punit.star
run_command script_check_id `pos_num
run_command script_check_id `pos_num.bit0
run_command script_check_id `pos_num.bit1
run_command script_check_id `pos_num.one
run_command script_check_id `prod.mk
run_command script_check_id `pprod
run_command script_check_id `pprod.mk
run_command script_check_id `pprod.fst
run_command script_check_id `pprod.snd
run_command script_check_id `propext
run_command script_check_id `pexpr
run_command script_check_id `pexpr.subst
run_command script_check_id `pre_monad.bind
run_command script_check_id `pre_monad.and_then
run_command script_check_id `pre_monad.seq
run_command script_check_id `put_str
run_command script_check_id `put_nat
run_command script_check_id `to_pexpr
run_command script_check_id `quot.mk
run_command script_check_id `quot.lift
run_command script_check_id `real
run_command script_check_id `real.of_int
run_command script_check_id `real.to_int
run_command script_check_id `real.is_int
run_command script_check_id `real.has_neg
run_command script_check_id `real.has_div
run_command script_check_id `real.has_add
run_command script_check_id `real.has_mul
run_command script_check_id `real.has_sub
run_command script_check_id `real.has_lt
run_command script_check_id `real.has_le
run_command script_check_id `rfl
run_command script_check_id `right_distrib
run_command script_check_id `ring
run_command script_check_id `scope_trace
run_command script_check_id `set_of
run_command script_check_id `sep
run_command script_check_id `semiring
run_command script_check_id `sigma
run_command script_check_id `sigma.cases_on
run_command script_check_id `sigma.mk
run_command script_check_id `sigma.fst
run_command script_check_id `sigma.snd
run_command script_check_id `psigma
run_command script_check_id `psigma.cases_on
run_command script_check_id `psigma.mk
run_command script_check_id `psigma.fst
run_command script_check_id `psigma.snd
run_command script_check_id `simp
run_command script_check_id `singleton
run_command script_check_id `sizeof
run_command script_check_id `smt.array
run_command script_check_id `smt.select
run_command script_check_id `smt.store
run_command script_check_id `smt.prove
run_command script_check_id `string
run_command script_check_id `string.empty
run_command script_check_id `string.str
run_command script_check_id `string.empty_ne_str
run_command script_check_id `string.str_ne_empty
run_command script_check_id `string.str_ne_str_left
run_command script_check_id `string.str_ne_str_right
run_command script_check_id `sub
run_command script_check_id `subsingleton
run_command script_check_id `subsingleton.elim
run_command script_check_id `subsingleton.helim
run_command script_check_id `subtype
run_command script_check_id `subtype.tag
run_command script_check_id `subtype.elt_of
run_command script_check_id `subtype.rec
run_command script_check_id `sum
run_command script_check_id `sum.cases_on
run_command script_check_id `sum.inl
run_command script_check_id `sum.inr
run_command script_check_id `psum
run_command script_check_id `psum.cases_on
run_command script_check_id `psum.inl
run_command script_check_id `psum.inr
run_command script_check_id `smt_state.mk
run_command script_check_id `smt_tactic.execute
run_command script_check_id `smt_tactic.execute_with
run_command script_check_id `tactic
run_command script_check_id `tactic.eval_expr
run_command script_check_id `tactic.constructor
run_command script_check_id `tactic.step
run_command script_check_id `tactic.to_expr
run_command script_check_id `tactic.skip
run_command script_check_id `tactic.try
run_command script_check_id `tactic.triv
run_command script_check_id `tactic.interactive
run_command script_check_id `tactic.interactive.exact
run_command script_check_id `trivial
run_command script_check_id `thunk
run_command script_check_id `to_fmt
run_command script_check_id `to_string
run_command script_check_id `trans_rel_left
run_command script_check_id `trans_rel_right
run_command script_check_id `true
run_command script_check_id `true.intro
run_command script_check_id `unification_hint
run_command script_check_id `unification_hint.mk
run_command script_check_id `unification_constraint
run_command script_check_id `unification_constraint.mk
run_command script_check_id `unit
run_command script_check_id `unit.cases_on
run_command script_check_id `unit.star
run_command script_check_id `user_attribute
run_command script_check_id `vm_monitor
run_command script_check_id `weak_order
run_command script_check_id `well_founded
run_command script_check_id `xor
run_command script_check_id `zero
run_command script_check_id `zero_le_one
run_command script_check_id `zero_lt_one
run_command script_check_id `zero_mul