refactor(library/norm_num): avoid manual constant name initialization
@rlewis1988 We group all Lean constants used in the C++ code at
src/library/constants.txt
Jeremy and Floris check this file before renaming constants in the
library. So, they can quickly decide whether C++ code will be affected
or not.
We also have a python script for initializing the C++ name objects.
To use the script:
- go to src/library
- execute
python ../../script/gen_constants_cpp.py constants.txt
It will create the boring initialization and finalization code, and
declare a procedure get_<id>_name() for each constant in the file constants.txt.
I also move the norm_num1.lean to the set of unit tests that are
executed whenever we push a commit to the main branch.
I found an assertion violation at line 606. Could you take a look?
Best,
Leo
This commit is contained in:
Leonardo de Moura
parent
e3a35ba4fd
commit
193a9d8cde
11 changed files with 547 additions and 371 deletions
|
|
@ -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 :=
|
theorem mk_cong (op : A → A) (a b : A) (H : a = b) : op a = op b :=
|
||||||
by congruence; exact H
|
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) :
|
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 :=
|
-a + -b = c :=
|
||||||
begin
|
begin
|
||||||
|
|
|
||||||
|
|
@ -4,10 +4,11 @@
|
||||||
#include "util/name.h"
|
#include "util/name.h"
|
||||||
namespace lean{
|
namespace lean{
|
||||||
name const * g_absurd = nullptr;
|
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 = 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 = nullptr;
|
||||||
name const * g_and_elim_left = nullptr;
|
name const * g_and_elim_left = nullptr;
|
||||||
name const * g_and_elim_right = 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_congr_fun = nullptr;
|
||||||
name const * g_decidable = nullptr;
|
name const * g_decidable = nullptr;
|
||||||
name const * g_decidable_by_contradiction = nullptr;
|
name const * g_decidable_by_contradiction = nullptr;
|
||||||
|
name const * g_distrib = nullptr;
|
||||||
name const * g_dite = nullptr;
|
name const * g_dite = nullptr;
|
||||||
name const * g_div = nullptr;
|
name const * g_div = nullptr;
|
||||||
name const * g_empty = 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 = nullptr;
|
||||||
name const * g_false_rec = nullptr;
|
name const * g_false_rec = nullptr;
|
||||||
name const * g_false_of_true_iff_false = nullptr;
|
name const * g_false_of_true_iff_false = nullptr;
|
||||||
|
name const * g_field = nullptr;
|
||||||
name const * g_funext = nullptr;
|
name const * g_funext = nullptr;
|
||||||
name const * g_has_zero = nullptr;
|
name const * g_has_zero = nullptr;
|
||||||
name const * g_has_one = nullptr;
|
name const * g_has_one = nullptr;
|
||||||
name const * g_has_zero_zero = nullptr;
|
name const * g_has_zero_zero = nullptr;
|
||||||
name const * g_has_one_one = nullptr;
|
name const * g_has_one_one = nullptr;
|
||||||
name const * g_has_add = nullptr;
|
name const * g_has_add = nullptr;
|
||||||
|
name const * g_has_div = nullptr;
|
||||||
name const * g_has_mul = 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 = nullptr;
|
||||||
name const * g_heq_refl = nullptr;
|
name const * g_heq_refl = nullptr;
|
||||||
name const * g_heq_to_eq = 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_implies_of_if_neg = nullptr;
|
||||||
name const * g_is_trunc_is_hprop_elim = nullptr;
|
name const * g_is_trunc_is_hprop_elim = nullptr;
|
||||||
name const * g_ite = 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 = nullptr;
|
||||||
name const * g_lift_down = nullptr;
|
name const * g_lift_down = nullptr;
|
||||||
name const * g_lift_up = nullptr;
|
name const * g_lift_up = nullptr;
|
||||||
|
name const * g_monoid = nullptr;
|
||||||
name const * g_mul = 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 = nullptr;
|
||||||
name const * g_nat_of_num = nullptr;
|
name const * g_nat_of_num = nullptr;
|
||||||
name const * g_nat_succ = 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 = nullptr;
|
||||||
name const * g_not_of_iff_false = nullptr;
|
name const * g_not_of_iff_false = nullptr;
|
||||||
name const * g_not_of_not_not_not = 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 = nullptr;
|
||||||
name const * g_num_zero = nullptr;
|
name const * g_num_zero = nullptr;
|
||||||
name const * g_num_pos = nullptr;
|
name const * g_num_pos = nullptr;
|
||||||
name const * g_of_iff_true = nullptr;
|
name const * g_of_iff_true = nullptr;
|
||||||
name const * g_one = nullptr;
|
name const * g_one = nullptr;
|
||||||
|
name const * g_one_mul = nullptr;
|
||||||
name const * g_option = nullptr;
|
name const * g_option = nullptr;
|
||||||
name const * g_option_some = nullptr;
|
name const * g_option_some = nullptr;
|
||||||
name const * g_option_none = 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_propext = nullptr;
|
||||||
name const * g_rat_divide = nullptr;
|
name const * g_rat_divide = nullptr;
|
||||||
name const * g_rat_of_num = 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 = nullptr;
|
||||||
name const * g_sigma_mk = nullptr;
|
name const * g_sigma_mk = nullptr;
|
||||||
name const * g_sorry = nullptr;
|
name const * g_sorry = nullptr;
|
||||||
name const * g_string = nullptr;
|
name const * g_string = nullptr;
|
||||||
name const * g_string_empty = nullptr;
|
name const * g_string_empty = nullptr;
|
||||||
name const * g_string_str = nullptr;
|
name const * g_string_str = nullptr;
|
||||||
|
name const * g_sub = nullptr;
|
||||||
name const * g_subsingleton = nullptr;
|
name const * g_subsingleton = nullptr;
|
||||||
name const * g_subsingleton_elim = nullptr;
|
name const * g_subsingleton_elim = nullptr;
|
||||||
name const * g_tactic = nullptr;
|
name const * g_tactic = nullptr;
|
||||||
|
|
@ -188,14 +254,19 @@ name const * g_true = nullptr;
|
||||||
name const * g_true_intro = nullptr;
|
name const * g_true_intro = nullptr;
|
||||||
name const * g_is_trunc_is_hset = nullptr;
|
name const * g_is_trunc_is_hset = nullptr;
|
||||||
name const * g_is_trunc_is_hprop = nullptr;
|
name const * g_is_trunc_is_hprop = nullptr;
|
||||||
|
name const * g_weak_order = nullptr;
|
||||||
name const * g_well_founded = nullptr;
|
name const * g_well_founded = nullptr;
|
||||||
name const * g_zero = 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() {
|
void initialize_constants() {
|
||||||
g_absurd = new name{"absurd"};
|
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 = 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 = new name{"and"};
|
||||||
g_and_elim_left = new name{"and", "elim_left"};
|
g_and_elim_left = new name{"and", "elim_left"};
|
||||||
g_and_elim_right = new name{"and", "elim_right"};
|
g_and_elim_right = new name{"and", "elim_right"};
|
||||||
|
|
@ -213,6 +284,7 @@ void initialize_constants() {
|
||||||
g_congr_fun = new name{"congr_fun"};
|
g_congr_fun = new name{"congr_fun"};
|
||||||
g_decidable = new name{"decidable"};
|
g_decidable = new name{"decidable"};
|
||||||
g_decidable_by_contradiction = new name{"decidable", "by_contradiction"};
|
g_decidable_by_contradiction = new name{"decidable", "by_contradiction"};
|
||||||
|
g_distrib = new name{"distrib"};
|
||||||
g_dite = new name{"dite"};
|
g_dite = new name{"dite"};
|
||||||
g_div = new name{"div"};
|
g_div = new name{"div"};
|
||||||
g_empty = new name{"empty"};
|
g_empty = new name{"empty"};
|
||||||
|
|
@ -234,13 +306,17 @@ void initialize_constants() {
|
||||||
g_false = new name{"false"};
|
g_false = new name{"false"};
|
||||||
g_false_rec = new name{"false", "rec"};
|
g_false_rec = new name{"false", "rec"};
|
||||||
g_false_of_true_iff_false = new name{"false_of_true_iff_false"};
|
g_false_of_true_iff_false = new name{"false_of_true_iff_false"};
|
||||||
|
g_field = new name{"field"};
|
||||||
g_funext = new name{"funext"};
|
g_funext = new name{"funext"};
|
||||||
g_has_zero = new name{"has_zero"};
|
g_has_zero = new name{"has_zero"};
|
||||||
g_has_one = new name{"has_one"};
|
g_has_one = new name{"has_one"};
|
||||||
g_has_zero_zero = new name{"has_zero", "zero"};
|
g_has_zero_zero = new name{"has_zero", "zero"};
|
||||||
g_has_one_one = new name{"has_one", "one"};
|
g_has_one_one = new name{"has_one", "one"};
|
||||||
g_has_add = new name{"has_add"};
|
g_has_add = new name{"has_add"};
|
||||||
|
g_has_div = new name{"has_div"};
|
||||||
g_has_mul = new name{"has_mul"};
|
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 = new name{"heq"};
|
||||||
g_heq_refl = new name{"heq", "refl"};
|
g_heq_refl = new name{"heq", "refl"};
|
||||||
g_heq_to_eq = new name{"heq", "to_eq"};
|
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_implies_of_if_neg = new name{"implies_of_if_neg"};
|
||||||
g_is_trunc_is_hprop_elim = new name{"is_trunc", "is_hprop", "elim"};
|
g_is_trunc_is_hprop_elim = new name{"is_trunc", "is_hprop", "elim"};
|
||||||
g_ite = new name{"ite"};
|
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 = new name{"lift"};
|
||||||
g_lift_down = new name{"lift", "down"};
|
g_lift_down = new name{"lift", "down"};
|
||||||
g_lift_up = new name{"lift", "up"};
|
g_lift_up = new name{"lift", "up"};
|
||||||
|
g_monoid = new name{"monoid"};
|
||||||
g_mul = new name{"mul"};
|
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 = new name{"nat"};
|
||||||
g_nat_of_num = new name{"nat", "of_num"};
|
g_nat_of_num = new name{"nat", "of_num"};
|
||||||
g_nat_succ = new name{"nat", "succ"};
|
g_nat_succ = new name{"nat", "succ"};
|
||||||
|
|
@ -274,11 +358,59 @@ void initialize_constants() {
|
||||||
g_not = new name{"not"};
|
g_not = new name{"not"};
|
||||||
g_not_of_iff_false = new name{"not_of_iff_false"};
|
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_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 = new name{"num"};
|
||||||
g_num_zero = new name{"num", "zero"};
|
g_num_zero = new name{"num", "zero"};
|
||||||
g_num_pos = new name{"num", "pos"};
|
g_num_pos = new name{"num", "pos"};
|
||||||
g_of_iff_true = new name{"of_iff_true"};
|
g_of_iff_true = new name{"of_iff_true"};
|
||||||
g_one = new name{"one"};
|
g_one = new name{"one"};
|
||||||
|
g_one_mul = new name{"one_mul"};
|
||||||
g_option = new name{"option"};
|
g_option = new name{"option"};
|
||||||
g_option_some = new name{"option", "some"};
|
g_option_some = new name{"option", "some"};
|
||||||
g_option_none = new name{"option", "none"};
|
g_option_none = new name{"option", "none"};
|
||||||
|
|
@ -304,12 +436,16 @@ void initialize_constants() {
|
||||||
g_propext = new name{"propext"};
|
g_propext = new name{"propext"};
|
||||||
g_rat_divide = new name{"rat", "divide"};
|
g_rat_divide = new name{"rat", "divide"};
|
||||||
g_rat_of_num = new name{"rat", "of_num"};
|
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 = new name{"sigma"};
|
||||||
g_sigma_mk = new name{"sigma", "mk"};
|
g_sigma_mk = new name{"sigma", "mk"};
|
||||||
g_sorry = new name{"sorry"};
|
g_sorry = new name{"sorry"};
|
||||||
g_string = new name{"string"};
|
g_string = new name{"string"};
|
||||||
g_string_empty = new name{"string", "empty"};
|
g_string_empty = new name{"string", "empty"};
|
||||||
g_string_str = new name{"string", "str"};
|
g_string_str = new name{"string", "str"};
|
||||||
|
g_sub = new name{"sub"};
|
||||||
g_subsingleton = new name{"subsingleton"};
|
g_subsingleton = new name{"subsingleton"};
|
||||||
g_subsingleton_elim = new name{"subsingleton", "elim"};
|
g_subsingleton_elim = new name{"subsingleton", "elim"};
|
||||||
g_tactic = new name{"tactic"};
|
g_tactic = new name{"tactic"};
|
||||||
|
|
@ -376,15 +512,20 @@ void initialize_constants() {
|
||||||
g_true_intro = new name{"true", "intro"};
|
g_true_intro = new name{"true", "intro"};
|
||||||
g_is_trunc_is_hset = new name{"is_trunc", "is_hset"};
|
g_is_trunc_is_hset = new name{"is_trunc", "is_hset"};
|
||||||
g_is_trunc_is_hprop = new name{"is_trunc", "is_hprop"};
|
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_well_founded = new name{"well_founded"};
|
||||||
g_zero = new name{"zero"};
|
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() {
|
void finalize_constants() {
|
||||||
delete g_absurd;
|
delete g_absurd;
|
||||||
delete g_distrib;
|
|
||||||
delete g_left_distrib;
|
|
||||||
delete g_right_distrib;
|
|
||||||
delete g_add;
|
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;
|
||||||
delete g_and_elim_left;
|
delete g_and_elim_left;
|
||||||
delete g_and_elim_right;
|
delete g_and_elim_right;
|
||||||
|
|
@ -402,6 +543,7 @@ void finalize_constants() {
|
||||||
delete g_congr_fun;
|
delete g_congr_fun;
|
||||||
delete g_decidable;
|
delete g_decidable;
|
||||||
delete g_decidable_by_contradiction;
|
delete g_decidable_by_contradiction;
|
||||||
|
delete g_distrib;
|
||||||
delete g_dite;
|
delete g_dite;
|
||||||
delete g_div;
|
delete g_div;
|
||||||
delete g_empty;
|
delete g_empty;
|
||||||
|
|
@ -423,13 +565,17 @@ void finalize_constants() {
|
||||||
delete g_false;
|
delete g_false;
|
||||||
delete g_false_rec;
|
delete g_false_rec;
|
||||||
delete g_false_of_true_iff_false;
|
delete g_false_of_true_iff_false;
|
||||||
|
delete g_field;
|
||||||
delete g_funext;
|
delete g_funext;
|
||||||
delete g_has_zero;
|
delete g_has_zero;
|
||||||
delete g_has_one;
|
delete g_has_one;
|
||||||
delete g_has_zero_zero;
|
delete g_has_zero_zero;
|
||||||
delete g_has_one_one;
|
delete g_has_one_one;
|
||||||
delete g_has_add;
|
delete g_has_add;
|
||||||
|
delete g_has_div;
|
||||||
delete g_has_mul;
|
delete g_has_mul;
|
||||||
|
delete g_has_neg;
|
||||||
|
delete g_has_sub;
|
||||||
delete g_heq;
|
delete g_heq;
|
||||||
delete g_heq_refl;
|
delete g_heq_refl;
|
||||||
delete g_heq_to_eq;
|
delete g_heq_to_eq;
|
||||||
|
|
@ -450,10 +596,18 @@ void finalize_constants() {
|
||||||
delete g_implies_of_if_neg;
|
delete g_implies_of_if_neg;
|
||||||
delete g_is_trunc_is_hprop_elim;
|
delete g_is_trunc_is_hprop_elim;
|
||||||
delete g_ite;
|
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;
|
||||||
delete g_lift_down;
|
delete g_lift_down;
|
||||||
delete g_lift_up;
|
delete g_lift_up;
|
||||||
|
delete g_monoid;
|
||||||
delete g_mul;
|
delete g_mul;
|
||||||
|
delete g_mul_one;
|
||||||
|
delete g_mul_zero_class;
|
||||||
|
delete g_mul_zero;
|
||||||
delete g_nat;
|
delete g_nat;
|
||||||
delete g_nat_of_num;
|
delete g_nat_of_num;
|
||||||
delete g_nat_succ;
|
delete g_nat_succ;
|
||||||
|
|
@ -463,11 +617,59 @@ void finalize_constants() {
|
||||||
delete g_not;
|
delete g_not;
|
||||||
delete g_not_of_iff_false;
|
delete g_not_of_iff_false;
|
||||||
delete g_not_of_not_not_not;
|
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;
|
||||||
delete g_num_zero;
|
delete g_num_zero;
|
||||||
delete g_num_pos;
|
delete g_num_pos;
|
||||||
delete g_of_iff_true;
|
delete g_of_iff_true;
|
||||||
delete g_one;
|
delete g_one;
|
||||||
|
delete g_one_mul;
|
||||||
delete g_option;
|
delete g_option;
|
||||||
delete g_option_some;
|
delete g_option_some;
|
||||||
delete g_option_none;
|
delete g_option_none;
|
||||||
|
|
@ -493,12 +695,16 @@ void finalize_constants() {
|
||||||
delete g_propext;
|
delete g_propext;
|
||||||
delete g_rat_divide;
|
delete g_rat_divide;
|
||||||
delete g_rat_of_num;
|
delete g_rat_of_num;
|
||||||
|
delete g_ring;
|
||||||
|
delete g_right_distrib;
|
||||||
|
delete g_semiring;
|
||||||
delete g_sigma;
|
delete g_sigma;
|
||||||
delete g_sigma_mk;
|
delete g_sigma_mk;
|
||||||
delete g_sorry;
|
delete g_sorry;
|
||||||
delete g_string;
|
delete g_string;
|
||||||
delete g_string_empty;
|
delete g_string_empty;
|
||||||
delete g_string_str;
|
delete g_string_str;
|
||||||
|
delete g_sub;
|
||||||
delete g_subsingleton;
|
delete g_subsingleton;
|
||||||
delete g_subsingleton_elim;
|
delete g_subsingleton_elim;
|
||||||
delete g_tactic;
|
delete g_tactic;
|
||||||
|
|
@ -565,14 +771,19 @@ void finalize_constants() {
|
||||||
delete g_true_intro;
|
delete g_true_intro;
|
||||||
delete g_is_trunc_is_hset;
|
delete g_is_trunc_is_hset;
|
||||||
delete g_is_trunc_is_hprop;
|
delete g_is_trunc_is_hprop;
|
||||||
|
delete g_weak_order;
|
||||||
delete g_well_founded;
|
delete g_well_founded;
|
||||||
delete g_zero;
|
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_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_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_name() { return *g_and; }
|
||||||
name const & get_and_elim_left_name() { return *g_and_elim_left; }
|
name const & get_and_elim_left_name() { return *g_and_elim_left; }
|
||||||
name const & get_and_elim_right_name() { return *g_and_elim_right; }
|
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_congr_fun_name() { return *g_congr_fun; }
|
||||||
name const & get_decidable_name() { return *g_decidable; }
|
name const & get_decidable_name() { return *g_decidable; }
|
||||||
name const & get_decidable_by_contradiction_name() { return *g_decidable_by_contradiction; }
|
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_dite_name() { return *g_dite; }
|
||||||
name const & get_div_name() { return *g_div; }
|
name const & get_div_name() { return *g_div; }
|
||||||
name const & get_empty_name() { return *g_empty; }
|
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_name() { return *g_false; }
|
||||||
name const & get_false_rec_name() { return *g_false_rec; }
|
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_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_funext_name() { return *g_funext; }
|
||||||
name const & get_has_zero_name() { return *g_has_zero; }
|
name const & get_has_zero_name() { return *g_has_zero; }
|
||||||
name const & get_has_one_name() { return *g_has_one; }
|
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_zero_zero_name() { return *g_has_zero_zero; }
|
||||||
name const & get_has_one_one_name() { return *g_has_one_one; }
|
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_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_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_name() { return *g_heq; }
|
||||||
name const & get_heq_refl_name() { return *g_heq_refl; }
|
name const & get_heq_refl_name() { return *g_heq_refl; }
|
||||||
name const & get_heq_to_eq_name() { return *g_heq_to_eq; }
|
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_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_is_trunc_is_hprop_elim_name() { return *g_is_trunc_is_hprop_elim; }
|
||||||
name const & get_ite_name() { return *g_ite; }
|
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_name() { return *g_lift; }
|
||||||
name const & get_lift_down_name() { return *g_lift_down; }
|
name const & get_lift_down_name() { return *g_lift_down; }
|
||||||
name const & get_lift_up_name() { return *g_lift_up; }
|
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_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_name() { return *g_nat; }
|
||||||
name const & get_nat_of_num_name() { return *g_nat_of_num; }
|
name const & get_nat_of_num_name() { return *g_nat_of_num; }
|
||||||
name const & get_nat_succ_name() { return *g_nat_succ; }
|
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_name() { return *g_not; }
|
||||||
name const & get_not_of_iff_false_name() { return *g_not_of_iff_false; }
|
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_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_name() { return *g_num; }
|
||||||
name const & get_num_zero_name() { return *g_num_zero; }
|
name const & get_num_zero_name() { return *g_num_zero; }
|
||||||
name const & get_num_pos_name() { return *g_num_pos; }
|
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_of_iff_true_name() { return *g_of_iff_true; }
|
||||||
name const & get_one_name() { return *g_one; }
|
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_name() { return *g_option; }
|
||||||
name const & get_option_some_name() { return *g_option_some; }
|
name const & get_option_some_name() { return *g_option_some; }
|
||||||
name const & get_option_none_name() { return *g_option_none; }
|
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_propext_name() { return *g_propext; }
|
||||||
name const & get_rat_divide_name() { return *g_rat_divide; }
|
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_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_name() { return *g_sigma; }
|
||||||
name const & get_sigma_mk_name() { return *g_sigma_mk; }
|
name const & get_sigma_mk_name() { return *g_sigma_mk; }
|
||||||
name const & get_sorry_name() { return *g_sorry; }
|
name const & get_sorry_name() { return *g_sorry; }
|
||||||
name const & get_string_name() { return *g_string; }
|
name const & get_string_name() { return *g_string; }
|
||||||
name const & get_string_empty_name() { return *g_string_empty; }
|
name const & get_string_empty_name() { return *g_string_empty; }
|
||||||
name const & get_string_str_name() { return *g_string_str; }
|
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_name() { return *g_subsingleton; }
|
||||||
name const & get_subsingleton_elim_name() { return *g_subsingleton_elim; }
|
name const & get_subsingleton_elim_name() { return *g_subsingleton_elim; }
|
||||||
name const & get_tactic_name() { return *g_tactic; }
|
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_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_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_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_well_founded_name() { return *g_well_founded; }
|
||||||
name const & get_zero_name() { return *g_zero; }
|
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; }
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -6,10 +6,11 @@ namespace lean {
|
||||||
void initialize_constants();
|
void initialize_constants();
|
||||||
void finalize_constants();
|
void finalize_constants();
|
||||||
name const & get_absurd_name();
|
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_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_name();
|
||||||
name const & get_and_elim_left_name();
|
name const & get_and_elim_left_name();
|
||||||
name const & get_and_elim_right_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_congr_fun_name();
|
||||||
name const & get_decidable_name();
|
name const & get_decidable_name();
|
||||||
name const & get_decidable_by_contradiction_name();
|
name const & get_decidable_by_contradiction_name();
|
||||||
|
name const & get_distrib_name();
|
||||||
name const & get_dite_name();
|
name const & get_dite_name();
|
||||||
name const & get_div_name();
|
name const & get_div_name();
|
||||||
name const & get_empty_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_name();
|
||||||
name const & get_false_rec_name();
|
name const & get_false_rec_name();
|
||||||
name const & get_false_of_true_iff_false_name();
|
name const & get_false_of_true_iff_false_name();
|
||||||
|
name const & get_field_name();
|
||||||
name const & get_funext_name();
|
name const & get_funext_name();
|
||||||
name const & get_has_zero_name();
|
name const & get_has_zero_name();
|
||||||
name const & get_has_one_name();
|
name const & get_has_one_name();
|
||||||
name const & get_has_zero_zero_name();
|
name const & get_has_zero_zero_name();
|
||||||
name const & get_has_one_one_name();
|
name const & get_has_one_one_name();
|
||||||
name const & get_has_add_name();
|
name const & get_has_add_name();
|
||||||
|
name const & get_has_div_name();
|
||||||
name const & get_has_mul_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_name();
|
||||||
name const & get_heq_refl_name();
|
name const & get_heq_refl_name();
|
||||||
name const & get_heq_to_eq_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_implies_of_if_neg_name();
|
||||||
name const & get_is_trunc_is_hprop_elim_name();
|
name const & get_is_trunc_is_hprop_elim_name();
|
||||||
name const & get_ite_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_name();
|
||||||
name const & get_lift_down_name();
|
name const & get_lift_down_name();
|
||||||
name const & get_lift_up_name();
|
name const & get_lift_up_name();
|
||||||
|
name const & get_monoid_name();
|
||||||
name const & get_mul_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_name();
|
||||||
name const & get_nat_of_num_name();
|
name const & get_nat_of_num_name();
|
||||||
name const & get_nat_succ_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_name();
|
||||||
name const & get_not_of_iff_false_name();
|
name const & get_not_of_iff_false_name();
|
||||||
name const & get_not_of_not_not_not_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_name();
|
||||||
name const & get_num_zero_name();
|
name const & get_num_zero_name();
|
||||||
name const & get_num_pos_name();
|
name const & get_num_pos_name();
|
||||||
name const & get_of_iff_true_name();
|
name const & get_of_iff_true_name();
|
||||||
name const & get_one_name();
|
name const & get_one_name();
|
||||||
|
name const & get_one_mul_name();
|
||||||
name const & get_option_name();
|
name const & get_option_name();
|
||||||
name const & get_option_some_name();
|
name const & get_option_some_name();
|
||||||
name const & get_option_none_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_propext_name();
|
||||||
name const & get_rat_divide_name();
|
name const & get_rat_divide_name();
|
||||||
name const & get_rat_of_num_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_name();
|
||||||
name const & get_sigma_mk_name();
|
name const & get_sigma_mk_name();
|
||||||
name const & get_sorry_name();
|
name const & get_sorry_name();
|
||||||
name const & get_string_name();
|
name const & get_string_name();
|
||||||
name const & get_string_empty_name();
|
name const & get_string_empty_name();
|
||||||
name const & get_string_str_name();
|
name const & get_string_str_name();
|
||||||
|
name const & get_sub_name();
|
||||||
name const & get_subsingleton_name();
|
name const & get_subsingleton_name();
|
||||||
name const & get_subsingleton_elim_name();
|
name const & get_subsingleton_elim_name();
|
||||||
name const & get_tactic_name();
|
name const & get_tactic_name();
|
||||||
|
|
@ -190,6 +256,10 @@ name const & get_true_name();
|
||||||
name const & get_true_intro_name();
|
name const & get_true_intro_name();
|
||||||
name const & get_is_trunc_is_hset_name();
|
name const & get_is_trunc_is_hset_name();
|
||||||
name const & get_is_trunc_is_hprop_name();
|
name const & get_is_trunc_is_hprop_name();
|
||||||
|
name const & get_weak_order_name();
|
||||||
name const & get_well_founded_name();
|
name const & get_well_founded_name();
|
||||||
name const & get_zero_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();
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -1,8 +1,9 @@
|
||||||
absurd
|
absurd
|
||||||
distrib
|
|
||||||
left_distrib
|
|
||||||
right_distrib
|
|
||||||
add
|
add
|
||||||
|
add_comm_group
|
||||||
|
add_comm_semigroup
|
||||||
|
add_monoid
|
||||||
|
add_group
|
||||||
and
|
and
|
||||||
and.elim_left
|
and.elim_left
|
||||||
and.elim_right
|
and.elim_right
|
||||||
|
|
@ -20,6 +21,7 @@ congr_arg
|
||||||
congr_fun
|
congr_fun
|
||||||
decidable
|
decidable
|
||||||
decidable.by_contradiction
|
decidable.by_contradiction
|
||||||
|
distrib
|
||||||
dite
|
dite
|
||||||
div
|
div
|
||||||
empty
|
empty
|
||||||
|
|
@ -41,13 +43,17 @@ exists.elim
|
||||||
false
|
false
|
||||||
false.rec
|
false.rec
|
||||||
false_of_true_iff_false
|
false_of_true_iff_false
|
||||||
|
field
|
||||||
funext
|
funext
|
||||||
has_zero
|
has_zero
|
||||||
has_one
|
has_one
|
||||||
has_zero.zero
|
has_zero.zero
|
||||||
has_one.one
|
has_one.one
|
||||||
has_add
|
has_add
|
||||||
|
has_div
|
||||||
has_mul
|
has_mul
|
||||||
|
has_neg
|
||||||
|
has_sub
|
||||||
heq
|
heq
|
||||||
heq.refl
|
heq.refl
|
||||||
heq.to_eq
|
heq.to_eq
|
||||||
|
|
@ -68,10 +74,18 @@ implies_of_if_pos
|
||||||
implies_of_if_neg
|
implies_of_if_neg
|
||||||
is_trunc.is_hprop.elim
|
is_trunc.is_hprop.elim
|
||||||
ite
|
ite
|
||||||
|
le.refl
|
||||||
|
left_distrib
|
||||||
|
linear_ordered_semiring
|
||||||
|
linear_ordered_ring
|
||||||
lift
|
lift
|
||||||
lift.down
|
lift.down
|
||||||
lift.up
|
lift.up
|
||||||
|
monoid
|
||||||
mul
|
mul
|
||||||
|
mul_one
|
||||||
|
mul_zero_class
|
||||||
|
mul_zero
|
||||||
nat
|
nat
|
||||||
nat.of_num
|
nat.of_num
|
||||||
nat.succ
|
nat.succ
|
||||||
|
|
@ -81,11 +95,59 @@ neg
|
||||||
not
|
not
|
||||||
not_of_iff_false
|
not_of_iff_false
|
||||||
not_of_not_not_not
|
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
|
||||||
num.zero
|
num.zero
|
||||||
num.pos
|
num.pos
|
||||||
of_iff_true
|
of_iff_true
|
||||||
one
|
one
|
||||||
|
one_mul
|
||||||
option
|
option
|
||||||
option.some
|
option.some
|
||||||
option.none
|
option.none
|
||||||
|
|
@ -111,12 +173,16 @@ prod.pr2
|
||||||
propext
|
propext
|
||||||
rat.divide
|
rat.divide
|
||||||
rat.of_num
|
rat.of_num
|
||||||
|
ring
|
||||||
|
right_distrib
|
||||||
|
semiring
|
||||||
sigma
|
sigma
|
||||||
sigma.mk
|
sigma.mk
|
||||||
sorry
|
sorry
|
||||||
string
|
string
|
||||||
string.empty
|
string.empty
|
||||||
string.str
|
string.str
|
||||||
|
sub
|
||||||
subsingleton
|
subsingleton
|
||||||
subsingleton.elim
|
subsingleton.elim
|
||||||
tactic
|
tactic
|
||||||
|
|
@ -183,5 +249,9 @@ true
|
||||||
true.intro
|
true.intro
|
||||||
is_trunc.is_hset
|
is_trunc.is_hset
|
||||||
is_trunc.is_hprop
|
is_trunc.is_hprop
|
||||||
|
weak_order
|
||||||
well_founded
|
well_founded
|
||||||
zero
|
zero
|
||||||
|
zero_mul
|
||||||
|
zero_le_one
|
||||||
|
zero_lt_one
|
||||||
|
|
|
||||||
|
|
@ -44,7 +44,6 @@ Author: Leonardo de Moura
|
||||||
#include "library/aux_recursors.h"
|
#include "library/aux_recursors.h"
|
||||||
#include "library/decl_stats.h"
|
#include "library/decl_stats.h"
|
||||||
#include "library/meng_paulson.h"
|
#include "library/meng_paulson.h"
|
||||||
#include "library/norm_num.h"
|
|
||||||
#include "library/class_instance_resolution.h"
|
#include "library/class_instance_resolution.h"
|
||||||
#include "library/type_context.h"
|
#include "library/type_context.h"
|
||||||
#include "library/congr_lemma_manager.h"
|
#include "library/congr_lemma_manager.h"
|
||||||
|
|
@ -91,7 +90,6 @@ void initialize_library_module() {
|
||||||
initialize_aux_recursors();
|
initialize_aux_recursors();
|
||||||
initialize_decl_stats();
|
initialize_decl_stats();
|
||||||
initialize_meng_paulson();
|
initialize_meng_paulson();
|
||||||
initialize_norm_num();
|
|
||||||
initialize_class_instance_resolution();
|
initialize_class_instance_resolution();
|
||||||
initialize_type_context();
|
initialize_type_context();
|
||||||
initialize_light_rule_set();
|
initialize_light_rule_set();
|
||||||
|
|
@ -105,7 +103,6 @@ void finalize_library_module() {
|
||||||
finalize_light_rule_set();
|
finalize_light_rule_set();
|
||||||
finalize_type_context();
|
finalize_type_context();
|
||||||
finalize_class_instance_resolution();
|
finalize_class_instance_resolution();
|
||||||
finalize_norm_num();
|
|
||||||
finalize_meng_paulson();
|
finalize_meng_paulson();
|
||||||
finalize_decl_stats();
|
finalize_decl_stats();
|
||||||
finalize_aux_recursors();
|
finalize_aux_recursors();
|
||||||
|
|
|
||||||
|
|
@ -3,90 +3,10 @@ Copyright (c) 2015 Microsoft Corporation. All rights reserved.
|
||||||
Released under Apache 2.0 license as described in the file LICENSE.
|
Released under Apache 2.0 license as described in the file LICENSE.
|
||||||
Author: Robert Y. Lewis
|
Author: Robert Y. Lewis
|
||||||
*/
|
*/
|
||||||
|
|
||||||
#include "library/norm_num.h"
|
#include "library/norm_num.h"
|
||||||
#include "library/constants.h"
|
#include "library/constants.h"
|
||||||
|
|
||||||
namespace lean {
|
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) {
|
static bool is_numeral_aux(expr const & e, bool is_first) {
|
||||||
buffer<expr> args;
|
buffer<expr> args;
|
||||||
expr const & f = get_app_args(e, 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 {
|
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 {
|
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) {
|
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()) {
|
if (instances.find(l_name) != instances.end()) {
|
||||||
return instances[l_name];
|
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) {
|
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()) {
|
if (instances.find(l_name) != instances.end()) {
|
||||||
return instances[l_name];
|
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) {
|
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()) {
|
if (instances.find(l_name) != instances.end()) {
|
||||||
return instances[l_name];
|
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 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<expr> inst = m_type_ctx.mk_class_instance(t);
|
optional<expr> inst = m_type_ctx.mk_class_instance(t);
|
||||||
if (inst) {
|
if (inst) {
|
||||||
return *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) {
|
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()) {
|
if (instances.find(l_name) != instances.end()) {
|
||||||
return instances[l_name];
|
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) {
|
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()) {
|
if (instances.find(l_name) != instances.end()) {
|
||||||
return instances[l_name];
|
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) {
|
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()) {
|
if (instances.find(l_name) != instances.end()) {
|
||||||
return instances[l_name];
|
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) {
|
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()) {
|
if (instances.find(l_name) != instances.end()) {
|
||||||
return instances[l_name];
|
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) {
|
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()) {
|
if (instances.find(l_name) != instances.end()) {
|
||||||
return instances[l_name];
|
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) {
|
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()) {
|
if (instances.find(l_name) != instances.end()) {
|
||||||
return instances[l_name];
|
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) {
|
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()) {
|
if (instances.find(l_name) != instances.end()) {
|
||||||
return instances[l_name];
|
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) {
|
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()) {
|
if (instances.find(l_name) != instances.end()) {
|
||||||
return instances[l_name];
|
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) {
|
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()) {
|
if (instances.find(l_name) != instances.end()) {
|
||||||
return instances[l_name];
|
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) {
|
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()) {
|
if (instances.find(l_name) != instances.end()) {
|
||||||
return instances[l_name];
|
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) {
|
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()) {
|
if (instances.find(l_name) != instances.end()) {
|
||||||
return instances[l_name];
|
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) {
|
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()) {
|
if (instances.find(l_name) != instances.end()) {
|
||||||
return instances[l_name];
|
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) {
|
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()) {
|
if (instances.find(l_name) != instances.end()) {
|
||||||
return instances[l_name];
|
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 norm_num_context::mk_cong(expr const & op, expr const & type, expr const & a,
|
||||||
expr const & b, expr const & eq) {
|
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 <t, p> such that p is a proof that lhs + rhs = t.
|
// returns <t, p> such that p is a proof that lhs + rhs = t.
|
||||||
|
|
@ -440,52 +360,52 @@ pair<expr, expr> norm_num_context::mk_norm_add(expr const & lhs, expr const & rh
|
||||||
if (is_bit0(lhs) && is_bit0(rhs)) { // typec is has_add
|
if (is_bit0(lhs) && is_bit0(rhs)) { // typec is has_add
|
||||||
auto p = mk_norm_add(args_lhs[2], args_rhs[2]);
|
auto p = mk_norm_add(args_lhs[2], args_rhs[2]);
|
||||||
rv = mk_app(lhs_head, type, typec, p.first);
|
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});
|
args_lhs[2], args_rhs[2], p.first, p.second});
|
||||||
} else if (is_bit0(lhs) && is_bit1(rhs)) {
|
} else if (is_bit0(lhs) && is_bit1(rhs)) {
|
||||||
auto p = mk_norm_add(args_lhs[2], args_rhs[3]);
|
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});
|
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});
|
args_lhs[2], args_rhs[3], p.first, p.second});
|
||||||
} else if (is_bit0(lhs) && is_one(rhs)) {
|
} 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]});
|
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
|
} else if (is_bit1(lhs) && is_bit0(rhs)) { // typec is has_one
|
||||||
auto p = mk_norm_add(args_lhs[3], args_rhs[2]);
|
auto p = mk_norm_add(args_lhs[3], args_rhs[2]);
|
||||||
rv = mk_app(lhs_head, type, typec, args_lhs[2], p.first);
|
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});
|
args_lhs[3], args_rhs[2], p.first, p.second});
|
||||||
} else if (is_bit1(lhs) && is_bit1(rhs)) { // typec is has_one
|
} else if (is_bit1(lhs) && is_bit1(rhs)) { // typec is has_one
|
||||||
auto add_ts = mk_norm_add(args_lhs[3], args_rhs[3]);
|
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);
|
auto p = mk_norm_add1(add1);
|
||||||
rv = mk_app({mk_const(get_bit0_name()), type, args_lhs[2], p.first});
|
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});
|
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
|
} 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);
|
auto p = mk_norm_add1(add1);
|
||||||
rv = p.first;
|
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});
|
args_lhs[3], p.first, p.second});
|
||||||
} else if (is_one(lhs) && is_bit0(rhs)) { // typec is has_one
|
} 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]});
|
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
|
} 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);
|
auto p = mk_norm_add1(add1);
|
||||||
rv = p.first;
|
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});
|
args_rhs[3], p.first, p.second});
|
||||||
} else if (is_one(lhs) && is_one(rhs)) {
|
} else if (is_one(lhs) && is_one(rhs)) {
|
||||||
rv = mk_app({mk_const(get_bit0_name()), type, mk_has_add(type), lhs});
|
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)) {
|
} else if (is_zero(lhs)) {
|
||||||
rv = rhs;
|
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)) {
|
} else if (is_zero(rhs)) {
|
||||||
rv = lhs;
|
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 {
|
} else {
|
||||||
throw exception("mk_norm_add got malformed args");
|
throw exception("mk_norm_add got malformed args");
|
||||||
}
|
}
|
||||||
|
|
@ -504,19 +424,19 @@ pair<expr, expr> norm_num_context::mk_norm_add1(expr const & e) {
|
||||||
if (is_bit0(p)) {
|
if (is_bit0(p)) {
|
||||||
auto has_one = args[2];
|
auto has_one = args[2];
|
||||||
rv = mk_app({mk_const(get_bit1_name()), args[0], args[2], args[1], ne_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
|
} 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});
|
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});
|
args[2], ne_args[3], np.first, np.second});
|
||||||
} else if (is_zero(p)) {
|
} else if (is_zero(p)) {
|
||||||
rv = mk_app({mk_const(get_one_name()), args[0], args[2]});
|
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)) {
|
} else if (is_one(p)) {
|
||||||
rv = mk_app({mk_const(get_bit0_name()), args[0], args[1],
|
rv = mk_app({mk_const(get_bit0_name()), args[0], args[1],
|
||||||
mk_app({mk_const(get_one_name()), args[0], args[2]})});
|
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 {
|
} else {
|
||||||
throw exception("malformed add1");
|
throw exception("malformed add1");
|
||||||
}
|
}
|
||||||
|
|
@ -537,24 +457,24 @@ pair<expr, expr> norm_num_context::mk_norm_mul(expr const & lhs, expr const & rh
|
||||||
expr prf;
|
expr prf;
|
||||||
if (is_zero(rhs)) {
|
if (is_zero(rhs)) {
|
||||||
rv = 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)) {
|
} else if (is_zero(lhs)) {
|
||||||
rv = 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)) {
|
} else if (is_one(rhs)) {
|
||||||
rv = lhs;
|
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)) {
|
} else if (is_bit0(rhs)) {
|
||||||
auto mtp = mk_norm_mul(lhs, args_rhs[2]);
|
auto mtp = mk_norm_mul(lhs, args_rhs[2]);
|
||||||
rv = mk_app({rhs_head, type, typec, mtp.first});
|
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});
|
args_rhs[2], mtp.first, mtp.second});
|
||||||
} else if (is_bit1(rhs)) {
|
} else if (is_bit1(rhs)) {
|
||||||
auto mtp = mk_norm_mul(lhs, args_rhs[3]);
|
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}),
|
auto atp = mk_norm_add(mk_app({mk_const(get_bit0_name()), type, args_rhs[2], mtp.first}),
|
||||||
lhs);
|
lhs);
|
||||||
rv = atp.first;
|
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});
|
mtp.first, atp.first, mtp.second, atp.second});
|
||||||
} else {
|
} else {
|
||||||
throw exception("mk_norm_mul got malformed args");
|
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);
|
expr f = get_app_args(e, args);
|
||||||
if (!is_constant(f)) {
|
if (!is_constant(f)) {
|
||||||
throw exception("cannot find num of nonconstant");
|
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]);
|
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]);
|
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]);
|
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]);
|
mpq num = mpq_of_expr(args[2]), den = mpq_of_expr(args[3]);
|
||||||
if (den != 0)
|
if (den != 0)
|
||||||
return mpq_of_expr(args[2]) / mpq_of_expr(args[3]);
|
return mpq_of_expr(args[2]) / mpq_of_expr(args[3]);
|
||||||
else
|
else
|
||||||
throw exception("divide by 0");
|
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]));
|
return neg(mpq_of_expr(args[2]));
|
||||||
} else {
|
} else {
|
||||||
auto v = to_mpq(e);
|
auto v = to_mpq(e);
|
||||||
|
|
@ -610,13 +530,13 @@ mpz norm_num_context::num_of_expr(expr const & e) {
|
||||||
if (v) {
|
if (v) {
|
||||||
return *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]);
|
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]);
|
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]);
|
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]));
|
return neg(num_of_expr(args[2]));
|
||||||
} else {
|
} else {
|
||||||
throw exception("expression in num_of_expr is malfomed");
|
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);
|
auto rhs_v = get_type_and_arg_of_neg(rhs);
|
||||||
expr type = rhs_v.first;
|
expr type = rhs_v.first;
|
||||||
auto sum_pr = mk_norm(mk_add(type, s_lhs_v, s_rhs_v)).second;
|
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});
|
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)) {
|
if (is_neg_app(rhs)) {
|
||||||
auto rhs_v = get_type_and_arg_of_neg(rhs).second;
|
auto rhs_v = get_type_and_arg_of_neg(rhs).second;
|
||||||
auto sum_pr = mk_norm(mk_add(type, s_rhs, rhs_v)).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});
|
s_lhs_v.second, s_rhs, rhs_v, sum_pr});
|
||||||
} else {
|
} else {
|
||||||
auto sum_pr = mk_norm(mk_add(type, s_lhs_v.second, rhs)).second;
|
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});
|
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));
|
lean_assert(!is_neg_app(s_lhs));
|
||||||
expr prf = mk_norm_eq_neg_add_pos(s_rhs, s_lhs, rhs);
|
expr prf = mk_norm_eq_neg_add_pos(s_rhs, s_lhs, rhs);
|
||||||
expr type = get_type_and_arg_of_neg(s_rhs).first;
|
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});
|
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) {
|
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_lhs));
|
||||||
lean_assert(is_neg_app(s_rhs));
|
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;
|
auto s_lhs_v = get_type_and_arg_of_neg(s_lhs).second;
|
||||||
expr s_rhs_v, type;
|
expr s_rhs_v, type;
|
||||||
std::tie(type, s_rhs_v) = get_type_and_arg_of_neg(s_rhs);
|
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));
|
auto prod_pr = mk_norm(mk_mul(type, s_lhs_v, s_rhs_v));
|
||||||
lean_assert(to_num(rhs) == to_num(prod_pr.first));
|
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});
|
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);
|
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 rhs_v = get_type_and_arg_of_neg(rhs).second;
|
||||||
auto prod_pr = mk_norm(mk_mul(type, s_lhs_v, s_rhs));
|
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});
|
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);
|
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 rhs_v = get_type_and_arg_of_neg(rhs).second;
|
||||||
auto prod_pr = mk_norm(mk_mul(type, s_lhs, s_rhs_v));
|
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});
|
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) {
|
expr norm_num_context::mk_div(expr const & type, expr const & e1, expr const & e2) {
|
||||||
auto has_div = mk_has_div(type);
|
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) {
|
expr norm_num_context::mk_neg(expr const & type, expr const & e) {
|
||||||
auto has_neg = mk_has_neg(type);
|
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) {
|
expr norm_num_context::mk_add(expr const & type, expr const & e1, expr const & e2) {
|
||||||
auto has_add = mk_has_add(type);
|
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) {
|
expr norm_num_context::mk_mul(expr const & type, expr const & e1, expr const & e2) {
|
||||||
auto has_mul = mk_has_mul(type);
|
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
|
// 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));
|
auto npr_r = mk_norm(mk_mul(type, rhs, den));
|
||||||
lean_assert(to_mpq(npr_l.first) == to_mpq(npr_r.first));
|
lean_assert(to_mpq(npr_l.first) == to_mpq(npr_r.first));
|
||||||
expr den_neq_zero = mk_nonzero_prf(den);
|
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});
|
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));
|
auto npr_r = mk_norm(mk_mul(type, den, rhs));
|
||||||
lean_assert(to_mpq(npr_l.first) == to_mpq(npr_r.first));
|
lean_assert(to_mpq(npr_l.first) == to_mpq(npr_r.first));
|
||||||
expr den_neq_zero = mk_nonzero_prf(den);
|
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});
|
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) {
|
expr norm_num_context::mk_nonzero_prf(expr const & e) {
|
||||||
buffer<expr> args;
|
buffer<expr> args;
|
||||||
expr f = get_app_args(e, args);
|
expr f = get_app_args(e, args);
|
||||||
if (const_name(f) == *g_neg) {
|
if (const_name(f) == get_neg_name()) {
|
||||||
return mk_app({mk_const(*g_nonzero_neg), args[0], mk_lin_ord_ring(args[0]),
|
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])});
|
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]);
|
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});
|
args[3], num_pr, den_pr});
|
||||||
} else {
|
} 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)});
|
e, mk_pos_prf(e)});
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
@ -837,12 +757,12 @@ expr norm_num_context::mk_pos_prf(expr const & e) {
|
||||||
expr prf;
|
expr prf;
|
||||||
if (is_bit0(e)) {
|
if (is_bit0(e)) {
|
||||||
prf = mk_pos_prf(args[2]);
|
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)) {
|
} else if (is_bit1(e)) {
|
||||||
prf = mk_nonneg_prf(args[3]);
|
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)) {
|
} 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 {
|
} else {
|
||||||
throw exception("mk_pos_proof called on zero or non_numeral");
|
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;
|
expr prf;
|
||||||
if (is_bit0(e)) {
|
if (is_bit0(e)) {
|
||||||
prf = mk_nonneg_prf(args[2]);
|
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)) {
|
} else if (is_bit1(e)) {
|
||||||
prf = mk_nonneg_prf(args[3]);
|
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)) {
|
} 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)) {
|
} 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)})});
|
mk_app({mk_const(get_zero_name()), type, mk_has_zero(type)})});
|
||||||
} else {
|
} else {
|
||||||
throw exception("mk_nonneg_proof called on zero or non_numeral");
|
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]));
|
auto prf = mk_norm(mk_div(type, new_num, args[3]));
|
||||||
lean_assert(to_mpq(prf.first) == to_mpq(rhs));
|
lean_assert(to_mpq(prf.first) == to_mpq(rhs));
|
||||||
expr den_ne_zero = mk_nonzero_prf(args[3]);
|
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});
|
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]));
|
auto prf = mk_norm(mk_div(type, new_num, args[3]));
|
||||||
lean_assert(to_mpq(prf.first) == to_mpq(rhs));
|
lean_assert(to_mpq(prf.first) == to_mpq(rhs));
|
||||||
expr den_ne_zero = mk_nonzero_prf(args[3]);
|
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});
|
rhs, den_ne_zero, prf.second});
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
@ -903,7 +823,7 @@ pair<expr, expr> norm_num_context::mk_norm(expr const & e) {
|
||||||
m_lvls = const_levels(f);
|
m_lvls = const_levels(f);
|
||||||
expr type = args[0];
|
expr type = args[0];
|
||||||
if (is_numeral(e)) {
|
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<expr, expr>(e, prf);
|
return pair<expr, expr>(e, prf);
|
||||||
}
|
}
|
||||||
mpq val = mpq_of_expr(e);
|
mpq val = mpq_of_expr(e);
|
||||||
|
|
@ -913,7 +833,7 @@ pair<expr, expr> norm_num_context::mk_norm(expr const & e) {
|
||||||
} else {
|
} else {
|
||||||
nval = mk_neg(type, from_mpq(neg(val), type));
|
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;
|
expr prf;
|
||||||
auto lhs_p = mk_norm(args[2]);
|
auto lhs_p = mk_norm(args[2]);
|
||||||
auto rhs_p = mk_norm(args[3]);
|
auto rhs_p = mk_norm(args[3]);
|
||||||
|
|
@ -936,21 +856,21 @@ pair<expr, expr> 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});
|
lhs_p.first, rhs_p.first, nval, lhs_p.second, rhs_p.second, prf});
|
||||||
return pair<expr, expr>(nval, rprf);
|
return pair<expr, expr>(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]));
|
expr sum = mk_add(args[0], args[2], mk_neg(args[0], args[3]));
|
||||||
auto anprf = mk_norm(sum);
|
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});
|
args[3], anprf.first, anprf.second});
|
||||||
return pair<expr, expr>(nval, rprf);
|
return pair<expr, expr>(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]);
|
auto prf = mk_norm(args[2]);
|
||||||
lean_assert(mpq_of_expr(prf.first) == neg(val));
|
lean_assert(mpq_of_expr(prf.first) == neg(val));
|
||||||
if (is_zero(prf.first)) {
|
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});
|
prf.second});
|
||||||
return pair<expr, expr>(prf.first, rprf);
|
return pair<expr, expr>(prf.first, rprf);
|
||||||
}
|
}
|
||||||
|
|
@ -962,11 +882,11 @@ pair<expr, expr> norm_num_context::mk_norm(expr const & e) {
|
||||||
nval_args[2], prf.second);
|
nval_args[2], prf.second);
|
||||||
return pair<expr, expr>(nval, rprf);
|
return pair<expr, expr>(nval, rprf);
|
||||||
} else {
|
} 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});
|
args[2], nval, prf.second});
|
||||||
return pair<expr, expr>(nval, rprf);
|
return pair<expr, expr>(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 lhs_p = mk_norm(args[2]);
|
||||||
auto rhs_p = mk_norm(args[3]);
|
auto rhs_p = mk_norm(args[3]);
|
||||||
expr prf;
|
expr prf;
|
||||||
|
|
@ -989,10 +909,10 @@ pair<expr, expr> norm_num_context::mk_norm(expr const & e) {
|
||||||
prf = mk_norm_eq_pos_mul_pos(lhs_p.first, rhs_p.first, nval);
|
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});
|
lhs_p.first, rhs_p.first, nval, lhs_p.second, rhs_p.second, prf});
|
||||||
return pair<expr, expr>(nval, rprf);
|
return pair<expr, expr>(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 lhs_p = mk_norm(args[2]);
|
||||||
auto rhs_p = mk_norm(args[3]);
|
auto rhs_p = mk_norm(args[3]);
|
||||||
expr prf;
|
expr prf;
|
||||||
|
|
@ -1004,7 +924,7 @@ pair<expr, expr> norm_num_context::mk_norm(expr const & e) {
|
||||||
auto rhs_mul = mk_norm(mk_mul(type, nval_num, rhs_p.first));
|
auto rhs_mul = mk_norm(mk_mul(type, nval_num, rhs_p.first));
|
||||||
expr den_nonzero = mk_nonzero_prf(rhs_p.first);
|
expr den_nonzero = mk_nonzero_prf(rhs_p.first);
|
||||||
expr nval_den_nonzero = mk_nonzero_prf(nval_den);
|
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_p.first, rhs_p.first, nval_num, nval_den, lhs_mul.first,
|
||||||
lhs_mul.second, rhs_mul.second, den_nonzero, nval_den_nonzero});
|
lhs_mul.second, rhs_mul.second, den_nonzero, nval_den_nonzero});
|
||||||
} else {
|
} else {
|
||||||
|
|
@ -1014,10 +934,10 @@ pair<expr, expr> norm_num_context::mk_norm(expr const & e) {
|
||||||
lean_assert(*val1 == *val2);
|
lean_assert(*val1 == *val2);
|
||||||
}
|
}
|
||||||
expr den_nonzero = mk_nonzero_prf(rhs_p.first);
|
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});
|
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.first, rhs_p.first, args[2], args[3], nval, prf,
|
||||||
lhs_p.second, rhs_p.second});
|
lhs_p.second, rhs_p.second});
|
||||||
return pair<expr, expr>(nval, rprf);
|
return pair<expr, expr>(nval, rprf);
|
||||||
|
|
@ -1038,171 +958,9 @@ pair<expr, expr> norm_num_context::mk_norm(expr const & e) {
|
||||||
return pair<expr, expr>(nval, rprf);
|
return pair<expr, expr>(nval, rprf);
|
||||||
} else if ((const_name(f) == get_zero_name() || const_name(f) == get_one_name())
|
} else if ((const_name(f) == get_zero_name() || const_name(f) == get_one_name())
|
||||||
&& args.size() == 2) {
|
&& args.size() == 2) {
|
||||||
return pair<expr, expr>(e, mk_app({mk_const(*g_mk_eq), args[0], e}));
|
return pair<expr, expr>(e, mk_app({mk_const(get_eq_refl_name()), args[0], e}));
|
||||||
} else {
|
} else {
|
||||||
throw exception("mk_norm found unrecognized combo ");
|
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;
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -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) {
|
inline mpq mpq_of_expr(type_context & type_ctx, expr const & e) {
|
||||||
return norm_num_context(type_ctx).mpq_of_expr(e);
|
return norm_num_context(type_ctx).mpq_of_expr(e);
|
||||||
}
|
}
|
||||||
|
|
||||||
void initialize_norm_num();
|
|
||||||
void finalize_norm_num();
|
|
||||||
}
|
}
|
||||||
|
|
|
||||||
|
|
@ -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
|
init_module.cpp change_tactic.cpp check_expr_tactic.cpp let_tactic.cpp
|
||||||
contradiction_tactic.cpp exfalso_tactic.cpp constructor_tactic.cpp
|
contradiction_tactic.cpp exfalso_tactic.cpp constructor_tactic.cpp
|
||||||
injection_tactic.cpp congruence_tactic.cpp relation_tactics.cpp
|
injection_tactic.cpp congruence_tactic.cpp relation_tactics.cpp
|
||||||
induction_tactic.cpp subst_tactic.cpp unfold_rec.cpp with_options_tactic.cpp)
|
induction_tactic.cpp subst_tactic.cpp unfold_rec.cpp with_options_tactic.cpp
|
||||||
|
norm_num_tactic.cpp)
|
||||||
|
|
@ -32,6 +32,7 @@ Author: Leonardo de Moura
|
||||||
#include "library/tactic/subst_tactic.h"
|
#include "library/tactic/subst_tactic.h"
|
||||||
#include "library/tactic/location.h"
|
#include "library/tactic/location.h"
|
||||||
#include "library/tactic/with_options_tactic.h"
|
#include "library/tactic/with_options_tactic.h"
|
||||||
|
#include "library/tactic/norm_num_tactic.h"
|
||||||
|
|
||||||
namespace lean {
|
namespace lean {
|
||||||
void initialize_tactic_module() {
|
void initialize_tactic_module() {
|
||||||
|
|
@ -62,9 +63,11 @@ void initialize_tactic_module() {
|
||||||
initialize_subst_tactic();
|
initialize_subst_tactic();
|
||||||
initialize_location();
|
initialize_location();
|
||||||
initialize_with_options_tactic();
|
initialize_with_options_tactic();
|
||||||
|
initialize_norm_num_tactic();
|
||||||
}
|
}
|
||||||
|
|
||||||
void finalize_tactic_module() {
|
void finalize_tactic_module() {
|
||||||
|
finalize_norm_num_tactic();
|
||||||
finalize_with_options_tactic();
|
finalize_with_options_tactic();
|
||||||
finalize_location();
|
finalize_location();
|
||||||
finalize_subst_tactic();
|
finalize_subst_tactic();
|
||||||
|
|
|
||||||
|
|
@ -8,11 +8,12 @@ Author: Robert Y. Lewis
|
||||||
#include "library/reducible.h"
|
#include "library/reducible.h"
|
||||||
#include "library/normalize.h"
|
#include "library/normalize.h"
|
||||||
#include "library/norm_num.h"
|
#include "library/norm_num.h"
|
||||||
|
#include "library/tmp_type_context.h"
|
||||||
#include "library/tactic/expr_to_tactic.h"
|
#include "library/tactic/expr_to_tactic.h"
|
||||||
|
|
||||||
namespace lean {
|
namespace lean {
|
||||||
tactic norm_num_tactic() {
|
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();
|
goals const & gs = s.get_goals();
|
||||||
if (empty(gs)) {
|
if (empty(gs)) {
|
||||||
throw_no_goal_if_enabled(s);
|
throw_no_goal_if_enabled(s);
|
||||||
|
|
@ -30,15 +31,16 @@ tactic norm_num_tactic() {
|
||||||
rhs = normalize(*rtc, rhs);
|
rhs = normalize(*rtc, rhs);
|
||||||
buffer<expr> hyps;
|
buffer<expr> hyps;
|
||||||
g.get_hyps(hyps);
|
g.get_hyps(hyps);
|
||||||
local_context ctx(to_list(hyps));
|
|
||||||
try {
|
try {
|
||||||
pair<expr, expr> p = mk_norm_num(env, ctx, lhs);
|
tmp_type_context ctx(env, ios.get_options());
|
||||||
|
ctx.set_local_instances(to_list(hyps));
|
||||||
|
pair<expr, expr> p = mk_norm_num(ctx, lhs);
|
||||||
expr new_lhs = p.first;
|
expr new_lhs = p.first;
|
||||||
expr new_lhs_pr = p.second;
|
expr new_lhs_pr = p.second;
|
||||||
pair<expr, expr> p2 = mk_norm_num(env, ctx, rhs);
|
pair<expr, expr> p2 = mk_norm_num(ctx, rhs);
|
||||||
expr new_rhs = p2.first;
|
expr new_rhs = p2.first;
|
||||||
expr new_rhs_pr = p2.second;
|
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) {
|
if (v_lhs == v_rhs) {
|
||||||
type_checker tc(env);
|
type_checker tc(env);
|
||||||
expr g_prf = mk_trans(tc, new_lhs_pr, mk_symm(tc, new_rhs_pr));
|
expr g_prf = mk_trans(tc, new_lhs_pr, mk_symm(tc, new_rhs_pr));
|
||||||
|
|
|
||||||
|
|
@ -1,5 +1,5 @@
|
||||||
import data.real
|
import data.real
|
||||||
open algebra real
|
open real
|
||||||
|
|
||||||
/-
|
/-
|
||||||
variable {A : Type}
|
variable {A : Type}
|
||||||
Loading…
Reference in a new issue