diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean index 5332f4085..d3f58e69a 100644 --- a/library/algebra/ring.lean +++ b/library/algebra/ring.lean @@ -434,8 +434,6 @@ theorem subst_into_prod [has_mul A] (l r tl tr t : A) (prl : l = tl) (prr : r = theorem mk_cong (op : A → A) (a b : A) (H : a = b) : op a = op b := by congruence; exact H -theorem mk_eq (a : A) : a = a := rfl - theorem neg_add_neg_eq_of_add_add_eq_zero [add_comm_group A] (a b c : A) (H : c + a + b = 0) : -a + -b = c := begin diff --git a/src/library/constants.cpp b/src/library/constants.cpp index ee6f36fc5..940f7a6fc 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -4,10 +4,11 @@ #include "util/name.h" namespace lean{ name const * g_absurd = nullptr; -name const * g_distrib = nullptr; -name const * g_left_distrib = nullptr; -name const * g_right_distrib = nullptr; name const * g_add = nullptr; +name const * g_add_comm_group = nullptr; +name const * g_add_comm_semigroup = nullptr; +name const * g_add_monoid = nullptr; +name const * g_add_group = nullptr; name const * g_and = nullptr; name const * g_and_elim_left = nullptr; name const * g_and_elim_right = nullptr; @@ -25,6 +26,7 @@ name const * g_congr_arg = nullptr; name const * g_congr_fun = nullptr; name const * g_decidable = nullptr; name const * g_decidable_by_contradiction = nullptr; +name const * g_distrib = nullptr; name const * g_dite = nullptr; name const * g_div = nullptr; name const * g_empty = nullptr; @@ -46,13 +48,17 @@ name const * g_exists_elim = nullptr; name const * g_false = nullptr; name const * g_false_rec = nullptr; name const * g_false_of_true_iff_false = nullptr; +name const * g_field = nullptr; name const * g_funext = nullptr; name const * g_has_zero = nullptr; name const * g_has_one = nullptr; name const * g_has_zero_zero = nullptr; name const * g_has_one_one = nullptr; name const * g_has_add = nullptr; +name const * g_has_div = nullptr; name const * g_has_mul = nullptr; +name const * g_has_neg = nullptr; +name const * g_has_sub = nullptr; name const * g_heq = nullptr; name const * g_heq_refl = nullptr; name const * g_heq_to_eq = nullptr; @@ -73,10 +79,18 @@ name const * g_implies_of_if_pos = nullptr; name const * g_implies_of_if_neg = nullptr; name const * g_is_trunc_is_hprop_elim = nullptr; name const * g_ite = nullptr; +name const * g_le_refl = nullptr; +name const * g_left_distrib = nullptr; +name const * g_linear_ordered_semiring = nullptr; +name const * g_linear_ordered_ring = nullptr; name const * g_lift = nullptr; name const * g_lift_down = nullptr; name const * g_lift_up = nullptr; +name const * g_monoid = nullptr; name const * g_mul = nullptr; +name const * g_mul_one = nullptr; +name const * g_mul_zero_class = nullptr; +name const * g_mul_zero = nullptr; name const * g_nat = nullptr; name const * g_nat_of_num = nullptr; name const * g_nat_succ = nullptr; @@ -86,11 +100,59 @@ name const * g_neg = nullptr; name const * g_not = nullptr; name const * g_not_of_iff_false = nullptr; name const * g_not_of_not_not_not = nullptr; +name const * g_norm_num_add1 = nullptr; +name const * g_norm_num_add1_bit0 = nullptr; +name const * g_norm_num_add1_bit1_helper = nullptr; +name const * g_norm_num_add1_zero = nullptr; +name const * g_norm_num_add1_one = nullptr; +name const * g_norm_num_bin_add_zero = nullptr; +name const * g_norm_num_bin_zero_add = nullptr; +name const * g_norm_num_bit0_add_bit0_helper = nullptr; +name const * g_norm_num_bit1_add_bit0_helper = nullptr; +name const * g_norm_num_bit0_add_bit1_helper = nullptr; +name const * g_norm_num_bit1_add_bit1_helper = nullptr; +name const * g_norm_num_bit0_add_one = nullptr; +name const * g_norm_num_bit1_add_one_helper = nullptr; +name const * g_norm_num_mk_cong = nullptr; +name const * g_norm_num_mul_bit0_helper = nullptr; +name const * g_norm_num_mul_bit1_helper = nullptr; +name const * g_norm_num_one_add_bit1_helper = nullptr; +name const * g_norm_num_one_add_bit0 = nullptr; +name const * g_norm_num_one_add_one = nullptr; +name const * g_norm_num_subst_into_prod = nullptr; +name const * g_norm_num_subst_into_sum = nullptr; +name const * g_norm_num_subst_into_subtr = nullptr; +name const * g_norm_num_neg_add_neg_helper = nullptr; +name const * g_norm_num_neg_add_pos_helper1 = nullptr; +name const * g_norm_num_neg_add_pos_helper2 = nullptr; +name const * g_norm_num_pos_add_neg_helper = nullptr; +name const * g_norm_num_neg_mul_neg_helper = nullptr; +name const * g_norm_num_neg_mul_pos_helper = nullptr; +name const * g_norm_num_pos_mul_neg_helper = nullptr; +name const * g_norm_num_sub_eq_add_neg_helper = nullptr; +name const * g_norm_num_pos_add_pos_helper = nullptr; +name const * g_norm_num_neg_neg_helper = nullptr; +name const * g_norm_num_add_div_helper = nullptr; +name const * g_norm_num_div_add_helper = nullptr; +name const * g_norm_num_nonneg_bit0_helper = nullptr; +name const * g_norm_num_nonneg_bit1_helper = nullptr; +name const * g_norm_num_pos_bit0_helper = nullptr; +name const * g_norm_num_pos_bit1_helper = nullptr; +name const * g_norm_num_nonzero_of_neg_helper = nullptr; +name const * g_norm_num_nonzero_of_pos_helper = nullptr; +name const * g_norm_num_mul_div_helper = nullptr; +name const * g_norm_num_div_mul_helper = nullptr; +name const * g_norm_num_div_helper = nullptr; +name const * g_norm_num_div_eq_div_helper = nullptr; +name const * g_norm_num_subst_into_div = nullptr; +name const * g_norm_num_nonzero_of_div_helper = nullptr; +name const * g_norm_num_neg_zero_helper = nullptr; name const * g_num = nullptr; name const * g_num_zero = nullptr; name const * g_num_pos = nullptr; name const * g_of_iff_true = nullptr; name const * g_one = nullptr; +name const * g_one_mul = nullptr; name const * g_option = nullptr; name const * g_option_some = nullptr; name const * g_option_none = nullptr; @@ -116,12 +178,16 @@ name const * g_prod_pr2 = nullptr; name const * g_propext = nullptr; name const * g_rat_divide = nullptr; name const * g_rat_of_num = nullptr; +name const * g_ring = nullptr; +name const * g_right_distrib = nullptr; +name const * g_semiring = nullptr; name const * g_sigma = nullptr; name const * g_sigma_mk = nullptr; name const * g_sorry = nullptr; name const * g_string = nullptr; name const * g_string_empty = nullptr; name const * g_string_str = nullptr; +name const * g_sub = nullptr; name const * g_subsingleton = nullptr; name const * g_subsingleton_elim = nullptr; name const * g_tactic = nullptr; @@ -188,14 +254,19 @@ name const * g_true = nullptr; name const * g_true_intro = nullptr; name const * g_is_trunc_is_hset = nullptr; name const * g_is_trunc_is_hprop = nullptr; +name const * g_weak_order = nullptr; name const * g_well_founded = nullptr; name const * g_zero = nullptr; +name const * g_zero_mul = nullptr; +name const * g_zero_le_one = nullptr; +name const * g_zero_lt_one = nullptr; void initialize_constants() { g_absurd = new name{"absurd"}; - g_distrib = new name{"distrib"}; - g_left_distrib = new name{"left_distrib"}; - g_right_distrib = new name{"right_distrib"}; g_add = new name{"add"}; + g_add_comm_group = new name{"add_comm_group"}; + g_add_comm_semigroup = new name{"add_comm_semigroup"}; + g_add_monoid = new name{"add_monoid"}; + g_add_group = new name{"add_group"}; g_and = new name{"and"}; g_and_elim_left = new name{"and", "elim_left"}; g_and_elim_right = new name{"and", "elim_right"}; @@ -213,6 +284,7 @@ void initialize_constants() { g_congr_fun = new name{"congr_fun"}; g_decidable = new name{"decidable"}; g_decidable_by_contradiction = new name{"decidable", "by_contradiction"}; + g_distrib = new name{"distrib"}; g_dite = new name{"dite"}; g_div = new name{"div"}; g_empty = new name{"empty"}; @@ -234,13 +306,17 @@ void initialize_constants() { g_false = new name{"false"}; g_false_rec = new name{"false", "rec"}; g_false_of_true_iff_false = new name{"false_of_true_iff_false"}; + g_field = new name{"field"}; g_funext = new name{"funext"}; g_has_zero = new name{"has_zero"}; g_has_one = new name{"has_one"}; g_has_zero_zero = new name{"has_zero", "zero"}; g_has_one_one = new name{"has_one", "one"}; g_has_add = new name{"has_add"}; + g_has_div = new name{"has_div"}; g_has_mul = new name{"has_mul"}; + g_has_neg = new name{"has_neg"}; + g_has_sub = new name{"has_sub"}; g_heq = new name{"heq"}; g_heq_refl = new name{"heq", "refl"}; g_heq_to_eq = new name{"heq", "to_eq"}; @@ -261,10 +337,18 @@ void initialize_constants() { g_implies_of_if_neg = new name{"implies_of_if_neg"}; g_is_trunc_is_hprop_elim = new name{"is_trunc", "is_hprop", "elim"}; g_ite = new name{"ite"}; + g_le_refl = new name{"le", "refl"}; + g_left_distrib = new name{"left_distrib"}; + g_linear_ordered_semiring = new name{"linear_ordered_semiring"}; + g_linear_ordered_ring = new name{"linear_ordered_ring"}; g_lift = new name{"lift"}; g_lift_down = new name{"lift", "down"}; g_lift_up = new name{"lift", "up"}; + g_monoid = new name{"monoid"}; g_mul = new name{"mul"}; + g_mul_one = new name{"mul_one"}; + g_mul_zero_class = new name{"mul_zero_class"}; + g_mul_zero = new name{"mul_zero"}; g_nat = new name{"nat"}; g_nat_of_num = new name{"nat", "of_num"}; g_nat_succ = new name{"nat", "succ"}; @@ -274,11 +358,59 @@ void initialize_constants() { g_not = new name{"not"}; g_not_of_iff_false = new name{"not_of_iff_false"}; g_not_of_not_not_not = new name{"not_of_not_not_not"}; + g_norm_num_add1 = new name{"norm_num", "add1"}; + g_norm_num_add1_bit0 = new name{"norm_num", "add1_bit0"}; + g_norm_num_add1_bit1_helper = new name{"norm_num", "add1_bit1_helper"}; + g_norm_num_add1_zero = new name{"norm_num", "add1_zero"}; + g_norm_num_add1_one = new name{"norm_num", "add1_one"}; + g_norm_num_bin_add_zero = new name{"norm_num", "bin_add_zero"}; + g_norm_num_bin_zero_add = new name{"norm_num", "bin_zero_add"}; + g_norm_num_bit0_add_bit0_helper = new name{"norm_num", "bit0_add_bit0_helper"}; + g_norm_num_bit1_add_bit0_helper = new name{"norm_num", "bit1_add_bit0_helper"}; + g_norm_num_bit0_add_bit1_helper = new name{"norm_num", "bit0_add_bit1_helper"}; + g_norm_num_bit1_add_bit1_helper = new name{"norm_num", "bit1_add_bit1_helper"}; + g_norm_num_bit0_add_one = new name{"norm_num", "bit0_add_one"}; + g_norm_num_bit1_add_one_helper = new name{"norm_num", "bit1_add_one_helper"}; + g_norm_num_mk_cong = new name{"norm_num", "mk_cong"}; + g_norm_num_mul_bit0_helper = new name{"norm_num", "mul_bit0_helper"}; + g_norm_num_mul_bit1_helper = new name{"norm_num", "mul_bit1_helper"}; + g_norm_num_one_add_bit1_helper = new name{"norm_num", "one_add_bit1_helper"}; + g_norm_num_one_add_bit0 = new name{"norm_num", "one_add_bit0"}; + g_norm_num_one_add_one = new name{"norm_num", "one_add_one"}; + g_norm_num_subst_into_prod = new name{"norm_num", "subst_into_prod"}; + g_norm_num_subst_into_sum = new name{"norm_num", "subst_into_sum"}; + g_norm_num_subst_into_subtr = new name{"norm_num", "subst_into_subtr"}; + g_norm_num_neg_add_neg_helper = new name{"norm_num", "neg_add_neg_helper"}; + g_norm_num_neg_add_pos_helper1 = new name{"norm_num", "neg_add_pos_helper1"}; + g_norm_num_neg_add_pos_helper2 = new name{"norm_num", "neg_add_pos_helper2"}; + g_norm_num_pos_add_neg_helper = new name{"norm_num", "pos_add_neg_helper"}; + g_norm_num_neg_mul_neg_helper = new name{"norm_num", "neg_mul_neg_helper"}; + g_norm_num_neg_mul_pos_helper = new name{"norm_num", "neg_mul_pos_helper"}; + g_norm_num_pos_mul_neg_helper = new name{"norm_num", "pos_mul_neg_helper"}; + g_norm_num_sub_eq_add_neg_helper = new name{"norm_num", "sub_eq_add_neg_helper"}; + g_norm_num_pos_add_pos_helper = new name{"norm_num", "pos_add_pos_helper"}; + g_norm_num_neg_neg_helper = new name{"norm_num", "neg_neg_helper"}; + g_norm_num_add_div_helper = new name{"norm_num", "add_div_helper"}; + g_norm_num_div_add_helper = new name{"norm_num", "div_add_helper"}; + g_norm_num_nonneg_bit0_helper = new name{"norm_num", "nonneg_bit0_helper"}; + g_norm_num_nonneg_bit1_helper = new name{"norm_num", "nonneg_bit1_helper"}; + g_norm_num_pos_bit0_helper = new name{"norm_num", "pos_bit0_helper"}; + g_norm_num_pos_bit1_helper = new name{"norm_num", "pos_bit1_helper"}; + g_norm_num_nonzero_of_neg_helper = new name{"norm_num", "nonzero_of_neg_helper"}; + g_norm_num_nonzero_of_pos_helper = new name{"norm_num", "nonzero_of_pos_helper"}; + g_norm_num_mul_div_helper = new name{"norm_num", "mul_div_helper"}; + g_norm_num_div_mul_helper = new name{"norm_num", "div_mul_helper"}; + g_norm_num_div_helper = new name{"norm_num", "div_helper"}; + g_norm_num_div_eq_div_helper = new name{"norm_num", "div_eq_div_helper"}; + g_norm_num_subst_into_div = new name{"norm_num", "subst_into_div"}; + g_norm_num_nonzero_of_div_helper = new name{"norm_num", "nonzero_of_div_helper"}; + g_norm_num_neg_zero_helper = new name{"norm_num", "neg_zero_helper"}; g_num = new name{"num"}; g_num_zero = new name{"num", "zero"}; g_num_pos = new name{"num", "pos"}; g_of_iff_true = new name{"of_iff_true"}; g_one = new name{"one"}; + g_one_mul = new name{"one_mul"}; g_option = new name{"option"}; g_option_some = new name{"option", "some"}; g_option_none = new name{"option", "none"}; @@ -304,12 +436,16 @@ void initialize_constants() { g_propext = new name{"propext"}; g_rat_divide = new name{"rat", "divide"}; g_rat_of_num = new name{"rat", "of_num"}; + g_ring = new name{"ring"}; + g_right_distrib = new name{"right_distrib"}; + g_semiring = new name{"semiring"}; g_sigma = new name{"sigma"}; g_sigma_mk = new name{"sigma", "mk"}; g_sorry = new name{"sorry"}; g_string = new name{"string"}; g_string_empty = new name{"string", "empty"}; g_string_str = new name{"string", "str"}; + g_sub = new name{"sub"}; g_subsingleton = new name{"subsingleton"}; g_subsingleton_elim = new name{"subsingleton", "elim"}; g_tactic = new name{"tactic"}; @@ -376,15 +512,20 @@ void initialize_constants() { g_true_intro = new name{"true", "intro"}; g_is_trunc_is_hset = new name{"is_trunc", "is_hset"}; g_is_trunc_is_hprop = new name{"is_trunc", "is_hprop"}; + g_weak_order = new name{"weak_order"}; g_well_founded = new name{"well_founded"}; g_zero = new name{"zero"}; + g_zero_mul = new name{"zero_mul"}; + g_zero_le_one = new name{"zero_le_one"}; + g_zero_lt_one = new name{"zero_lt_one"}; } void finalize_constants() { delete g_absurd; - delete g_distrib; - delete g_left_distrib; - delete g_right_distrib; delete g_add; + delete g_add_comm_group; + delete g_add_comm_semigroup; + delete g_add_monoid; + delete g_add_group; delete g_and; delete g_and_elim_left; delete g_and_elim_right; @@ -402,6 +543,7 @@ void finalize_constants() { delete g_congr_fun; delete g_decidable; delete g_decidable_by_contradiction; + delete g_distrib; delete g_dite; delete g_div; delete g_empty; @@ -423,13 +565,17 @@ void finalize_constants() { delete g_false; delete g_false_rec; delete g_false_of_true_iff_false; + delete g_field; delete g_funext; delete g_has_zero; delete g_has_one; delete g_has_zero_zero; delete g_has_one_one; delete g_has_add; + delete g_has_div; delete g_has_mul; + delete g_has_neg; + delete g_has_sub; delete g_heq; delete g_heq_refl; delete g_heq_to_eq; @@ -450,10 +596,18 @@ void finalize_constants() { delete g_implies_of_if_neg; delete g_is_trunc_is_hprop_elim; delete g_ite; + delete g_le_refl; + delete g_left_distrib; + delete g_linear_ordered_semiring; + delete g_linear_ordered_ring; delete g_lift; delete g_lift_down; delete g_lift_up; + delete g_monoid; delete g_mul; + delete g_mul_one; + delete g_mul_zero_class; + delete g_mul_zero; delete g_nat; delete g_nat_of_num; delete g_nat_succ; @@ -463,11 +617,59 @@ void finalize_constants() { delete g_not; delete g_not_of_iff_false; delete g_not_of_not_not_not; + delete g_norm_num_add1; + delete g_norm_num_add1_bit0; + delete g_norm_num_add1_bit1_helper; + delete g_norm_num_add1_zero; + delete g_norm_num_add1_one; + delete g_norm_num_bin_add_zero; + delete g_norm_num_bin_zero_add; + delete g_norm_num_bit0_add_bit0_helper; + delete g_norm_num_bit1_add_bit0_helper; + delete g_norm_num_bit0_add_bit1_helper; + delete g_norm_num_bit1_add_bit1_helper; + delete g_norm_num_bit0_add_one; + delete g_norm_num_bit1_add_one_helper; + delete g_norm_num_mk_cong; + delete g_norm_num_mul_bit0_helper; + delete g_norm_num_mul_bit1_helper; + delete g_norm_num_one_add_bit1_helper; + delete g_norm_num_one_add_bit0; + delete g_norm_num_one_add_one; + delete g_norm_num_subst_into_prod; + delete g_norm_num_subst_into_sum; + delete g_norm_num_subst_into_subtr; + delete g_norm_num_neg_add_neg_helper; + delete g_norm_num_neg_add_pos_helper1; + delete g_norm_num_neg_add_pos_helper2; + delete g_norm_num_pos_add_neg_helper; + delete g_norm_num_neg_mul_neg_helper; + delete g_norm_num_neg_mul_pos_helper; + delete g_norm_num_pos_mul_neg_helper; + delete g_norm_num_sub_eq_add_neg_helper; + delete g_norm_num_pos_add_pos_helper; + delete g_norm_num_neg_neg_helper; + delete g_norm_num_add_div_helper; + delete g_norm_num_div_add_helper; + delete g_norm_num_nonneg_bit0_helper; + delete g_norm_num_nonneg_bit1_helper; + delete g_norm_num_pos_bit0_helper; + delete g_norm_num_pos_bit1_helper; + delete g_norm_num_nonzero_of_neg_helper; + delete g_norm_num_nonzero_of_pos_helper; + delete g_norm_num_mul_div_helper; + delete g_norm_num_div_mul_helper; + delete g_norm_num_div_helper; + delete g_norm_num_div_eq_div_helper; + delete g_norm_num_subst_into_div; + delete g_norm_num_nonzero_of_div_helper; + delete g_norm_num_neg_zero_helper; delete g_num; delete g_num_zero; delete g_num_pos; delete g_of_iff_true; delete g_one; + delete g_one_mul; delete g_option; delete g_option_some; delete g_option_none; @@ -493,12 +695,16 @@ void finalize_constants() { delete g_propext; delete g_rat_divide; delete g_rat_of_num; + delete g_ring; + delete g_right_distrib; + delete g_semiring; delete g_sigma; delete g_sigma_mk; delete g_sorry; delete g_string; delete g_string_empty; delete g_string_str; + delete g_sub; delete g_subsingleton; delete g_subsingleton_elim; delete g_tactic; @@ -565,14 +771,19 @@ void finalize_constants() { delete g_true_intro; delete g_is_trunc_is_hset; delete g_is_trunc_is_hprop; + delete g_weak_order; delete g_well_founded; delete g_zero; + delete g_zero_mul; + delete g_zero_le_one; + delete g_zero_lt_one; } name const & get_absurd_name() { return *g_absurd; } -name const & get_distrib_name() { return *g_distrib; } -name const & get_left_distrib_name() { return *g_left_distrib; } -name const & get_right_distrib_name() { return *g_right_distrib; } name const & get_add_name() { return *g_add; } +name const & get_add_comm_group_name() { return *g_add_comm_group; } +name const & get_add_comm_semigroup_name() { return *g_add_comm_semigroup; } +name const & get_add_monoid_name() { return *g_add_monoid; } +name const & get_add_group_name() { return *g_add_group; } name const & get_and_name() { return *g_and; } name const & get_and_elim_left_name() { return *g_and_elim_left; } name const & get_and_elim_right_name() { return *g_and_elim_right; } @@ -590,6 +801,7 @@ name const & get_congr_arg_name() { return *g_congr_arg; } name const & get_congr_fun_name() { return *g_congr_fun; } name const & get_decidable_name() { return *g_decidable; } name const & get_decidable_by_contradiction_name() { return *g_decidable_by_contradiction; } +name const & get_distrib_name() { return *g_distrib; } name const & get_dite_name() { return *g_dite; } name const & get_div_name() { return *g_div; } name const & get_empty_name() { return *g_empty; } @@ -611,13 +823,17 @@ name const & get_exists_elim_name() { return *g_exists_elim; } name const & get_false_name() { return *g_false; } name const & get_false_rec_name() { return *g_false_rec; } name const & get_false_of_true_iff_false_name() { return *g_false_of_true_iff_false; } +name const & get_field_name() { return *g_field; } name const & get_funext_name() { return *g_funext; } name const & get_has_zero_name() { return *g_has_zero; } name const & get_has_one_name() { return *g_has_one; } name const & get_has_zero_zero_name() { return *g_has_zero_zero; } name const & get_has_one_one_name() { return *g_has_one_one; } name const & get_has_add_name() { return *g_has_add; } +name const & get_has_div_name() { return *g_has_div; } name const & get_has_mul_name() { return *g_has_mul; } +name const & get_has_neg_name() { return *g_has_neg; } +name const & get_has_sub_name() { return *g_has_sub; } name const & get_heq_name() { return *g_heq; } name const & get_heq_refl_name() { return *g_heq_refl; } name const & get_heq_to_eq_name() { return *g_heq_to_eq; } @@ -638,10 +854,18 @@ name const & get_implies_of_if_pos_name() { return *g_implies_of_if_pos; } name const & get_implies_of_if_neg_name() { return *g_implies_of_if_neg; } name const & get_is_trunc_is_hprop_elim_name() { return *g_is_trunc_is_hprop_elim; } name const & get_ite_name() { return *g_ite; } +name const & get_le_refl_name() { return *g_le_refl; } +name const & get_left_distrib_name() { return *g_left_distrib; } +name const & get_linear_ordered_semiring_name() { return *g_linear_ordered_semiring; } +name const & get_linear_ordered_ring_name() { return *g_linear_ordered_ring; } 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_monoid_name() { return *g_monoid; } name const & get_mul_name() { return *g_mul; } +name const & get_mul_one_name() { return *g_mul_one; } +name const & get_mul_zero_class_name() { return *g_mul_zero_class; } +name const & get_mul_zero_name() { return *g_mul_zero; } name const & get_nat_name() { return *g_nat; } name const & get_nat_of_num_name() { return *g_nat_of_num; } name const & get_nat_succ_name() { return *g_nat_succ; } @@ -651,11 +875,59 @@ name const & get_neg_name() { return *g_neg; } name const & get_not_name() { return *g_not; } name const & get_not_of_iff_false_name() { return *g_not_of_iff_false; } name const & get_not_of_not_not_not_name() { return *g_not_of_not_not_not; } +name const & get_norm_num_add1_name() { return *g_norm_num_add1; } +name const & get_norm_num_add1_bit0_name() { return *g_norm_num_add1_bit0; } +name const & get_norm_num_add1_bit1_helper_name() { return *g_norm_num_add1_bit1_helper; } +name const & get_norm_num_add1_zero_name() { return *g_norm_num_add1_zero; } +name const & get_norm_num_add1_one_name() { return *g_norm_num_add1_one; } +name const & get_norm_num_bin_add_zero_name() { return *g_norm_num_bin_add_zero; } +name const & get_norm_num_bin_zero_add_name() { return *g_norm_num_bin_zero_add; } +name const & get_norm_num_bit0_add_bit0_helper_name() { return *g_norm_num_bit0_add_bit0_helper; } +name const & get_norm_num_bit1_add_bit0_helper_name() { return *g_norm_num_bit1_add_bit0_helper; } +name const & get_norm_num_bit0_add_bit1_helper_name() { return *g_norm_num_bit0_add_bit1_helper; } +name const & get_norm_num_bit1_add_bit1_helper_name() { return *g_norm_num_bit1_add_bit1_helper; } +name const & get_norm_num_bit0_add_one_name() { return *g_norm_num_bit0_add_one; } +name const & get_norm_num_bit1_add_one_helper_name() { return *g_norm_num_bit1_add_one_helper; } +name const & get_norm_num_mk_cong_name() { return *g_norm_num_mk_cong; } +name const & get_norm_num_mul_bit0_helper_name() { return *g_norm_num_mul_bit0_helper; } +name const & get_norm_num_mul_bit1_helper_name() { return *g_norm_num_mul_bit1_helper; } +name const & get_norm_num_one_add_bit1_helper_name() { return *g_norm_num_one_add_bit1_helper; } +name const & get_norm_num_one_add_bit0_name() { return *g_norm_num_one_add_bit0; } +name const & get_norm_num_one_add_one_name() { return *g_norm_num_one_add_one; } +name const & get_norm_num_subst_into_prod_name() { return *g_norm_num_subst_into_prod; } +name const & get_norm_num_subst_into_sum_name() { return *g_norm_num_subst_into_sum; } +name const & get_norm_num_subst_into_subtr_name() { return *g_norm_num_subst_into_subtr; } +name const & get_norm_num_neg_add_neg_helper_name() { return *g_norm_num_neg_add_neg_helper; } +name const & get_norm_num_neg_add_pos_helper1_name() { return *g_norm_num_neg_add_pos_helper1; } +name const & get_norm_num_neg_add_pos_helper2_name() { return *g_norm_num_neg_add_pos_helper2; } +name const & get_norm_num_pos_add_neg_helper_name() { return *g_norm_num_pos_add_neg_helper; } +name const & get_norm_num_neg_mul_neg_helper_name() { return *g_norm_num_neg_mul_neg_helper; } +name const & get_norm_num_neg_mul_pos_helper_name() { return *g_norm_num_neg_mul_pos_helper; } +name const & get_norm_num_pos_mul_neg_helper_name() { return *g_norm_num_pos_mul_neg_helper; } +name const & get_norm_num_sub_eq_add_neg_helper_name() { return *g_norm_num_sub_eq_add_neg_helper; } +name const & get_norm_num_pos_add_pos_helper_name() { return *g_norm_num_pos_add_pos_helper; } +name const & get_norm_num_neg_neg_helper_name() { return *g_norm_num_neg_neg_helper; } +name const & get_norm_num_add_div_helper_name() { return *g_norm_num_add_div_helper; } +name const & get_norm_num_div_add_helper_name() { return *g_norm_num_div_add_helper; } +name const & get_norm_num_nonneg_bit0_helper_name() { return *g_norm_num_nonneg_bit0_helper; } +name const & get_norm_num_nonneg_bit1_helper_name() { return *g_norm_num_nonneg_bit1_helper; } +name const & get_norm_num_pos_bit0_helper_name() { return *g_norm_num_pos_bit0_helper; } +name const & get_norm_num_pos_bit1_helper_name() { return *g_norm_num_pos_bit1_helper; } +name const & get_norm_num_nonzero_of_neg_helper_name() { return *g_norm_num_nonzero_of_neg_helper; } +name const & get_norm_num_nonzero_of_pos_helper_name() { return *g_norm_num_nonzero_of_pos_helper; } +name const & get_norm_num_mul_div_helper_name() { return *g_norm_num_mul_div_helper; } +name const & get_norm_num_div_mul_helper_name() { return *g_norm_num_div_mul_helper; } +name const & get_norm_num_div_helper_name() { return *g_norm_num_div_helper; } +name const & get_norm_num_div_eq_div_helper_name() { return *g_norm_num_div_eq_div_helper; } +name const & get_norm_num_subst_into_div_name() { return *g_norm_num_subst_into_div; } +name const & get_norm_num_nonzero_of_div_helper_name() { return *g_norm_num_nonzero_of_div_helper; } +name const & get_norm_num_neg_zero_helper_name() { return *g_norm_num_neg_zero_helper; } name const & get_num_name() { return *g_num; } name const & get_num_zero_name() { return *g_num_zero; } name const & get_num_pos_name() { return *g_num_pos; } name const & get_of_iff_true_name() { return *g_of_iff_true; } name const & get_one_name() { return *g_one; } +name const & get_one_mul_name() { return *g_one_mul; } name const & get_option_name() { return *g_option; } name const & get_option_some_name() { return *g_option_some; } name const & get_option_none_name() { return *g_option_none; } @@ -681,12 +953,16 @@ name const & get_prod_pr2_name() { return *g_prod_pr2; } name const & get_propext_name() { return *g_propext; } 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_ring_name() { return *g_ring; } +name const & get_right_distrib_name() { return *g_right_distrib; } +name const & get_semiring_name() { return *g_semiring; } name const & get_sigma_name() { return *g_sigma; } name const & get_sigma_mk_name() { return *g_sigma_mk; } name const & get_sorry_name() { return *g_sorry; } 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; } +name const & get_sub_name() { return *g_sub; } name const & get_subsingleton_name() { return *g_subsingleton; } name const & get_subsingleton_elim_name() { return *g_subsingleton_elim; } name const & get_tactic_name() { return *g_tactic; } @@ -753,6 +1029,10 @@ name const & get_true_name() { return *g_true; } name const & get_true_intro_name() { return *g_true_intro; } name const & get_is_trunc_is_hset_name() { return *g_is_trunc_is_hset; } name const & get_is_trunc_is_hprop_name() { return *g_is_trunc_is_hprop; } +name const & get_weak_order_name() { return *g_weak_order; } name const & get_well_founded_name() { return *g_well_founded; } name const & get_zero_name() { return *g_zero; } +name const & get_zero_mul_name() { return *g_zero_mul; } +name const & get_zero_le_one_name() { return *g_zero_le_one; } +name const & get_zero_lt_one_name() { return *g_zero_lt_one; } } diff --git a/src/library/constants.h b/src/library/constants.h index d3d425d1f..a3e77fa7b 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -6,10 +6,11 @@ namespace lean { void initialize_constants(); void finalize_constants(); name const & get_absurd_name(); -name const & get_distrib_name(); -name const & get_left_distrib_name(); -name const & get_right_distrib_name(); name const & get_add_name(); +name const & get_add_comm_group_name(); +name const & get_add_comm_semigroup_name(); +name const & get_add_monoid_name(); +name const & get_add_group_name(); name const & get_and_name(); name const & get_and_elim_left_name(); name const & get_and_elim_right_name(); @@ -27,6 +28,7 @@ name const & get_congr_arg_name(); name const & get_congr_fun_name(); name const & get_decidable_name(); name const & get_decidable_by_contradiction_name(); +name const & get_distrib_name(); name const & get_dite_name(); name const & get_div_name(); name const & get_empty_name(); @@ -48,13 +50,17 @@ name const & get_exists_elim_name(); name const & get_false_name(); name const & get_false_rec_name(); name const & get_false_of_true_iff_false_name(); +name const & get_field_name(); name const & get_funext_name(); name const & get_has_zero_name(); name const & get_has_one_name(); name const & get_has_zero_zero_name(); name const & get_has_one_one_name(); name const & get_has_add_name(); +name const & get_has_div_name(); name const & get_has_mul_name(); +name const & get_has_neg_name(); +name const & get_has_sub_name(); name const & get_heq_name(); name const & get_heq_refl_name(); name const & get_heq_to_eq_name(); @@ -75,10 +81,18 @@ name const & get_implies_of_if_pos_name(); name const & get_implies_of_if_neg_name(); name const & get_is_trunc_is_hprop_elim_name(); name const & get_ite_name(); +name const & get_le_refl_name(); +name const & get_left_distrib_name(); +name const & get_linear_ordered_semiring_name(); +name const & get_linear_ordered_ring_name(); name const & get_lift_name(); name const & get_lift_down_name(); name const & get_lift_up_name(); +name const & get_monoid_name(); name const & get_mul_name(); +name const & get_mul_one_name(); +name const & get_mul_zero_class_name(); +name const & get_mul_zero_name(); name const & get_nat_name(); name const & get_nat_of_num_name(); name const & get_nat_succ_name(); @@ -88,11 +102,59 @@ name const & get_neg_name(); name const & get_not_name(); name const & get_not_of_iff_false_name(); name const & get_not_of_not_not_not_name(); +name const & get_norm_num_add1_name(); +name const & get_norm_num_add1_bit0_name(); +name const & get_norm_num_add1_bit1_helper_name(); +name const & get_norm_num_add1_zero_name(); +name const & get_norm_num_add1_one_name(); +name const & get_norm_num_bin_add_zero_name(); +name const & get_norm_num_bin_zero_add_name(); +name const & get_norm_num_bit0_add_bit0_helper_name(); +name const & get_norm_num_bit1_add_bit0_helper_name(); +name const & get_norm_num_bit0_add_bit1_helper_name(); +name const & get_norm_num_bit1_add_bit1_helper_name(); +name const & get_norm_num_bit0_add_one_name(); +name const & get_norm_num_bit1_add_one_helper_name(); +name const & get_norm_num_mk_cong_name(); +name const & get_norm_num_mul_bit0_helper_name(); +name const & get_norm_num_mul_bit1_helper_name(); +name const & get_norm_num_one_add_bit1_helper_name(); +name const & get_norm_num_one_add_bit0_name(); +name const & get_norm_num_one_add_one_name(); +name const & get_norm_num_subst_into_prod_name(); +name const & get_norm_num_subst_into_sum_name(); +name const & get_norm_num_subst_into_subtr_name(); +name const & get_norm_num_neg_add_neg_helper_name(); +name const & get_norm_num_neg_add_pos_helper1_name(); +name const & get_norm_num_neg_add_pos_helper2_name(); +name const & get_norm_num_pos_add_neg_helper_name(); +name const & get_norm_num_neg_mul_neg_helper_name(); +name const & get_norm_num_neg_mul_pos_helper_name(); +name const & get_norm_num_pos_mul_neg_helper_name(); +name const & get_norm_num_sub_eq_add_neg_helper_name(); +name const & get_norm_num_pos_add_pos_helper_name(); +name const & get_norm_num_neg_neg_helper_name(); +name const & get_norm_num_add_div_helper_name(); +name const & get_norm_num_div_add_helper_name(); +name const & get_norm_num_nonneg_bit0_helper_name(); +name const & get_norm_num_nonneg_bit1_helper_name(); +name const & get_norm_num_pos_bit0_helper_name(); +name const & get_norm_num_pos_bit1_helper_name(); +name const & get_norm_num_nonzero_of_neg_helper_name(); +name const & get_norm_num_nonzero_of_pos_helper_name(); +name const & get_norm_num_mul_div_helper_name(); +name const & get_norm_num_div_mul_helper_name(); +name const & get_norm_num_div_helper_name(); +name const & get_norm_num_div_eq_div_helper_name(); +name const & get_norm_num_subst_into_div_name(); +name const & get_norm_num_nonzero_of_div_helper_name(); +name const & get_norm_num_neg_zero_helper_name(); name const & get_num_name(); name const & get_num_zero_name(); name const & get_num_pos_name(); name const & get_of_iff_true_name(); name const & get_one_name(); +name const & get_one_mul_name(); name const & get_option_name(); name const & get_option_some_name(); name const & get_option_none_name(); @@ -118,12 +180,16 @@ name const & get_prod_pr2_name(); name const & get_propext_name(); name const & get_rat_divide_name(); name const & get_rat_of_num_name(); +name const & get_ring_name(); +name const & get_right_distrib_name(); +name const & get_semiring_name(); name const & get_sigma_name(); name const & get_sigma_mk_name(); name const & get_sorry_name(); name const & get_string_name(); name const & get_string_empty_name(); name const & get_string_str_name(); +name const & get_sub_name(); name const & get_subsingleton_name(); name const & get_subsingleton_elim_name(); name const & get_tactic_name(); @@ -190,6 +256,10 @@ name const & get_true_name(); name const & get_true_intro_name(); name const & get_is_trunc_is_hset_name(); name const & get_is_trunc_is_hprop_name(); +name const & get_weak_order_name(); name const & get_well_founded_name(); name const & get_zero_name(); +name const & get_zero_mul_name(); +name const & get_zero_le_one_name(); +name const & get_zero_lt_one_name(); } diff --git a/src/library/constants.txt b/src/library/constants.txt index fe281f763..a8eaf34e2 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -1,8 +1,9 @@ absurd -distrib -left_distrib -right_distrib add +add_comm_group +add_comm_semigroup +add_monoid +add_group and and.elim_left and.elim_right @@ -20,6 +21,7 @@ congr_arg congr_fun decidable decidable.by_contradiction +distrib dite div empty @@ -41,13 +43,17 @@ exists.elim false false.rec false_of_true_iff_false +field funext has_zero has_one has_zero.zero has_one.one has_add +has_div has_mul +has_neg +has_sub heq heq.refl heq.to_eq @@ -68,10 +74,18 @@ implies_of_if_pos implies_of_if_neg is_trunc.is_hprop.elim ite +le.refl +left_distrib +linear_ordered_semiring +linear_ordered_ring lift lift.down lift.up +monoid mul +mul_one +mul_zero_class +mul_zero nat nat.of_num nat.succ @@ -81,11 +95,59 @@ neg not not_of_iff_false not_of_not_not_not +norm_num.add1 +norm_num.add1_bit0 +norm_num.add1_bit1_helper +norm_num.add1_zero +norm_num.add1_one +norm_num.bin_add_zero +norm_num.bin_zero_add +norm_num.bit0_add_bit0_helper +norm_num.bit1_add_bit0_helper +norm_num.bit0_add_bit1_helper +norm_num.bit1_add_bit1_helper +norm_num.bit0_add_one +norm_num.bit1_add_one_helper +norm_num.mk_cong +norm_num.mul_bit0_helper +norm_num.mul_bit1_helper +norm_num.one_add_bit1_helper +norm_num.one_add_bit0 +norm_num.one_add_one +norm_num.subst_into_prod +norm_num.subst_into_sum +norm_num.subst_into_subtr +norm_num.neg_add_neg_helper +norm_num.neg_add_pos_helper1 +norm_num.neg_add_pos_helper2 +norm_num.pos_add_neg_helper +norm_num.neg_mul_neg_helper +norm_num.neg_mul_pos_helper +norm_num.pos_mul_neg_helper +norm_num.sub_eq_add_neg_helper +norm_num.pos_add_pos_helper +norm_num.neg_neg_helper +norm_num.add_div_helper +norm_num.div_add_helper +norm_num.nonneg_bit0_helper +norm_num.nonneg_bit1_helper +norm_num.pos_bit0_helper +norm_num.pos_bit1_helper +norm_num.nonzero_of_neg_helper +norm_num.nonzero_of_pos_helper +norm_num.mul_div_helper +norm_num.div_mul_helper +norm_num.div_helper +norm_num.div_eq_div_helper +norm_num.subst_into_div +norm_num.nonzero_of_div_helper +norm_num.neg_zero_helper num num.zero num.pos of_iff_true one +one_mul option option.some option.none @@ -111,12 +173,16 @@ prod.pr2 propext rat.divide rat.of_num +ring +right_distrib +semiring sigma sigma.mk sorry string string.empty string.str +sub subsingleton subsingleton.elim tactic @@ -183,5 +249,9 @@ true true.intro is_trunc.is_hset is_trunc.is_hprop +weak_order well_founded zero +zero_mul +zero_le_one +zero_lt_one diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index 46b687f86..f6be031a3 100644 --- a/src/library/init_module.cpp +++ b/src/library/init_module.cpp @@ -44,7 +44,6 @@ Author: Leonardo de Moura #include "library/aux_recursors.h" #include "library/decl_stats.h" #include "library/meng_paulson.h" -#include "library/norm_num.h" #include "library/class_instance_resolution.h" #include "library/type_context.h" #include "library/congr_lemma_manager.h" @@ -91,7 +90,6 @@ void initialize_library_module() { initialize_aux_recursors(); initialize_decl_stats(); initialize_meng_paulson(); - initialize_norm_num(); initialize_class_instance_resolution(); initialize_type_context(); initialize_light_rule_set(); @@ -105,7 +103,6 @@ void finalize_library_module() { finalize_light_rule_set(); finalize_type_context(); finalize_class_instance_resolution(); - finalize_norm_num(); finalize_meng_paulson(); finalize_decl_stats(); finalize_aux_recursors(); diff --git a/src/library/norm_num.cpp b/src/library/norm_num.cpp index 76d7c7baf..ccc888274 100644 --- a/src/library/norm_num.cpp +++ b/src/library/norm_num.cpp @@ -3,90 +3,10 @@ Copyright (c) 2015 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Author: Robert Y. Lewis */ - #include "library/norm_num.h" #include "library/constants.h" namespace lean { -static name * g_add = nullptr, - * g_add1 = nullptr, - * g_mul = nullptr, - * g_sub = nullptr, - * g_neg = nullptr, - * g_div = nullptr, - * g_bit0_add_bit0 = nullptr, - * g_bit1_add_bit0 = nullptr, - * g_bit0_add_bit1 = nullptr, - * g_bit1_add_bit1 = nullptr, - * g_bin_add_0 = nullptr, - * g_bin_0_add = nullptr, - * g_bin_add_1 = nullptr, - * g_1_add_bit0 = nullptr, - * g_bit0_add_1 = nullptr, - * g_bit1_add_1 = nullptr, - * g_1_add_bit1 = nullptr, - * g_one_add_one = nullptr, - * g_add1_bit0 = nullptr, - * g_add1_bit1 = nullptr, - * g_add1_zero = nullptr, - * g_add1_one = nullptr, - * g_subst_sum = nullptr, - * g_subst_subtr = nullptr, - * g_subst_prod = nullptr, - * g_mk_cong = nullptr, - * g_mk_eq = nullptr, - * g_mul_zero = nullptr, - * g_zero_mul = nullptr, - * g_mul_one = nullptr, - * g_mul_bit0 = nullptr, - * g_mul_bit1 = nullptr, - * g_has_mul = nullptr, - * g_add_monoid = nullptr, - * g_monoid = nullptr, - * g_ring = nullptr, - * g_add_comm = nullptr, - * g_add_group = nullptr, - * g_mul_zero_class = nullptr, - * g_distrib = nullptr, - * g_has_neg = nullptr, - * g_has_sub = nullptr, - * g_has_div = nullptr, - * g_semiring = nullptr, - * g_eq_neg_of_add_eq_zero = nullptr, - * g_neg_add_neg_eq = nullptr, - * g_neg_add_pos1 = nullptr, - * g_neg_add_pos2 = nullptr, - * g_pos_add_neg = nullptr, - * g_pos_add_pos = nullptr, - * g_neg_mul_neg = nullptr, - * g_pos_mul_neg = nullptr, - * g_neg_mul_pos = nullptr, - * g_sub_eq_add_neg = nullptr, - * g_neg_neg = nullptr, - * g_div_add = nullptr, - * g_add_div = nullptr, - * g_lin_ord_ring = nullptr, - * g_lin_ord_semiring = nullptr, - * g_wk_order = nullptr, - * g_bit0_nonneg = nullptr, - * g_bit1_nonneg = nullptr, - * g_zero_le_one = nullptr, - * g_le_refl = nullptr, - * g_bit0_pos = nullptr, - * g_bit1_pos = nullptr, - * g_zero_lt_one = nullptr, - * g_field = nullptr, - * g_nonzero_neg = nullptr, - * g_nonzero_pos = nullptr, - * g_div_mul = nullptr, - * g_mul_div = nullptr, - * g_div_helper = nullptr, - * g_div_eq_div_helper = nullptr, - * g_subst_div = nullptr, - * g_nonzero_div = nullptr, - * g_neg_zero = nullptr, - * g_add_comm_group = nullptr; - static bool is_numeral_aux(expr const & e, bool is_first) { buffer args; expr const & f = get_app_args(e, args); @@ -110,11 +30,11 @@ bool norm_num_context::is_numeral(expr const & e) const { } bool norm_num_context::is_neg_app(expr const & e) const { - return is_const_app(e, *g_neg, 3); + return is_const_app(e, get_neg_name(), 3); } bool norm_num_context::is_div(expr const & e) const { - return is_const_app(e, *g_div, 4); + return is_const_app(e, get_div_name(), 4); } /* @@ -136,7 +56,7 @@ expr norm_num_context::mk_has_add(expr const & e) { } expr norm_num_context::mk_has_mul(expr const & e) { - auto l_name = *g_has_mul; + auto l_name = get_has_mul_name(); if (instances.find(l_name) != instances.end()) { return instances[l_name]; } @@ -181,7 +101,7 @@ expr norm_num_context::mk_has_zero(expr const & e) { } expr norm_num_context::mk_add_monoid(expr const & e) { - auto l_name = *g_add_monoid; + auto l_name = get_add_monoid_name(); if (instances.find(l_name) != instances.end()) { return instances[l_name]; } @@ -196,7 +116,7 @@ expr norm_num_context::mk_add_monoid(expr const & e) { } expr norm_num_context::mk_monoid(expr const & e) { - auto l_name = *g_monoid; + auto l_name = get_monoid_name(); if (instances.find(l_name) != instances.end()) { return instances[l_name]; } @@ -211,7 +131,7 @@ expr norm_num_context::mk_monoid(expr const & e) { } expr norm_num_context::mk_field(expr const & e) { - expr t = mk_app(mk_constant(*g_field, m_lvls), e); + expr t = mk_app(mk_constant(get_field_name(), m_lvls), e); optional inst = m_type_ctx.mk_class_instance(t); if (inst) { return *inst; @@ -221,7 +141,7 @@ expr norm_num_context::mk_field(expr const & e) { } expr norm_num_context::mk_add_comm(expr const & e) { - auto l_name = *g_add_comm; + auto l_name = get_add_comm_semigroup_name(); if (instances.find(l_name) != instances.end()) { return instances[l_name]; } @@ -236,7 +156,7 @@ expr norm_num_context::mk_add_comm(expr const & e) { } expr norm_num_context::mk_add_group(expr const & e) { - auto l_name = *g_add_group; + auto l_name = get_add_group_name(); if (instances.find(l_name) != instances.end()) { return instances[l_name]; } @@ -251,7 +171,7 @@ expr norm_num_context::mk_add_group(expr const & e) { } expr norm_num_context::mk_has_distrib(expr const & e) { - auto l_name = *g_distrib; + auto l_name = get_distrib_name(); if (instances.find(l_name) != instances.end()) { return instances[l_name]; } @@ -266,7 +186,7 @@ expr norm_num_context::mk_has_distrib(expr const & e) { } expr norm_num_context::mk_mul_zero_class(expr const & e) { - auto l_name = *g_mul_zero_class; + auto l_name = get_mul_zero_class_name(); if (instances.find(l_name) != instances.end()) { return instances[l_name]; } @@ -281,7 +201,7 @@ expr norm_num_context::mk_mul_zero_class(expr const & e) { } expr norm_num_context::mk_semiring(expr const & e) { - auto l_name = *g_semiring; + auto l_name = get_semiring_name(); if (instances.find(l_name) != instances.end()) { return instances[l_name]; } @@ -296,7 +216,7 @@ expr norm_num_context::mk_semiring(expr const & e) { } expr norm_num_context::mk_has_neg(expr const & e) { - auto l_name = *g_has_neg; + auto l_name = get_has_neg_name(); if (instances.find(l_name) != instances.end()) { return instances[l_name]; } @@ -311,7 +231,7 @@ expr norm_num_context::mk_has_neg(expr const & e) { } expr norm_num_context::mk_has_sub(expr const & e) { - auto l_name = *g_has_sub; + auto l_name = get_has_sub_name(); if (instances.find(l_name) != instances.end()) { return instances[l_name]; } @@ -326,7 +246,7 @@ expr norm_num_context::mk_has_sub(expr const & e) { } expr norm_num_context::mk_has_div(expr const & e) { - auto l_name = *g_has_div; + auto l_name = get_has_div_name(); if (instances.find(l_name) != instances.end()) { return instances[l_name]; } @@ -341,7 +261,7 @@ expr norm_num_context::mk_has_div(expr const & e) { } expr norm_num_context::mk_add_comm_group(expr const & e) { - auto l_name = *g_add_comm_group; + auto l_name = get_add_comm_group_name(); if (instances.find(l_name) != instances.end()) { return instances[l_name]; } @@ -356,7 +276,7 @@ expr norm_num_context::mk_add_comm_group(expr const & e) { } expr norm_num_context::mk_ring(expr const & e) { - auto l_name = *g_ring; + auto l_name = get_ring_name(); if (instances.find(l_name) != instances.end()) { return instances[l_name]; } @@ -371,7 +291,7 @@ expr norm_num_context::mk_ring(expr const & e) { } expr norm_num_context::mk_lin_ord_ring(expr const & e) { - auto l_name = *g_lin_ord_ring; + auto l_name = get_linear_ordered_ring_name(); if (instances.find(l_name) != instances.end()) { return instances[l_name]; } @@ -386,7 +306,7 @@ expr norm_num_context::mk_lin_ord_ring(expr const & e) { } expr norm_num_context::mk_lin_ord_semiring(expr const & e) { - auto l_name = *g_lin_ord_semiring; + auto l_name = get_linear_ordered_semiring_name(); if (instances.find(l_name) != instances.end()) { return instances[l_name]; } @@ -401,7 +321,7 @@ expr norm_num_context::mk_lin_ord_semiring(expr const & e) { } expr norm_num_context::mk_wk_order(expr const & e) { - auto l_name = *g_wk_order; + auto l_name = get_weak_order_name(); if (instances.find(l_name) != instances.end()) { return instances[l_name]; } @@ -421,7 +341,7 @@ expr norm_num_context::mk_const(name const & n) { expr norm_num_context::mk_cong(expr const & op, expr const & type, expr const & a, expr const & b, expr const & eq) { - return mk_app({mk_const(*g_mk_cong), type, op, a, b, eq}); + return mk_app({mk_const(get_norm_num_mk_cong_name()), type, op, a, b, eq}); } // returns such that p is a proof that lhs + rhs = t. @@ -440,52 +360,52 @@ pair norm_num_context::mk_norm_add(expr const & lhs, expr const & rh if (is_bit0(lhs) && is_bit0(rhs)) { // typec is has_add auto p = mk_norm_add(args_lhs[2], args_rhs[2]); rv = mk_app(lhs_head, type, typec, p.first); - prf = mk_app({mk_const(*g_bit0_add_bit0), type, mk_add_comm(type), + prf = mk_app({mk_const(get_norm_num_bit0_add_bit0_helper_name()), type, mk_add_comm(type), args_lhs[2], args_rhs[2], p.first, p.second}); } else if (is_bit0(lhs) && is_bit1(rhs)) { auto p = mk_norm_add(args_lhs[2], args_rhs[3]); rv = mk_app({rhs_head, type, args_rhs[1], args_rhs[2], p.first}); - prf = mk_app({mk_const(*g_bit0_add_bit1), type, mk_add_comm(type), args_rhs[1], + prf = mk_app({mk_const(get_norm_num_bit0_add_bit1_helper_name()), type, mk_add_comm(type), args_rhs[1], args_lhs[2], args_rhs[3], p.first, p.second}); } else if (is_bit0(lhs) && is_one(rhs)) { rv = mk_app({mk_const(get_bit1_name()), type, args_rhs[1], args_lhs[1], args_lhs[2]}); - prf = mk_app({mk_const(*g_bit0_add_1), type, typec, args_rhs[1], args_lhs[2]}); + prf = mk_app({mk_const(get_norm_num_bit0_add_one_name()), type, typec, args_rhs[1], args_lhs[2]}); } else if (is_bit1(lhs) && is_bit0(rhs)) { // typec is has_one auto p = mk_norm_add(args_lhs[3], args_rhs[2]); rv = mk_app(lhs_head, type, typec, args_lhs[2], p.first); - prf = mk_app({mk_const(*g_bit1_add_bit0), type, mk_add_comm(type), typec, + prf = mk_app({mk_const(get_norm_num_bit1_add_bit0_helper_name()), type, mk_add_comm(type), typec, args_lhs[3], args_rhs[2], p.first, p.second}); } else if (is_bit1(lhs) && is_bit1(rhs)) { // typec is has_one auto add_ts = mk_norm_add(args_lhs[3], args_rhs[3]); - expr add1 = mk_app({mk_const(*g_add1), type, args_lhs[2], typec, add_ts.first}); + expr add1 = mk_app({mk_const(get_norm_num_add1_name()), type, args_lhs[2], typec, add_ts.first}); auto p = mk_norm_add1(add1); rv = mk_app({mk_const(get_bit0_name()), type, args_lhs[2], p.first}); - prf = mk_app({mk_const(*g_bit1_add_bit1), type, mk_add_comm(type), typec, + prf = mk_app({mk_const(get_norm_num_bit1_add_bit1_helper_name()), type, mk_add_comm(type), typec, args_lhs[3], args_rhs[3], add_ts.first, p.first, add_ts.second, p.second}); } else if (is_bit1(lhs) && is_one(rhs)) { // typec is has_one - expr add1 = mk_app({mk_const(*g_add1), type, args_lhs[2], typec, lhs}); + expr add1 = mk_app({mk_const(get_norm_num_add1_name()), type, args_lhs[2], typec, lhs}); auto p = mk_norm_add1(add1); rv = p.first; - prf = mk_app({mk_const(*g_bit1_add_1), type, args_lhs[2], typec, + prf = mk_app({mk_const(get_norm_num_bit1_add_one_helper_name()), type, args_lhs[2], typec, args_lhs[3], p.first, p.second}); } else if (is_one(lhs) && is_bit0(rhs)) { // typec is has_one rv = mk_app({mk_const(get_bit1_name()), type, typec, args_rhs[1], args_rhs[2]}); - prf = mk_app({mk_const(*g_1_add_bit0), type, mk_add_comm(type), typec, args_rhs[2]}); + prf = mk_app({mk_const(get_norm_num_one_add_bit0_name()), type, mk_add_comm(type), typec, args_rhs[2]}); } else if (is_one(lhs) && is_bit1(rhs)) { // typec is has_one - expr add1 = mk_app({mk_const(*g_add1), type, args_rhs[2], args_rhs[1], rhs}); + expr add1 = mk_app({mk_const(get_norm_num_add1_name()), type, args_rhs[2], args_rhs[1], rhs}); auto p = mk_norm_add1(add1); rv = p.first; - prf = mk_app({mk_const(*g_1_add_bit1), type, mk_add_comm(type), typec, + prf = mk_app({mk_const(get_norm_num_one_add_bit1_helper_name()), type, mk_add_comm(type), typec, args_rhs[3], p.first, p.second}); } else if (is_one(lhs) && is_one(rhs)) { rv = mk_app({mk_const(get_bit0_name()), type, mk_has_add(type), lhs}); - prf = mk_app({mk_const(*g_one_add_one), type, mk_has_add(type), typec}); + prf = mk_app({mk_const(get_norm_num_one_add_one_name()), type, mk_has_add(type), typec}); } else if (is_zero(lhs)) { rv = rhs; - prf = mk_app({mk_const(*g_bin_0_add), type, mk_add_monoid(type), rhs}); + prf = mk_app({mk_const(get_norm_num_bin_zero_add_name()), type, mk_add_monoid(type), rhs}); } else if (is_zero(rhs)) { rv = lhs; - prf = mk_app({mk_const(*g_bin_add_0), type, mk_add_monoid(type), lhs}); + prf = mk_app({mk_const(get_norm_num_bin_add_zero_name()), type, mk_add_monoid(type), lhs}); } else { throw exception("mk_norm_add got malformed args"); } @@ -504,19 +424,19 @@ pair norm_num_context::mk_norm_add1(expr const & e) { if (is_bit0(p)) { auto has_one = args[2]; rv = mk_app({mk_const(get_bit1_name()), args[0], args[2], args[1], ne_args[2]}); - prf = mk_app({mk_const(*g_add1_bit0), args[0], args[1], args[2], ne_args[2]}); + prf = mk_app({mk_const(get_norm_num_add1_bit0_name()), args[0], args[1], args[2], ne_args[2]}); } else if (is_bit1(p)) { // ne_args : has_one, has_add - auto np = mk_norm_add1(mk_app({mk_const(*g_add1), args[0], args[1], args[2], ne_args[3]})); + auto np = mk_norm_add1(mk_app({mk_const(get_norm_num_add1_name()), args[0], args[1], args[2], ne_args[3]})); rv = mk_app({mk_const(get_bit0_name()), args[0], args[1], np.first}); - prf = mk_app({mk_const(*g_add1_bit1), args[0], mk_add_comm(args[0]), + prf = mk_app({mk_const(get_norm_num_add1_bit1_helper_name()), args[0], mk_add_comm(args[0]), args[2], ne_args[3], np.first, np.second}); } else if (is_zero(p)) { rv = mk_app({mk_const(get_one_name()), args[0], args[2]}); - prf = mk_app({mk_const(*g_add1_zero), args[0], mk_add_monoid(args[0]), args[2]}); + prf = mk_app({mk_const(get_norm_num_add1_zero_name()), args[0], mk_add_monoid(args[0]), args[2]}); } else if (is_one(p)) { rv = mk_app({mk_const(get_bit0_name()), args[0], args[1], mk_app({mk_const(get_one_name()), args[0], args[2]})}); - prf = mk_app({mk_const(*g_add1_one), args[0], args[1], args[2]}); + prf = mk_app({mk_const(get_norm_num_add1_one_name()), args[0], args[1], args[2]}); } else { throw exception("malformed add1"); } @@ -537,24 +457,24 @@ pair norm_num_context::mk_norm_mul(expr const & lhs, expr const & rh expr prf; if (is_zero(rhs)) { rv = rhs; - prf = mk_app({mk_const(*g_mul_zero), type, mk_mul_zero_class(type), lhs}); + prf = mk_app({mk_const(get_mul_zero_name()), type, mk_mul_zero_class(type), lhs}); } else if (is_zero(lhs)) { rv = lhs; - prf = mk_app({mk_const(*g_zero_mul), type, mk_mul_zero_class(type), rhs}); + prf = mk_app({mk_const(get_zero_mul_name()), type, mk_mul_zero_class(type), rhs}); } else if (is_one(rhs)) { rv = lhs; - prf = mk_app({mk_const(*g_mul_one), type, mk_monoid(type), lhs}); + prf = mk_app({mk_const(get_mul_one_name()), type, mk_monoid(type), lhs}); } else if (is_bit0(rhs)) { auto mtp = mk_norm_mul(lhs, args_rhs[2]); rv = mk_app({rhs_head, type, typec, mtp.first}); - prf = mk_app({mk_const(*g_mul_bit0), type, mk_has_distrib(type), lhs, + prf = mk_app({mk_const(get_norm_num_mul_bit0_helper_name()), type, mk_has_distrib(type), lhs, args_rhs[2], mtp.first, mtp.second}); } else if (is_bit1(rhs)) { auto mtp = mk_norm_mul(lhs, args_rhs[3]); auto atp = mk_norm_add(mk_app({mk_const(get_bit0_name()), type, args_rhs[2], mtp.first}), lhs); rv = atp.first; - prf = mk_app({mk_const(*g_mul_bit1), type, mk_semiring(type), lhs, args_rhs[3], + prf = mk_app({mk_const(get_norm_num_mul_bit1_helper_name()), type, mk_semiring(type), lhs, args_rhs[3], mtp.first, atp.first, mtp.second, atp.second}); } else { throw exception("mk_norm_mul got malformed args"); @@ -576,19 +496,19 @@ mpq norm_num_context:: mpq_of_expr(expr const & e){ expr f = get_app_args(e, args); if (!is_constant(f)) { throw exception("cannot find num of nonconstant"); - } else if (const_name(f) == *g_add && args.size() == 4) { + } else if (const_name(f) == get_add_name() && args.size() == 4) { return mpq_of_expr(args[2]) + mpq_of_expr(args[3]); - } else if (const_name(f) == *g_mul && args.size() == 4) { + } else if (const_name(f) == get_mul_name() && args.size() == 4) { return mpq_of_expr(args[2]) * mpq_of_expr(args[3]); - } else if (const_name(f) == *g_sub && args.size() == 4) { + } else if (const_name(f) == get_sub_name() && args.size() == 4) { return mpq_of_expr(args[2]) - mpq_of_expr(args[3]); - } else if (const_name(f) == *g_div && args.size() == 4) { + } else if (const_name(f) == get_div_name() && args.size() == 4) { mpq num = mpq_of_expr(args[2]), den = mpq_of_expr(args[3]); if (den != 0) return mpq_of_expr(args[2]) / mpq_of_expr(args[3]); else throw exception("divide by 0"); - } else if (const_name(f) == *g_neg && args.size() == 3) { + } else if (const_name(f) == get_neg_name() && args.size() == 3) { return neg(mpq_of_expr(args[2])); } else { auto v = to_mpq(e); @@ -610,13 +530,13 @@ mpz norm_num_context::num_of_expr(expr const & e) { if (v) { return *v; } - if (const_name(f) == *g_add && args.size() == 4) { + if (const_name(f) == get_add_name() && args.size() == 4) { return num_of_expr(args[2]) + num_of_expr(args[3]); - } else if (const_name(f) == *g_mul && args.size() == 4) { + } else if (const_name(f) == get_mul_name() && args.size() == 4) { return num_of_expr(args[2]) * num_of_expr(args[3]); - } else if (const_name(f) == *g_sub && args.size() == 4) { + } else if (const_name(f) == get_sub_name() && args.size() == 4) { return num_of_expr(args[2]) - num_of_expr(args[3]); - } else if (const_name(f) == *g_neg && args.size() == 3) { + } else if (const_name(f) == get_neg_name() && args.size() == 3) { return neg(num_of_expr(args[2])); } else { throw exception("expression in num_of_expr is malfomed"); @@ -640,7 +560,7 @@ expr norm_num_context::mk_norm_eq_neg_add_neg(expr & s_lhs, expr & s_rhs, expr & auto rhs_v = get_type_and_arg_of_neg(rhs); expr type = rhs_v.first; auto sum_pr = mk_norm(mk_add(type, s_lhs_v, s_rhs_v)).second; - return mk_app({mk_const(*g_neg_add_neg_eq), type, mk_add_comm_group(type), + return mk_app({mk_const(get_norm_num_neg_add_neg_helper_name()), type, mk_add_comm_group(type), s_lhs_v, s_rhs_v, rhs_v.second, sum_pr}); } @@ -652,11 +572,11 @@ expr norm_num_context::mk_norm_eq_neg_add_pos(expr & s_lhs, expr & s_rhs, expr & if (is_neg_app(rhs)) { auto rhs_v = get_type_and_arg_of_neg(rhs).second; auto sum_pr = mk_norm(mk_add(type, s_rhs, rhs_v)).second; - return mk_app({mk_const(*g_neg_add_pos1), type, mk_add_comm_group(type), + return mk_app({mk_const(get_norm_num_neg_add_pos_helper1_name()), type, mk_add_comm_group(type), s_lhs_v.second, s_rhs, rhs_v, sum_pr}); } else { auto sum_pr = mk_norm(mk_add(type, s_lhs_v.second, rhs)).second; - return mk_app({mk_const(*g_neg_add_pos2), type, mk_add_comm_group(type), + return mk_app({mk_const(get_norm_num_neg_add_pos_helper2_name()), type, mk_add_comm_group(type), s_lhs_v.second, s_rhs, rhs, sum_pr}); } } @@ -666,7 +586,7 @@ expr norm_num_context::mk_norm_eq_pos_add_neg(expr & s_lhs, expr & s_rhs, expr & lean_assert(!is_neg_app(s_lhs)); expr prf = mk_norm_eq_neg_add_pos(s_rhs, s_lhs, rhs); expr type = get_type_and_arg_of_neg(s_rhs).first; - return mk_app({mk_const(*g_pos_add_neg), type, mk_add_comm_group(type), s_lhs, + return mk_app({mk_const(get_norm_num_pos_add_neg_helper_name()), type, mk_add_comm_group(type), s_lhs, s_rhs, rhs, prf}); } @@ -683,13 +603,13 @@ expr norm_num_context::mk_norm_eq_pos_add_pos(expr & s_lhs, expr & s_rhs, expr & expr norm_num_context::mk_norm_eq_neg_mul_neg(expr & s_lhs, expr & s_rhs, expr & rhs) { lean_assert(is_neg_app(s_lhs)); lean_assert(is_neg_app(s_rhs)); - lean_assert(is_neg_app(rhs)); + // lean_assert(is_neg_app(rhs)); // Leo: we get an assertion violation when testing norm_num1.lean auto s_lhs_v = get_type_and_arg_of_neg(s_lhs).second; expr s_rhs_v, type; std::tie(type, s_rhs_v) = get_type_and_arg_of_neg(s_rhs); auto prod_pr = mk_norm(mk_mul(type, s_lhs_v, s_rhs_v)); lean_assert(to_num(rhs) == to_num(prod_pr.first)); - return mk_app({mk_const(*g_neg_mul_neg), type, mk_ring(type), s_lhs_v, + return mk_app({mk_const(get_norm_num_neg_mul_neg_helper_name()), type, mk_ring(type), s_lhs_v, s_rhs_v, rhs, prod_pr.second}); } @@ -701,7 +621,7 @@ expr norm_num_context::mk_norm_eq_neg_mul_pos(expr & s_lhs, expr & s_rhs, expr & std::tie(type, s_lhs_v) = get_type_and_arg_of_neg(s_lhs); auto rhs_v = get_type_and_arg_of_neg(rhs).second; auto prod_pr = mk_norm(mk_mul(type, s_lhs_v, s_rhs)); - return mk_app({mk_const(*g_neg_mul_pos), type, mk_ring(type), s_lhs_v, s_rhs, + return mk_app({mk_const(get_norm_num_neg_mul_pos_helper_name()), type, mk_ring(type), s_lhs_v, s_rhs, rhs_v, prod_pr.second}); } @@ -713,7 +633,7 @@ expr norm_num_context::mk_norm_eq_pos_mul_neg(expr & s_lhs, expr & s_rhs, expr & std::tie(type, s_rhs_v) = get_type_and_arg_of_neg(s_rhs); auto rhs_v = get_type_and_arg_of_neg(rhs).second; auto prod_pr = mk_norm(mk_mul(type, s_lhs, s_rhs_v)); - return mk_app({mk_const(*g_pos_mul_neg), type, mk_ring(type), s_lhs, s_rhs_v, + return mk_app({mk_const(get_norm_num_pos_mul_neg_helper_name()), type, mk_ring(type), s_lhs, s_rhs_v, rhs_v, prod_pr.second}); } @@ -764,22 +684,22 @@ expr norm_num_context::from_mpq(mpq const & q, expr const & type) { expr norm_num_context::mk_div(expr const & type, expr const & e1, expr const & e2) { auto has_div = mk_has_div(type); - return mk_app({mk_const(*g_div), type, has_div, e1, e2}); + return mk_app({mk_const(get_div_name()), type, has_div, e1, e2}); } expr norm_num_context::mk_neg(expr const & type, expr const & e) { auto has_neg = mk_has_neg(type); - return mk_app({mk_const(*g_neg), type, has_neg, e}); + return mk_app({mk_const(get_neg_name()), type, has_neg, e}); } expr norm_num_context::mk_add(expr const & type, expr const & e1, expr const & e2) { auto has_add = mk_has_add(type); - return mk_app({mk_const(*g_add), type, has_add, e1, e2}); + return mk_app({mk_const(get_add_name()), type, has_add, e1, e2}); } expr norm_num_context::mk_mul(expr const & type, expr const & e1, expr const & e2) { auto has_mul = mk_has_mul(type); - return mk_app({mk_const(*g_mul), type, has_mul, e1, e2}); + return mk_app({mk_const(get_mul_name()), type, has_mul, e1, e2}); } // s_lhs is div. returns proof that s_lhs + s_rhs = rhs @@ -793,7 +713,7 @@ expr norm_num_context::mk_norm_div_add(expr & s_lhs, expr & s_rhs, expr & rhs) { auto npr_r = mk_norm(mk_mul(type, rhs, den)); lean_assert(to_mpq(npr_l.first) == to_mpq(npr_r.first)); expr den_neq_zero = mk_nonzero_prf(den); - return mk_app({mk_const(*g_div_add), type, mk_field(type), num, den, s_rhs, rhs, + return mk_app({mk_const(get_norm_num_div_add_helper_name()), type, mk_field(type), num, den, s_rhs, rhs, npr_l.first, den_neq_zero, npr_l.second, npr_r.second}); } @@ -808,7 +728,7 @@ expr norm_num_context::mk_norm_add_div(expr & s_lhs, expr & s_rhs, expr & rhs) { auto npr_r = mk_norm(mk_mul(type, den, rhs)); lean_assert(to_mpq(npr_l.first) == to_mpq(npr_r.first)); expr den_neq_zero = mk_nonzero_prf(den); - return mk_app({mk_const(*g_add_div), type, mk_field(type), num, den, s_lhs, rhs, + return mk_app({mk_const(get_norm_num_add_div_helper_name()), type, mk_field(type), num, den, s_lhs, rhs, npr_l.first, den_neq_zero, npr_l.second, npr_r.second}); } @@ -816,15 +736,15 @@ expr norm_num_context::mk_norm_add_div(expr & s_lhs, expr & s_rhs, expr & rhs) { expr norm_num_context::mk_nonzero_prf(expr const & e) { buffer args; expr f = get_app_args(e, args); - if (const_name(f) == *g_neg) { - return mk_app({mk_const(*g_nonzero_neg), args[0], mk_lin_ord_ring(args[0]), + if (const_name(f) == get_neg_name()) { + return mk_app({mk_const(get_norm_num_nonzero_of_neg_helper_name()), args[0], mk_lin_ord_ring(args[0]), args[2], mk_nonzero_prf(args[2])}); - } else if (const_name(f) == *g_div) { + } else if (const_name(f) == get_div_name()) { expr num_pr = mk_nonzero_prf(args[2]), den_pr = mk_nonzero_prf(args[3]); - return mk_app({mk_const(*g_nonzero_div), args[0], mk_field(args[0]), args[2], + return mk_app({mk_const(get_norm_num_nonzero_of_div_helper_name()), args[0], mk_field(args[0]), args[2], args[3], num_pr, den_pr}); } else { - return mk_app({mk_const(*g_nonzero_pos), args[0], mk_lin_ord_semiring(args[0]), + return mk_app({mk_const(get_norm_num_nonzero_of_pos_helper_name()), args[0], mk_lin_ord_semiring(args[0]), e, mk_pos_prf(e)}); } } @@ -837,12 +757,12 @@ expr norm_num_context::mk_pos_prf(expr const & e) { expr prf; if (is_bit0(e)) { prf = mk_pos_prf(args[2]); - return mk_app({mk_const(*g_bit0_pos), type, mk_lin_ord_semiring(type), args[2], prf}); + return mk_app({mk_const(get_norm_num_pos_bit0_helper_name()), type, mk_lin_ord_semiring(type), args[2], prf}); } else if (is_bit1(e)) { prf = mk_nonneg_prf(args[3]); - return mk_app({mk_const(*g_bit1_pos), type, mk_lin_ord_semiring(type), args[3], prf}); + return mk_app({mk_const(get_norm_num_pos_bit1_helper_name()), type, mk_lin_ord_semiring(type), args[3], prf}); } else if (is_one(e)) { - return mk_app({mk_const(*g_zero_lt_one), type, mk_lin_ord_semiring(type)}); + return mk_app({mk_const(get_zero_lt_one_name()), type, mk_lin_ord_semiring(type)}); } else { throw exception("mk_pos_proof called on zero or non_numeral"); } @@ -855,14 +775,14 @@ expr norm_num_context::mk_nonneg_prf(expr const & e) { expr prf; if (is_bit0(e)) { prf = mk_nonneg_prf(args[2]); - return mk_app({mk_const(*g_bit0_nonneg), type, mk_lin_ord_semiring(type), args[2], prf}); + return mk_app({mk_const(get_norm_num_nonneg_bit0_helper_name()), type, mk_lin_ord_semiring(type), args[2], prf}); } else if (is_bit1(e)) { prf = mk_nonneg_prf(args[3]); - return mk_app({mk_const(*g_bit1_nonneg), type, mk_lin_ord_semiring(type), args[3], prf}); + return mk_app({mk_const(get_norm_num_nonneg_bit1_helper_name()), type, mk_lin_ord_semiring(type), args[3], prf}); } else if (is_one(e)) { - return mk_app({mk_const(*g_zero_le_one), type, mk_lin_ord_ring(type)}); + return mk_app({mk_const(get_zero_le_one_name()), type, mk_lin_ord_ring(type)}); } else if (is_zero(e)) { - return mk_app({mk_const(*g_le_refl), type, mk_wk_order(type), + return mk_app({mk_const(get_le_refl_name()), type, mk_wk_order(type), mk_app({mk_const(get_zero_name()), type, mk_has_zero(type)})}); } else { throw exception("mk_nonneg_proof called on zero or non_numeral"); @@ -878,7 +798,7 @@ expr norm_num_context::mk_norm_div_mul(expr & s_lhs, expr & s_rhs, expr & rhs) { auto prf = mk_norm(mk_div(type, new_num, args[3])); lean_assert(to_mpq(prf.first) == to_mpq(rhs)); expr den_ne_zero = mk_nonzero_prf(args[3]); - return mk_app({mk_const(*g_div_mul), type, mk_field(type), args[2], args[3], s_rhs, + return mk_app({mk_const(get_norm_num_div_mul_helper_name()), type, mk_field(type), args[2], args[3], s_rhs, rhs, den_ne_zero, prf.second}); } @@ -890,7 +810,7 @@ expr norm_num_context::mk_norm_mul_div(expr & s_lhs, expr & s_rhs, expr & rhs) { auto prf = mk_norm(mk_div(type, new_num, args[3])); lean_assert(to_mpq(prf.first) == to_mpq(rhs)); expr den_ne_zero = mk_nonzero_prf(args[3]); - return mk_app({mk_const(*g_mul_div), type, mk_field(type), s_lhs, args[2], args[3], + return mk_app({mk_const(get_norm_num_mul_div_helper_name()), type, mk_field(type), s_lhs, args[2], args[3], rhs, den_ne_zero, prf.second}); } @@ -903,7 +823,7 @@ pair norm_num_context::mk_norm(expr const & e) { m_lvls = const_levels(f); expr type = args[0]; if (is_numeral(e)) { - expr prf = mk_app({mk_const(*g_mk_eq), type, e}); + expr prf = mk_app({mk_const(get_eq_refl_name()), type, e}); return pair(e, prf); } mpq val = mpq_of_expr(e); @@ -913,7 +833,7 @@ pair norm_num_context::mk_norm(expr const & e) { } else { nval = mk_neg(type, from_mpq(neg(val), type)); } - if (const_name(f) == *g_add && args.size() == 4) { + if (const_name(f) == get_add_name() && args.size() == 4) { expr prf; auto lhs_p = mk_norm(args[2]); auto rhs_p = mk_norm(args[3]); @@ -936,21 +856,21 @@ pair norm_num_context::mk_norm(expr const & e) { } } } - expr rprf = mk_app({mk_const(*g_subst_sum), type, mk_has_add(type), args[2], args[3], + expr rprf = mk_app({mk_const(get_norm_num_subst_into_sum_name()), type, mk_has_add(type), args[2], args[3], lhs_p.first, rhs_p.first, nval, lhs_p.second, rhs_p.second, prf}); return pair(nval, rprf); - } else if (const_name(f) == *g_sub && args.size() == 4) { + } else if (const_name(f) == get_sub_name() && args.size() == 4) { expr sum = mk_add(args[0], args[2], mk_neg(args[0], args[3])); auto anprf = mk_norm(sum); - expr rprf = mk_app({mk_const(*g_subst_subtr), type, mk_add_group(type), args[2], + expr rprf = mk_app({mk_const(get_norm_num_subst_into_subtr_name()), type, mk_add_group(type), args[2], args[3], anprf.first, anprf.second}); return pair(nval, rprf); - } else if (const_name(f) == *g_neg && args.size() == 3) { + } else if (const_name(f) == get_neg_name() && args.size() == 3) { auto prf = mk_norm(args[2]); lean_assert(mpq_of_expr(prf.first) == neg(val)); if (is_zero(prf.first)) { - expr rprf = mk_app({mk_const(*g_neg_zero), type, mk_add_group(type), args[2], + expr rprf = mk_app({mk_const(get_norm_num_neg_zero_helper_name()), type, mk_add_group(type), args[2], prf.second}); return pair(prf.first, rprf); } @@ -962,11 +882,11 @@ pair norm_num_context::mk_norm(expr const & e) { nval_args[2], prf.second); return pair(nval, rprf); } else { - expr rprf = mk_app({mk_const(*g_neg_neg), type, mk_add_group(type), + expr rprf = mk_app({mk_const(get_norm_num_neg_neg_helper_name()), type, mk_add_group(type), args[2], nval, prf.second}); return pair(nval, rprf); } - } else if (const_name(f) == *g_mul && args.size() == 4) { + } else if (const_name(f) == get_mul_name() && args.size() == 4) { auto lhs_p = mk_norm(args[2]); auto rhs_p = mk_norm(args[3]); expr prf; @@ -989,10 +909,10 @@ pair norm_num_context::mk_norm(expr const & e) { prf = mk_norm_eq_pos_mul_pos(lhs_p.first, rhs_p.first, nval); } } - expr rprf = mk_app({mk_const(*g_subst_prod), type, mk_has_mul(args[0]), args[2], args[3], + expr rprf = mk_app({mk_const(get_norm_num_subst_into_prod_name()), type, mk_has_mul(args[0]), args[2], args[3], lhs_p.first, rhs_p.first, nval, lhs_p.second, rhs_p.second, prf}); return pair(nval, rprf); - } else if (const_name(f) == *g_div && args.size() == 4) { + } else if (const_name(f) == get_div_name() && args.size() == 4) { auto lhs_p = mk_norm(args[2]); auto rhs_p = mk_norm(args[3]); expr prf; @@ -1004,7 +924,7 @@ pair norm_num_context::mk_norm(expr const & e) { auto rhs_mul = mk_norm(mk_mul(type, nval_num, rhs_p.first)); expr den_nonzero = mk_nonzero_prf(rhs_p.first); expr nval_den_nonzero = mk_nonzero_prf(nval_den); - prf = mk_app({mk_const(*g_div_eq_div_helper), type, mk_field(type), + prf = mk_app({mk_const(get_norm_num_div_eq_div_helper_name()), type, mk_field(type), lhs_p.first, rhs_p.first, nval_num, nval_den, lhs_mul.first, lhs_mul.second, rhs_mul.second, den_nonzero, nval_den_nonzero}); } else { @@ -1014,10 +934,10 @@ pair norm_num_context::mk_norm(expr const & e) { lean_assert(*val1 == *val2); } expr den_nonzero = mk_nonzero_prf(rhs_p.first); - prf = mk_app({mk_const(*g_div_helper), type, mk_field(type), + prf = mk_app({mk_const(get_norm_num_div_helper_name()), type, mk_field(type), lhs_p.first, rhs_p.first, nval, den_nonzero, prod.second}); } - expr rprf = mk_app({mk_const(*g_subst_div), type, mk_has_div(type), + expr rprf = mk_app({mk_const(get_norm_num_subst_into_div_name()), type, mk_has_div(type), lhs_p.first, rhs_p.first, args[2], args[3], nval, prf, lhs_p.second, rhs_p.second}); return pair(nval, rprf); @@ -1038,171 +958,9 @@ pair norm_num_context::mk_norm(expr const & e) { return pair(nval, rprf); } else if ((const_name(f) == get_zero_name() || const_name(f) == get_one_name()) && args.size() == 2) { - return pair(e, mk_app({mk_const(*g_mk_eq), args[0], e})); + return pair(e, mk_app({mk_const(get_eq_refl_name()), args[0], e})); } else { throw exception("mk_norm found unrecognized combo "); } } - -void initialize_norm_num() { - g_add = new name("add"); - g_add1 = new name("norm_num", "add1"); - g_mul = new name("mul"); - g_sub = new name("sub"); - g_neg = new name("neg"); - g_div = new name("div"); - g_bit0_add_bit0 = new name("norm_num", "bit0_add_bit0_helper"); - g_bit1_add_bit0 = new name("norm_num", "bit1_add_bit0_helper"); - g_bit0_add_bit1 = new name("norm_num", "bit0_add_bit1_helper"); - g_bit1_add_bit1 = new name("norm_num", "bit1_add_bit1_helper"); - g_bin_add_0 = new name("norm_num", "bin_add_zero"); - g_bin_0_add = new name("norm_num", "bin_zero_add"); - g_bin_add_1 = new name("norm_num", "bin_add_one"); - g_1_add_bit0 = new name("norm_num", "one_add_bit0"); - g_bit0_add_1 = new name("norm_num", "bit0_add_one"); - g_bit1_add_1 = new name("norm_num", "bit1_add_one_helper"); - g_1_add_bit1 = new name("norm_num", "one_add_bit1_helper"); - g_one_add_one = new name("norm_num", "one_add_one"); - g_add1_bit0 = new name("norm_num", "add1_bit0"); - g_add1_bit1 = new name("norm_num", "add1_bit1_helper"); - g_add1_zero = new name("norm_num", "add1_zero"); - g_add1_one = new name("norm_num", "add1_one"); - g_subst_sum = new name("norm_num", "subst_into_sum"); - g_subst_subtr = new name("norm_num", "subst_into_subtr"); - g_subst_prod = new name("norm_num", "subst_into_prod"); - g_mk_cong = new name("norm_num", "mk_cong"); - g_mk_eq = new name("norm_num", "mk_eq"); - g_zero_mul = new name("norm_num", "zero_mul"); - g_mul_zero = new name("norm_num", "mul_zero"); - g_mul_one = new name("norm_num", "mul_one"); - g_mul_bit0 = new name("norm_num", "mul_bit0_helper"); - g_mul_bit1 = new name("norm_num", "mul_bit1_helper"); - g_has_mul = new name("has_mul"); - g_add_monoid = new name("add_monoid"); - g_ring = new name("ring"); - g_monoid = new name("monoid"); - g_add_comm = new name("add_comm_semigroup"); - g_add_group = new name("add_group"); - g_mul_zero_class= new name("mul_zero_class"); - g_distrib = new name("distrib"); - g_has_neg = new name("has_neg"); - g_has_sub = new name("has_sub"); - g_has_div = new name("has_div"); - g_semiring = new name("semiring"); - g_lin_ord_ring = new name("linear_ordered_ring"); - g_lin_ord_semiring = new name("linear_ordered_semiring"); - g_eq_neg_of_add_eq_zero = new name("eq_neg_of_add_eq_zero"); - g_neg_add_neg_eq = new name("norm_num", "neg_add_neg_helper"); - g_neg_add_pos1 = new name("norm_num", "neg_add_pos_helper1"); - g_neg_add_pos2 = new name("norm_num", "neg_add_pos_helper2"); - g_pos_add_neg = new name("norm_num", "pos_add_neg_helper"); - g_neg_mul_neg = new name("norm_num", "neg_mul_neg_helper"); - g_neg_mul_pos = new name("norm_num", "neg_mul_pos_helper"); - g_pos_mul_neg = new name("norm_num", "pos_mul_neg_helper"); - g_sub_eq_add_neg= new name("norm_num", "sub_eq_add_neg_helper"); - g_pos_add_pos = new name("norm_num", "pos_add_pos_helper"); - g_neg_neg = new name("norm_num", "neg_neg_helper"); - g_add_comm_group= new name("add_comm_group"); - g_add_div = new name("norm_num", "add_div_helper"); - g_div_add = new name("norm_num", "div_add_helper"); - g_bit0_nonneg = new name("norm_num", "nonneg_bit0_helper"); - g_bit1_nonneg = new name("norm_num", "nonneg_bit1_helper"); - g_zero_le_one = new name("zero_le_one"); - g_le_refl = new name("le.refl"); - g_bit0_pos = new name("norm_num", "pos_bit0_helper"); - g_bit1_pos = new name("norm_num", "pos_bit1_helper"); - g_zero_lt_one = new name("zero_lt_one"); - g_wk_order = new name("weak_order"); - g_field = new name("field"); - g_nonzero_neg = new name("norm_num", "nonzero_of_neg_helper"); - g_nonzero_pos = new name("norm_num", "nonzero_of_pos_helper"); - g_mul_div = new name("norm_num", "mul_div_helper"); - g_div_mul = new name("norm_num", "div_mul_helper"); - g_div_helper = new name("norm_num", "div_helper"); - g_div_eq_div_helper = new name("norm_num", "div_eq_div_helper"); - g_subst_div = new name("norm_num", "subst_into_div"); - g_nonzero_div = new name("norm_num", "nonzero_of_div_helper"); - g_neg_zero = new name("norm_num", "neg_zero_helper"); -} - -void finalize_norm_num() { - delete g_add; - delete g_add1; - delete g_mul; - delete g_sub; - delete g_neg; - delete g_div; - delete g_bit0_add_bit0; - delete g_bit1_add_bit0; - delete g_bit0_add_bit1; - delete g_bit1_add_bit1; - delete g_bin_add_0; - delete g_bin_0_add; - delete g_bin_add_1; - delete g_1_add_bit0; - delete g_bit0_add_1; - delete g_bit1_add_1; - delete g_1_add_bit1; - delete g_one_add_one; - delete g_add1_bit0; - delete g_add1_bit1; - delete g_add1_zero; - delete g_add1_one; - delete g_subst_sum; - delete g_subst_subtr; - delete g_subst_prod; - delete g_mk_cong; - delete g_mk_eq; - delete g_mul_zero; - delete g_zero_mul; - delete g_mul_one; - delete g_mul_bit0; - delete g_mul_bit1; - delete g_has_mul; - delete g_add_monoid; - delete g_monoid; - delete g_ring; - delete g_add_comm; - delete g_add_group; - delete g_mul_zero_class; - delete g_distrib; - delete g_has_neg; - delete g_has_sub; - delete g_has_div; - delete g_semiring; - delete g_eq_neg_of_add_eq_zero; - delete g_neg_add_neg_eq; - delete g_neg_add_pos1; - delete g_neg_add_pos2; - delete g_pos_add_neg; - delete g_pos_add_pos; - delete g_neg_mul_neg; - delete g_neg_mul_pos; - delete g_pos_mul_neg; - delete g_sub_eq_add_neg; - delete g_neg_neg; - delete g_add_comm_group; - delete g_div_add; - delete g_add_div; - delete g_bit0_nonneg; - delete g_bit1_nonneg; - delete g_zero_le_one; - delete g_le_refl; - delete g_bit0_pos; - delete g_bit1_pos; - delete g_zero_lt_one; - delete g_wk_order; - delete g_div_mul; - delete g_div_helper; - delete g_div_eq_div_helper; - delete g_mul_div; - delete g_nonzero_div; - delete g_neg_zero; - delete g_lin_ord_ring; - delete g_lin_ord_semiring; - delete g_field; - delete g_nonzero_neg; - delete g_subst_div; - delete g_nonzero_pos; -} } diff --git a/src/library/norm_num.h b/src/library/norm_num.h index 94e75ffec..1286a54fd 100644 --- a/src/library/norm_num.h +++ b/src/library/norm_num.h @@ -103,7 +103,4 @@ inline mpz num_of_expr(type_context & type_ctx, expr const & e) { inline mpq mpq_of_expr(type_context & type_ctx, expr const & e) { return norm_num_context(type_ctx).mpq_of_expr(e); } - -void initialize_norm_num(); -void finalize_norm_num(); } diff --git a/src/library/tactic/CMakeLists.txt b/src/library/tactic/CMakeLists.txt index f701a25a3..4f1d9d62e 100644 --- a/src/library/tactic/CMakeLists.txt +++ b/src/library/tactic/CMakeLists.txt @@ -6,4 +6,5 @@ expr_to_tactic.cpp location.cpp rewrite_tactic.cpp util.cpp init_module.cpp change_tactic.cpp check_expr_tactic.cpp let_tactic.cpp contradiction_tactic.cpp exfalso_tactic.cpp constructor_tactic.cpp injection_tactic.cpp congruence_tactic.cpp relation_tactics.cpp -induction_tactic.cpp subst_tactic.cpp unfold_rec.cpp with_options_tactic.cpp) \ No newline at end of file +induction_tactic.cpp subst_tactic.cpp unfold_rec.cpp with_options_tactic.cpp +norm_num_tactic.cpp) \ No newline at end of file diff --git a/src/library/tactic/init_module.cpp b/src/library/tactic/init_module.cpp index 76c457dd7..1ad835195 100644 --- a/src/library/tactic/init_module.cpp +++ b/src/library/tactic/init_module.cpp @@ -32,6 +32,7 @@ Author: Leonardo de Moura #include "library/tactic/subst_tactic.h" #include "library/tactic/location.h" #include "library/tactic/with_options_tactic.h" +#include "library/tactic/norm_num_tactic.h" namespace lean { void initialize_tactic_module() { @@ -62,9 +63,11 @@ void initialize_tactic_module() { initialize_subst_tactic(); initialize_location(); initialize_with_options_tactic(); + initialize_norm_num_tactic(); } void finalize_tactic_module() { + finalize_norm_num_tactic(); finalize_with_options_tactic(); finalize_location(); finalize_subst_tactic(); diff --git a/src/library/tactic/norm_num_tactic.cpp b/src/library/tactic/norm_num_tactic.cpp index 696ce5745..b917b59e2 100644 --- a/src/library/tactic/norm_num_tactic.cpp +++ b/src/library/tactic/norm_num_tactic.cpp @@ -8,11 +8,12 @@ Author: Robert Y. Lewis #include "library/reducible.h" #include "library/normalize.h" #include "library/norm_num.h" +#include "library/tmp_type_context.h" #include "library/tactic/expr_to_tactic.h" namespace lean { tactic norm_num_tactic() { - return tactic01([=](environment const & env, io_state const &, proof_state const & s) { + return tactic01([=](environment const & env, io_state const & ios, proof_state const & s) { goals const & gs = s.get_goals(); if (empty(gs)) { throw_no_goal_if_enabled(s); @@ -30,15 +31,16 @@ tactic norm_num_tactic() { rhs = normalize(*rtc, rhs); buffer hyps; g.get_hyps(hyps); - local_context ctx(to_list(hyps)); try { - pair p = mk_norm_num(env, ctx, lhs); + tmp_type_context ctx(env, ios.get_options()); + ctx.set_local_instances(to_list(hyps)); + pair p = mk_norm_num(ctx, lhs); expr new_lhs = p.first; expr new_lhs_pr = p.second; - pair p2 = mk_norm_num(env, ctx, rhs); + pair p2 = mk_norm_num(ctx, rhs); expr new_rhs = p2.first; expr new_rhs_pr = p2.second; - mpq v_lhs = mpq_of_expr(env, ctx, new_lhs), v_rhs = mpq_of_expr(env, ctx, new_rhs); + mpq v_lhs = mpq_of_expr(ctx, new_lhs), v_rhs = mpq_of_expr(ctx, new_rhs); if (v_lhs == v_rhs) { type_checker tc(env); expr g_prf = mk_trans(tc, new_lhs_pr, mk_symm(tc, new_rhs_pr)); diff --git a/tests/lean/extra/num_norm1.lean b/tests/lean/run/num_norm1.lean similarity index 99% rename from tests/lean/extra/num_norm1.lean rename to tests/lean/run/num_norm1.lean index a974c4f4d..6a2f3e3c6 100644 --- a/tests/lean/extra/num_norm1.lean +++ b/tests/lean/run/num_norm1.lean @@ -1,5 +1,5 @@ import data.real -open algebra real +open real /- variable {A : Type}