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

feat(norm_num): performance and style fixes

Browse source
This commit is contained in:
Rob Lewis 2015-11-10 13:40:34 -05:00 committed by Leonardo de Moura
parent 4bf0519843
commit 44a099f6f1
5 changed files with 463 additions and 273 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

97
library/algebra/numeral.lean
View file

@ -7,6 +7,8 @@ Author: Robert Y. Lewis
import algebra.ordered_field
open algebra
namespace norm_num
variable {A : Type}
definition add1 [s : has_add A] [s' : has_one A] (a : A) : A := add a one
@ -30,22 +32,25 @@ theorem bit1_add_bit0 [s : add_comm_semigroup A] [s' : has_one A] (a b : A) :
rewrite [↑bit0, ↑bit1, add_comm_middle], congruence, apply add_comm_four
end
theorem bit1_add_bit0_helper [s : add_comm_semigroup A] [s' : has_one A] (a b t : A) (H : a + b = t) :
bit1 a + bit0 b = bit1 t :=
theorem bit1_add_bit0_helper [s : add_comm_semigroup A] [s' : has_one A] (a b t : A)
(H : a + b = t) : bit1 a + bit0 b = bit1 t :=
by rewrite -H; apply bit1_add_bit0
theorem bit0_add_bit1 [s : add_comm_semigroup A] [s' : has_one A] (a b : A) :
bit0 a + bit1 b = bit1 (a + b) :=
by rewrite [{bit0 a + _}add.comm, {a + _}add.comm]; apply bit1_add_bit0
theorem bit0_add_bit1_helper [s : add_comm_semigroup A] [s' : has_one A] (a b t : A) (H : a + b = t) :
bit0 a + bit1 b = bit1 t :=
theorem bit0_add_bit1_helper [s : add_comm_semigroup A] [s' : has_one A] (a b t : A)
(H : a + b = t) : bit0 a + bit1 b = bit1 t :=
by rewrite -H; apply bit0_add_bit1
theorem bit1_add_bit1 [s : add_comm_semigroup A] [s' : has_one A] (a b : A) : bit1 a + bit1 b = bit0 (add1 (a + b)) :=
theorem bit1_add_bit1 [s : add_comm_semigroup A] [s' : has_one A] (a b : A) :
bit1 a + bit1 b = bit0 (add1 (a + b)) :=
begin
rewrite ↑[bit0, bit1, add1],
apply sorry
rewrite ↑[bit0, bit1, add1, add.assoc],
rewrite [*add.assoc, {_ + (b + 1)}add.comm, {_ + (b + 1 + _)}add.comm,
{_ + (b + 1 + _ + _)}add.comm, *add.assoc, {1 + a}add.comm, -{b + (a + 1)}add.assoc,
{b + a}add.comm, *add.assoc]
end
theorem bit1_add_bit1_helper [s : add_comm_semigroup A] [s' : has_one A] (a b t s: A)
@ -59,9 +64,11 @@ theorem bin_zero_add [s : add_monoid A] (a : A) : zero + a = a := !zero_add
theorem one_add_bit0 [s : add_comm_semigroup A] [s' : has_one A] (a : A) : one + bit0 a = bit1 a :=
begin rewrite ↑[bit0, bit1], rewrite add.comm end
theorem bit0_add_one [s : has_add A] [s' : has_one A] (a : A) : bit0 a + one = bit1 a := rfl
theorem bit0_add_one [s : has_add A] [s' : has_one A] (a : A) : bit0 a + one = bit1 a :=
rfl
theorem bit1_add_one [s : has_add A] [s' : has_one A] (a : A) : bit1 a + one = add1 (bit1 a) := rfl
theorem bit1_add_one [s : has_add A] [s' : has_one A] (a : A) : bit1 a + one = add1 (bit1 a) :=
rfl
theorem bit1_add_one_helper [s : has_add A] [s' : has_one A] (a t : A) (H : add1 (bit1 a) = t) :
bit1 a + one = t :=
@ -99,8 +106,8 @@ theorem add1_zero [s : add_monoid A] [s' : has_one A] : add1 (zero : A) = one :=
theorem one_add_one [s : has_add A] [s' : has_one A] : (one : A) + one = bit0 one :=
rfl
theorem subst_into_sum [s : has_add A] (l r tl tr t : A) (prl : l = tl) (prr : r = tr) (prt : tl + tr = t) :
l + r = t :=
theorem subst_into_sum [s : has_add A] (l r tl tr t : A) (prl : l = tl) (prr : r = tr)
(prt : tl + tr = t) : l + r = t :=
by rewrite [prl, prr, prt]
-- multiplication
@ -137,8 +144,13 @@ theorem mk_cong (op : A → A) (a b : A) (H : a = b) : op a = op b :=
theorem mk_eq (a : A) : a = a := rfl
theorem neg_add_neg_eq_of_add_add_eq_zero [s : add_comm_group A] (a b c : A) (H : c + a + b = 0) : -a + -b = c :=
begin apply add_neg_eq_of_eq_add, apply neg_eq_of_add_eq_zero, rewrite [add.comm, add.assoc, add.comm b, -add.assoc, H] end
theorem neg_add_neg_eq_of_add_add_eq_zero [s : add_comm_group A] (a b c : A) (H : c + a + b = 0) :
-a + -b = c :=
begin
apply add_neg_eq_of_eq_add,
apply neg_eq_of_add_eq_zero,
rewrite [add.comm, add.assoc, add.comm b, -add.assoc, H]
end
theorem neg_add_neg_helper [s : add_comm_group A] (a b c : A) (H : a + b = c) : -a + -b = -c :=
begin apply iff.mp !neg_eq_neg_iff_eq, rewrite [neg_add, *neg_neg, H] end
@ -155,8 +167,8 @@ theorem neg_add_pos_helper2 [s : add_comm_group A] (a b c : A) (H : a + c = b) :
theorem pos_add_neg_helper [s : add_comm_group A] (a b c : A) (H : b + a = c) : a + b = c :=
by rewrite [add.comm, H]
theorem sub_eq_add_neg_helper [s : add_comm_group A] (t₁ t₂ e w₁ w₂: A) (H₁ : t₁ = w₁) (H₂ : t₂ = w₂)
(H : w₁ + -w₂ = e) : t₁ - t₂ = e :=
theorem sub_eq_add_neg_helper [s : add_comm_group A] (t₁ t₂ e w₁ w₂: A) (H₁ : t₁ = w₁)
(H₂ : t₂ = w₂) (H : w₁ + -w₂ = e) : t₁ - t₂ = e :=
by rewrite [sub_eq_add_neg, H₁, H₂, H]
theorem pos_add_pos_helper [s : add_comm_group A] (a b c h₁ h₂ : A) (H₁ : a = h₁) (H₂ : b = h₂)
@ -185,36 +197,43 @@ theorem nonneg_bit0_helper [s : linear_ordered_semiring A] (a : A) (H : a ≥ 0)
by rewrite ↑bit0; apply add_nonneg H H
theorem pos_bit1_helper [s : linear_ordered_semiring A] (a : A) (H : a ≥ 0) : bit1 a > 0 :=
begin rewrite ↑bit1, apply add_pos_of_nonneg_of_pos, apply nonneg_bit0_helper _ H, apply zero_lt_one end
begin
rewrite ↑bit1,
apply add_pos_of_nonneg_of_pos,
apply nonneg_bit0_helper _ H,
apply zero_lt_one
end
theorem nonneg_bit1_helper [s : linear_ordered_semiring A] (a : A) (H : a ≥ 0) : bit1 a ≥ 0 :=
by apply le_of_lt; apply pos_bit1_helper _ H
theorem div_add_helper [s : field A] (n d b c val : A) (Hd : d ≠ 0) (H : n + b * d = val) (H2 : c * d = val) :
n / d + b = c :=
theorem div_add_helper [s : field A] (n d b c val : A) (Hd : d ≠ 0) (H : n + b * d = val)
(H2 : c * d = val) : n / d + b = c :=
begin
apply eq_of_mul_eq_mul_of_nonzero_right Hd,
rewrite [H2, -H, right_distrib, div_mul_cancel _ Hd]
end
theorem add_div_helper [s : field A] (n d b c val : A) (Hd : d ≠ 0) (H : d * b + n = val) (H2 : d * c = val) :
b + n / d = c :=
theorem add_div_helper [s : field A] (n d b c val : A) (Hd : d ≠ 0) (H : d * b + n = val)
(H2 : d * c = val) : b + n / d = c :=
begin
apply eq_of_mul_eq_mul_of_nonzero_left Hd,
rewrite [H2, -H, left_distrib, mul_div_cancel' Hd]
end
theorem div_mul_helper [s : field A] (n d c v : A) (Hd : d ≠ 0) (H : (n * c) / d = v) : (n / d) * c = v :=
begin rewrite [-H, field.div_mul_eq_mul_div_comm _ _ Hd, mul_div_assoc] end
theorem div_mul_helper [s : field A] (n d c v : A) (Hd : d ≠ 0) (H : (n * c) / d = v) :
(n / d) * c = v :=
by rewrite [-H, field.div_mul_eq_mul_div_comm _ _ Hd, mul_div_assoc]
theorem mul_div_helper [s : field A] (a n d v : A) (Hd : d ≠ 0) (H : (a * n) / d = v) : a * (n / d) = v :=
begin rewrite [-H, mul_div_assoc] end
theorem mul_div_helper [s : field A] (a n d v : A) (Hd : d ≠ 0) (H : (a * n) / d = v) :
a * (n / d) = v :=
by rewrite [-H, mul_div_assoc]
theorem nonzero_of_pos_helper [s : linear_ordered_semiring A] (a : A) (H : a > 0) : a ≠ 0 :=
ne_of_gt H
theorem nonzero_of_neg_helper [s : linear_ordered_ring A] (a : A) (H : a > 0) : -a ≠ 0 :=
begin apply ne_of_lt, apply neg_neg_of_pos H end
theorem nonzero_of_neg_helper [s : linear_ordered_ring A] (a : A) (H : a ≠ 0) : -a ≠ 0 :=
begin intro Ha, apply H, apply eq_of_neg_eq_neg, rewrite neg_zero, exact Ha end
theorem nonzero_of_div_helper [s : field A] (a b : A) (Ha : a ≠ 0) (Hb : b ≠ 0) : a / b ≠ 0 :=
begin
@ -225,11 +244,29 @@ theorem nonzero_of_div_helper [s : field A] (a b : A) (Ha : a ≠ 0) (Hb : b ≠
end
theorem div_helper [s : field A] (n d v : A) (Hd : d ≠ 0) (H : v * d = n) : n / d = v :=
begin apply eq_of_mul_eq_mul_of_nonzero_right Hd, rewrite (div_mul_cancel _ Hd), exact eq.symm H end
begin
apply eq_of_mul_eq_mul_of_nonzero_right Hd,
rewrite (div_mul_cancel _ Hd),
exact eq.symm H
end
theorem div_eq_div_helper [s : field A] (a b c d v : A) (H1 : a * d = v) (H2 : c * b = v)
(Hb : b ≠ 0) (Hd : d ≠ 0) : a / b = c / d :=
begin apply eq_div_of_mul_eq, exact Hd, rewrite div_mul_eq_mul_div, apply eq.symm, apply eq_div_of_mul_eq, exact Hb, rewrite [H1, H2] end
begin
apply eq_div_of_mul_eq,
exact Hd,
rewrite div_mul_eq_mul_div,
apply eq.symm,
apply eq_div_of_mul_eq,
exact Hb,
rewrite [H1, H2]
end
theorem subst_into_div [s : has_division A] (a₁ b₁ a₂ b₂ v : A) (H : a₁ / b₁ = v) (H1 : a₂ = a₁) (H2 : b₂ = b₁) :
a₂ / b₂ = v := by rewrite [H1, H2, H]
theorem subst_into_div [s : has_div A] (a₁ b₁ a₂ b₂ v : A) (H : a₁ / b₁ = v) (H1 : a₂ = a₁)
(H2 : b₂ = b₁) : a₂ / b₂ = v :=
by rewrite [H1, H2, H]
theorem neg_zero_helper [s : add_group A] (a : A) (H : a = 0) : - a = 0 :=
by rewrite [H, neg_zero]
end norm_num

526
src/library/norm_num.cpp
View file

@ -56,8 +56,8 @@ static name * g_add = 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_pos_add_neg = nullptr,
* g_pos_add_pos = nullptr,
* g_neg_mul_neg = nullptr,
* g_pos_mul_neg = nullptr,
* g_neg_mul_pos = nullptr,
@ -68,22 +68,23 @@ static name * g_add = 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_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_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) {
@ -120,9 +121,14 @@ bool norm_num_context::is_div(expr const & e) const {
Takes A : Type, and tries to synthesize has_add A.
*/
expr norm_num_context::mk_has_add(expr const & e) {
expr t = mk_app(mk_constant(get_has_add_name(), m_lvls), e);
auto l_name = get_has_add_name();
if (instances.find(l_name) != instances.end()) {
return instances[l_name];
}
expr t = mk_app(mk_constant(l_name, m_lvls), e);
optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
if (inst) {
instances[l_name] = *inst;
return *inst;
} else {
throw exception("failed to synthesize has_add instance");
@ -130,9 +136,14 @@ expr norm_num_context::mk_has_add(expr const & e) {
}
expr norm_num_context::mk_has_mul(expr const & e) {
expr t = mk_app(mk_constant(*g_has_mul, m_lvls), e);
auto l_name = *g_has_mul;
if (instances.find(l_name) != instances.end()) {
return instances[l_name];
}
expr t = mk_app(mk_constant(l_name, m_lvls), e);
optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
if (inst) {
instances[l_name] = *inst;
return *inst;
} else {
throw exception("failed to synthesize has_mul instance");
@ -140,9 +151,14 @@ expr norm_num_context::mk_has_mul(expr const & e) {
}
expr norm_num_context::mk_has_one(expr const & e) {
expr t = mk_app(mk_constant(get_has_one_name(), m_lvls), e);
auto l_name = get_has_one_name();
if (instances.find(l_name) != instances.end()) {
return instances[l_name];
}
expr t = mk_app(mk_constant(l_name, m_lvls), e);
optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
if (inst) {
instances[l_name] = *inst;
return *inst;
} else {
throw exception("failed to synthesize has_one instance");
@ -150,9 +166,14 @@ expr norm_num_context::mk_has_one(expr const & e) {
}
expr norm_num_context::mk_has_zero(expr const & e) {
expr t = mk_app(mk_constant(get_has_zero_name(), m_lvls), e);
auto l_name = get_has_zero_name();
if (instances.find(l_name) != instances.end()) {
return instances[l_name];
}
expr t = mk_app(mk_constant(l_name, m_lvls), e);
optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
if (inst) {
instances[l_name] = *inst;
return *inst;
} else {
throw exception("failed to synthesize has_one instance");
@ -160,9 +181,14 @@ expr norm_num_context::mk_has_zero(expr const & e) {
}
expr norm_num_context::mk_add_monoid(expr const & e) {
expr t = mk_app(mk_constant(*g_add_monoid, m_lvls), e);
auto l_name = *g_add_monoid;
if (instances.find(l_name) != instances.end()) {
return instances[l_name];
}
expr t = mk_app(mk_constant(l_name, m_lvls), e);
optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
if (inst) {
instances[l_name] = *inst;
return *inst;
} else {
throw exception("failed to synthesize add_monoid instance");
@ -170,9 +196,14 @@ expr norm_num_context::mk_add_monoid(expr const & e) {
}
expr norm_num_context::mk_monoid(expr const & e) {
expr t = mk_app(mk_constant(*g_monoid, m_lvls), e);
auto l_name = *g_monoid;
if (instances.find(l_name) != instances.end()) {
return instances[l_name];
}
expr t = mk_app(mk_constant(l_name, m_lvls), e);
optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
if (inst) {
instances[l_name] = *inst;
return *inst;
} else {
throw exception("failed to synthesize monoid instance");
@ -190,9 +221,14 @@ expr norm_num_context::mk_field(expr const & e) {
}
expr norm_num_context::mk_add_comm(expr const & e) {
expr t = mk_app(mk_constant(*g_add_comm, m_lvls), e);
auto l_name = *g_add_comm;
if (instances.find(l_name) != instances.end()) {
return instances[l_name];
}
expr t = mk_app(mk_constant(l_name, m_lvls), e);
optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
if (inst) {
instances[l_name] = *inst;
return *inst;
} else {
throw exception("failed to synthesize add_comm_semigroup instance");
@ -200,9 +236,14 @@ expr norm_num_context::mk_add_comm(expr const & e) {
}
expr norm_num_context::mk_add_group(expr const & e) {
expr t = mk_app(mk_constant(*g_add_group, m_lvls), e);
auto l_name = *g_add_group;
if (instances.find(l_name) != instances.end()) {
return instances[l_name];
}
expr t = mk_app(mk_constant(l_name, m_lvls), e);
optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
if (inst) {
instances[l_name] = *inst;
return *inst;
} else {
throw exception("failed to synthesize add_comm_semigroup instance");
@ -210,9 +251,14 @@ expr norm_num_context::mk_add_group(expr const & e) {
}
expr norm_num_context::mk_has_distrib(expr const & e) {
expr t = mk_app(mk_constant(*g_distrib, m_lvls), e);
auto l_name = *g_distrib;
if (instances.find(l_name) != instances.end()) {
return instances[l_name];
}
expr t = mk_app(mk_constant(l_name, m_lvls), e);
optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
if (inst) {
instances[l_name] = *inst;
return *inst;
} else {
throw exception("failed to synthesize has_distrib instance");
@ -220,9 +266,14 @@ expr norm_num_context::mk_has_distrib(expr const & e) {
}
expr norm_num_context::mk_mul_zero_class(expr const & e) {
expr t = mk_app(mk_constant(*g_mul_zero_class, m_lvls), e);
auto l_name = *g_mul_zero_class;
if (instances.find(l_name) != instances.end()) {
return instances[l_name];
}
expr t = mk_app(mk_constant(l_name, m_lvls), e);
optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
if (inst) {
instances[l_name] = *inst;
return *inst;
} else {
throw exception("failed to synthesize mul_zero instance");
@ -230,9 +281,14 @@ expr norm_num_context::mk_mul_zero_class(expr const & e) {
}
expr norm_num_context::mk_semiring(expr const & e) {
expr t = mk_app(mk_constant(*g_semiring, m_lvls), e);
auto l_name = *g_semiring;
if (instances.find(l_name) != instances.end()) {
return instances[l_name];
}
expr t = mk_app(mk_constant(l_name, m_lvls), e);
optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
if (inst) {
instances[l_name] = *inst;
return *inst;
} else {
throw exception("failed to synthesize semiring instance");
@ -240,9 +296,14 @@ expr norm_num_context::mk_semiring(expr const & e) {
}
expr norm_num_context::mk_has_neg(expr const & e) {
expr t = mk_app(mk_constant(*g_has_neg, m_lvls), e);
auto l_name = *g_has_neg;
if (instances.find(l_name) != instances.end()) {
return instances[l_name];
}
expr t = mk_app(mk_constant(l_name, m_lvls), e);
optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
if (inst) {
instances[l_name] = *inst;
return *inst;
} else {
throw exception("failed to synthesize has_neg instance");
@ -250,9 +311,14 @@ expr norm_num_context::mk_has_neg(expr const & e) {
}
expr norm_num_context::mk_has_sub(expr const & e) {
expr t = mk_app(mk_constant(*g_has_sub, m_lvls), e);
auto l_name = *g_has_sub;
if (instances.find(l_name) != instances.end()) {
return instances[l_name];
}
expr t = mk_app(mk_constant(l_name, m_lvls), e);
optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
if (inst) {
instances[l_name] = *inst;
return *inst;
} else {
throw exception("failed to synthesize has_sub instance");
@ -260,9 +326,14 @@ expr norm_num_context::mk_has_sub(expr const & e) {
}
expr norm_num_context::mk_has_div(expr const & e) {
expr t = mk_app(mk_constant(*g_has_div, m_lvls), e);
auto l_name = *g_has_div;
if (instances.find(l_name) != instances.end()) {
return instances[l_name];
}
expr t = mk_app(mk_constant(l_name, m_lvls), e);
optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
if (inst) {
instances[l_name] = *inst;
return *inst;
} else {
throw exception("failed to synthesize has_div instance");
@ -270,9 +341,14 @@ expr norm_num_context::mk_has_div(expr const & e) {
}
expr norm_num_context::mk_add_comm_group(expr const & e) {
expr t = mk_app(mk_constant(*g_add_comm_group, m_lvls), e);
auto l_name = *g_add_comm_group;
if (instances.find(l_name) != instances.end()) {
return instances[l_name];
}
expr t = mk_app(mk_constant(l_name, m_lvls), e);
optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
if (inst) {
instances[l_name] = *inst;
return *inst;
} else {
throw exception("failed to synthesize add_comm_group instance");
@ -280,9 +356,14 @@ expr norm_num_context::mk_add_comm_group(expr const & e) {
}
expr norm_num_context::mk_ring(expr const & e) {
expr t = mk_app(mk_constant(*g_ring, m_lvls), e);
auto l_name = *g_ring;
if (instances.find(l_name) != instances.end()) {
return instances[l_name];
}
expr t = mk_app(mk_constant(l_name, m_lvls), e);
optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
if (inst) {
instances[l_name] = *inst;
return *inst;
} else {
throw exception("failed to synthesize ring instance");
@ -290,9 +371,14 @@ expr norm_num_context::mk_ring(expr const & e) {
}
expr norm_num_context::mk_lin_ord_ring(expr const & e) {
expr t = mk_app(mk_constant(*g_lin_ord_ring, m_lvls), e);
auto l_name = *g_lin_ord_ring;
if (instances.find(l_name) != instances.end()) {
return instances[l_name];
}
expr t = mk_app(mk_constant(l_name, m_lvls), e);
optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
if (inst) {
instances[l_name] = *inst;
return *inst;
} else {
throw exception("failed to synthesize lin_ord_ring instance");
@ -300,9 +386,14 @@ expr norm_num_context::mk_lin_ord_ring(expr const & e) {
}
expr norm_num_context::mk_lin_ord_semiring(expr const & e) {
expr t = mk_app(mk_constant(*g_lin_ord_semiring, m_lvls), e);
auto l_name = *g_lin_ord_semiring;
if (instances.find(l_name) != instances.end()) {
return instances[l_name];
}
expr t = mk_app(mk_constant(l_name, m_lvls), e);
optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
if (inst) {
instances[l_name] = *inst;
return *inst;
} else {
throw exception("failed to synthesize lin_ord_semiring instance");
@ -310,9 +401,14 @@ expr norm_num_context::mk_lin_ord_semiring(expr const & e) {
}
expr norm_num_context::mk_wk_order(expr const & e) {
expr t = mk_app(mk_constant(*g_wk_order, m_lvls), e);
auto l_name = *g_wk_order;
if (instances.find(l_name) != instances.end()) {
return instances[l_name];
}
expr t = mk_app(mk_constant(l_name, m_lvls), e);
optional<expr> inst = mk_class_instance(m_env, m_ctx, t);
if (inst) {
instances[l_name] = *inst;
return *inst;
} else {
throw exception("failed to synthesize weak_order instance");
@ -323,7 +419,8 @@ expr norm_num_context::mk_const(name const & n) {
return mk_constant(n, m_lvls);
}
expr norm_num_context::mk_cong(expr const & op, expr const & type, expr const & a, expr const & b, expr const & eq) {
expr norm_num_context::mk_cong(expr const & op, expr const & type, expr const & a,
expr const & b, expr const & eq) {
return mk_app({mk_const(*g_mk_cong), type, op, a, b, eq});
}
@ -338,35 +435,39 @@ pair<expr, expr> norm_num_context::mk_norm_add(expr const & lhs, expr const & rh
}
auto type = args_lhs[0];
auto typec = args_lhs[1];
// std::cout << "typec in mk_norm_add is: " << typec << ". lhs: " << lhs << ", rhs: " << rhs << "\n";
expr rv;
expr prf;
if (is_bit0(lhs) && is_bit0(rhs)) { // typec is has_add
auto p = mk_norm_add(args_lhs[2], args_rhs[2]);
rv = mk_app(lhs_head, type, typec, p.first);
prf = mk_app({mk_const(*g_bit0_add_bit0), type, mk_add_comm(type), args_lhs[2], args_rhs[2], p.first, p.second});
prf = mk_app({mk_const(*g_bit0_add_bit0), type, mk_add_comm(type),
args_lhs[2], args_rhs[2], p.first, p.second});
} else if (is_bit0(lhs) && is_bit1(rhs)) {
auto p = mk_norm_add(args_lhs[2], args_rhs[3]);
rv = mk_app({rhs_head, type, args_rhs[1], args_rhs[2], p.first});
prf = mk_app({mk_const(*g_bit0_add_bit1), type, mk_add_comm(type), args_rhs[1], args_lhs[2], args_rhs[3], p.first, p.second});
prf = mk_app({mk_const(*g_bit0_add_bit1), type, mk_add_comm(type), args_rhs[1],
args_lhs[2], args_rhs[3], p.first, p.second});
} else if (is_bit0(lhs) && is_one(rhs)) {
rv = mk_app({mk_const(get_bit1_name()), type, args_rhs[1], args_lhs[1], args_lhs[2]});
prf = mk_app({mk_const(*g_bit0_add_1), type, typec, args_rhs[1], args_lhs[2]});
} else if (is_bit1(lhs) && is_bit0(rhs)) { // typec is has_one
auto p = mk_norm_add(args_lhs[3], args_rhs[2]);
rv = mk_app(lhs_head, type, typec, args_lhs[2], p.first);
prf = mk_app({mk_const(*g_bit1_add_bit0), type, mk_add_comm(type), typec, args_lhs[3], args_rhs[2], p.first, p.second});
prf = mk_app({mk_const(*g_bit1_add_bit0), type, mk_add_comm(type), typec,
args_lhs[3], args_rhs[2], p.first, p.second});
} else if (is_bit1(lhs) && is_bit1(rhs)) { // typec is has_one
auto add_ts = mk_norm_add(args_lhs[3], args_rhs[3]);
expr add1 = mk_app({mk_const(*g_add1), type, args_lhs[2], typec, add_ts.first});
auto p = mk_norm_add1(add1);
rv = mk_app({mk_const(get_bit0_name()), type, args_lhs[2], p.first});
prf = mk_app({mk_const(*g_bit1_add_bit1), type, mk_add_comm(type), typec, args_lhs[3], args_rhs[3], add_ts.first, p.first, add_ts.second, p.second});
prf = mk_app({mk_const(*g_bit1_add_bit1), type, mk_add_comm(type), typec,
args_lhs[3], args_rhs[3], add_ts.first, p.first, add_ts.second, p.second});
} else if (is_bit1(lhs) && is_one(rhs)) { // typec is has_one
expr add1 = mk_app({mk_const(*g_add1), type, args_lhs[2], typec, lhs});
auto p = mk_norm_add1(add1);
rv = p.first;
prf = mk_app({mk_const(*g_bit1_add_1), type, args_lhs[2], typec, args_lhs[3], p.first, p.second});
prf = mk_app({mk_const(*g_bit1_add_1), type, args_lhs[2], typec,
args_lhs[3], p.first, p.second});
} else if (is_one(lhs) && is_bit0(rhs)) { // typec is has_one
rv = mk_app({mk_const(get_bit1_name()), type, typec, args_rhs[1], args_rhs[2]});
prf = mk_app({mk_const(*g_1_add_bit0), type, mk_add_comm(type), typec, args_rhs[2]});
@ -374,7 +475,8 @@ pair<expr, expr> norm_num_context::mk_norm_add(expr const & lhs, expr const & rh
expr add1 = mk_app({mk_const(*g_add1), type, args_rhs[2], args_rhs[1], rhs});
auto p = mk_norm_add1(add1);
rv = p.first;
prf = mk_app({mk_const(*g_1_add_bit1), type, mk_add_comm(type), typec, args_rhs[3], p.first, p.second});
prf = mk_app({mk_const(*g_1_add_bit1), type, mk_add_comm(type), typec,
args_rhs[3], p.first, p.second});
} else if (is_one(lhs) && is_one(rhs)) {
rv = mk_app({mk_const(get_bit0_name()), type, mk_has_add(type), lhs});
prf = mk_app({mk_const(*g_one_add_one), type, mk_has_add(type), typec});
@ -385,10 +487,7 @@ pair<expr, expr> norm_num_context::mk_norm_add(expr const & lhs, expr const & rh
rv = lhs;
prf = mk_app({mk_const(*g_bin_add_0), type, mk_add_monoid(type), lhs});
} else {
std::cout << "\n\n bad args: " << lhs_head << ", " << rhs_head << "\n";
std::cout << "\nlhs: " << lhs;
std::cout << "\nrhs: " << rhs;
throw exception("mk_norm_add got malformed args");
throw exception("mk_norm_add got malformed args");
}
return pair<expr, expr>(rv, prf);
}
@ -409,15 +508,16 @@ pair<expr, expr> norm_num_context::mk_norm_add1(expr const & e) {
} 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]}));
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]), args[2], ne_args[3], np.first, np.second});
prf = mk_app({mk_const(*g_add1_bit1), args[0], mk_add_comm(args[0]),
args[2], ne_args[3], np.first, np.second});
} else if (is_zero(p)) {
rv = mk_app({mk_const(get_one_name()), args[0], args[2]});
prf = mk_app({mk_const(*g_add1_zero), args[0], mk_add_monoid(args[0]), args[2]});
} else if (is_one(p)) {
rv = mk_app({mk_const(get_bit0_name()), args[0], args[1], mk_app({mk_const(get_one_name()), args[0], args[2]})});
rv = mk_app({mk_const(get_bit0_name()), args[0], args[1],
mk_app({mk_const(get_one_name()), args[0], args[2]})});
prf = mk_app({mk_const(*g_add1_one), args[0], args[1], args[2]});
} else {
std::cout << "malformed add1: " << ne << "\n";
throw exception("malformed add1");
}
return pair<expr, expr>(rv, prf);
@ -447,31 +547,21 @@ pair<expr, expr> norm_num_context::mk_norm_mul(expr const & lhs, expr const & rh
} else if (is_bit0(rhs)) {
auto mtp = mk_norm_mul(lhs, args_rhs[2]);
rv = mk_app({rhs_head, type, typec, mtp.first});
prf = mk_app({mk_const(*g_mul_bit0), type, mk_has_distrib(type), lhs, args_rhs[2], mtp.first, mtp.second});
prf = mk_app({mk_const(*g_mul_bit0), type, mk_has_distrib(type), lhs,
args_rhs[2], mtp.first, mtp.second});
} else if (is_bit1(rhs)) {
auto mtp = mk_norm_mul(lhs, args_rhs[3]);
// std::cout << "** in mk_norm_mul. calling mk_norm_add on" << mtp.first << ", " << lhs;
auto atp = mk_norm_add(mk_app({mk_const(get_bit0_name()), type, args_rhs[2], mtp.first}), lhs);
auto atp = mk_norm_add(mk_app({mk_const(get_bit0_name()), type, args_rhs[2], mtp.first}),
lhs);
rv = atp.first;
prf = mk_app({mk_const(*g_mul_bit1), type, mk_semiring(type), lhs, args_rhs[3],
mtp.first, atp.first, mtp.second, atp.second});
} else {
std::cout << "bad args to mk_norm_mul: " << rhs << "\n";
throw exception("mk_norm_mul got malformed args");
}
return pair<expr, expr>(rv, prf);
}
pair<expr, expr> norm_num_context::mk_norm_div(expr const &, expr const &) {
// TODO(Rob)
throw exception("not implemented yet -- mk_norm_div");
}
pair<expr, expr> norm_num_context::mk_norm_sub(expr const &, expr const &) {
// TODO(Rob)
throw exception("not implemented yet -- mk_norm_sub");
}
optional<mpq> norm_num_context::to_mpq(expr const & e) {
auto v = to_num(e);
if (v) {
@ -505,7 +595,6 @@ mpq norm_num_context:: mpq_of_expr(expr const & e){
if (v) {
return *v;
} else {
std::cout << "error : " << f << args.size() << "\n";
throw exception("expression in mpq_of_expr is malfomed");
}
}
@ -530,7 +619,6 @@ mpz norm_num_context::num_of_expr(expr const & e) {
} else if (const_name(f) == *g_neg && args.size() == 3) {
return neg(num_of_expr(args[2]));
} else {
std::cout << "error : " << f << "\n";
throw exception("expression in num_of_expr is malfomed");
}
}
@ -551,8 +639,9 @@ expr norm_num_context::mk_norm_eq_neg_add_neg(expr & s_lhs, expr & s_rhs, expr &
auto s_rhs_v = get_type_and_arg_of_neg(s_rhs).second;
auto rhs_v = get_type_and_arg_of_neg(rhs);
expr type = rhs_v.first;
auto sum_pr = mk_norm_eq_pos_add_pos(s_lhs_v, s_rhs_v, rhs_v.second);
return mk_app({mk_const(*g_neg_add_neg_eq), type, mk_add_comm_group(type), s_lhs_v, s_rhs_v, rhs_v.second, sum_pr});
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),
s_lhs_v, s_rhs_v, rhs_v.second, sum_pr});
}
expr norm_num_context::mk_norm_eq_neg_add_pos(expr & s_lhs, expr & s_rhs, expr & rhs) {
@ -562,11 +651,13 @@ expr norm_num_context::mk_norm_eq_neg_add_pos(expr & s_lhs, expr & s_rhs, expr &
expr type = s_lhs_v.first;
if (is_neg_app(rhs)) {
auto rhs_v = get_type_and_arg_of_neg(rhs).second;
auto sum_pr = mk_norm_eq_pos_add_pos(s_rhs, rhs_v, s_lhs_v.second);
return mk_app({mk_const(*g_neg_add_pos1), type, mk_add_comm_group(type), s_lhs_v.second, s_rhs, rhs_v, sum_pr});
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),
s_lhs_v.second, s_rhs, rhs_v, sum_pr});
} else {
auto sum_pr = mk_norm_eq_pos_add_pos(s_lhs_v.second, rhs, s_rhs);
return mk_app({mk_const(*g_neg_add_pos2), type, mk_add_comm_group(type), s_lhs_v.second, s_rhs, rhs, sum_pr});
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),
s_lhs_v.second, s_rhs, rhs, sum_pr});
}
}
@ -575,7 +666,8 @@ expr norm_num_context::mk_norm_eq_pos_add_neg(expr & s_lhs, expr & s_rhs, expr &
lean_assert(!is_neg_app(s_lhs));
expr prf = mk_norm_eq_neg_add_pos(s_rhs, s_lhs, rhs);
expr type = get_type_and_arg_of_neg(s_rhs).first;
return mk_app({mk_const(*g_pos_add_neg), type, mk_add_comm_group(type), s_lhs, s_rhs, rhs, prf});
return mk_app({mk_const(*g_pos_add_neg), type, mk_add_comm_group(type), s_lhs,
s_rhs, rhs, prf});
}
// returns a proof that s_lhs + s_rhs = rhs, where all are nonneg normalized numerals
@ -595,9 +687,10 @@ expr norm_num_context::mk_norm_eq_neg_mul_neg(expr & s_lhs, expr & s_rhs, expr &
auto s_lhs_v = get_type_and_arg_of_neg(s_lhs).second;
expr s_rhs_v, type;
std::tie(type, s_rhs_v) = get_type_and_arg_of_neg(s_rhs);
auto prod_pr = mk_norm(mk_mul(type, s_lhs_v, s_rhs_v)); //, rhs);
auto prod_pr = mk_norm(mk_mul(type, s_lhs_v, s_rhs_v));
lean_assert(to_num(rhs) == to_num(prod_pr.first));
return mk_app({mk_const(*g_neg_mul_neg), type, mk_ring(type), s_lhs_v, s_rhs_v, rhs, prod_pr.second});
return mk_app({mk_const(*g_neg_mul_neg), type, mk_ring(type), s_lhs_v,
s_rhs_v, rhs, prod_pr.second});
}
expr norm_num_context::mk_norm_eq_neg_mul_pos(expr & s_lhs, expr & s_rhs, expr & rhs) {
@ -607,8 +700,9 @@ expr norm_num_context::mk_norm_eq_neg_mul_pos(expr & s_lhs, expr & s_rhs, expr &
expr s_lhs_v, type;
std::tie(type, s_lhs_v) = get_type_and_arg_of_neg(s_lhs);
auto rhs_v = get_type_and_arg_of_neg(rhs).second;
auto prod_pr = mk_norm(mk_mul(type, s_lhs_v, s_rhs)); //, rhs_v);
return mk_app({mk_const(*g_neg_mul_pos), type, mk_ring(type), s_lhs_v, s_rhs, rhs_v, prod_pr.second});
auto prod_pr = mk_norm(mk_mul(type, s_lhs_v, s_rhs));
return mk_app({mk_const(*g_neg_mul_pos), type, mk_ring(type), s_lhs_v, s_rhs,
rhs_v, prod_pr.second});
}
expr norm_num_context::mk_norm_eq_pos_mul_neg(expr & s_lhs, expr & s_rhs, expr & rhs) {
@ -618,8 +712,9 @@ expr norm_num_context::mk_norm_eq_pos_mul_neg(expr & s_lhs, expr & s_rhs, expr &
expr s_rhs_v, type;
std::tie(type, s_rhs_v) = get_type_and_arg_of_neg(s_rhs);
auto rhs_v = get_type_and_arg_of_neg(rhs).second;
auto prod_pr = mk_norm(mk_mul(type, s_lhs, s_rhs_v)); //, rhs_v);
return mk_app({mk_const(*g_pos_mul_neg), type, mk_ring(type), s_lhs, s_rhs_v, rhs_v, prod_pr.second});
auto prod_pr = mk_norm(mk_mul(type, s_lhs, s_rhs_v));
return mk_app({mk_const(*g_pos_mul_neg), type, mk_ring(type), s_lhs, s_rhs_v,
rhs_v, prod_pr.second});
}
// returns a proof that s_lhs + s_rhs = rhs, where all are nonneg normalized numerals
@ -637,9 +732,11 @@ expr norm_num_context::from_pos_num(mpz const & n, expr const & type) {
if (n == 1)
return mk_app({mk_const(get_one_name()), type, mk_has_one(type)});
if (n % mpz(2) == 1)
return mk_app({mk_const(get_bit1_name()), type, mk_has_one(type), mk_has_add(type), from_pos_num(n/2, type)});
return mk_app({mk_const(get_bit1_name()), type, mk_has_one(type),
mk_has_add(type), from_pos_num(n/2, type)});
else
return mk_app({mk_const(get_bit0_name()), type, mk_has_add(type), from_pos_num(n/2, type)});
return mk_app({mk_const(get_bit0_name()), type, mk_has_add(type),
from_pos_num(n/2, type)});
}
expr norm_num_context::from_num(mpz const & n, expr const & type) {
@ -685,38 +782,6 @@ expr norm_num_context::mk_mul(expr const & type, expr const & e1, expr const & e
return mk_app({mk_const(*g_mul), type, has_mul, e1, e2});
}
/*mpz mpz_gcd(mpz a, mpz b) {
return b == 0 ? a : mpz_gcd(b, a % b);
}*/
/*pair<expr, expr> norm_num_context::mk_norm_div_over_div(expr & lhs, expr & rhs) {
buffer<expr> lhs_args, rhs_args;
get_app_args(lhs, lhs_args);
get_app_args(rhs, rhs_args);
expr type = lhs_args[0];
expr a = lhs_args[2], b = lhs_args[3], c = rhs_args[2], d = rhs_args[3];
lean_assert(!is_div(a) && !is_div(b) && !is_div(c) && !is_div(d));
// normalizing (a/b) / (c/d), where a, b, c, d are not divs
auto nlhs = mk_norm(mk_mul(type, a, d));
auto nrhs = mk_norm(mk_mul(type, b, c));
auto nlhs_val = to_num(nlhs.first), rlhs_val = to_num(nrhs.first);
if (nlhs_val && rlhs_val) {
}
}
pair<expr, expr> norm_num_context::mk_norm_div_over_num(expr &, expr &) {
}
pair<expr, expr> norm_num_context::mk_norm_num_over_div(expr &, expr &) {
}
pair<expr, expr> norm_num_context::mk_norm_num_over_num(expr &, expr &) {
}*/
// s_lhs is div. returns proof that s_lhs + s_rhs = rhs
expr norm_num_context::mk_norm_div_add(expr & s_lhs, expr & s_rhs, expr & rhs) {
buffer<expr> s_lhs_args;
@ -727,7 +792,6 @@ expr norm_num_context::mk_norm_div_add(expr & s_lhs, expr & s_rhs, expr & rhs) {
auto npr_l = mk_norm(new_lhs);
auto npr_r = mk_norm(mk_mul(type, rhs, den));
lean_assert(to_mpq(npr_l.first) == to_mpq(npr_r.first));
if (!(is_numeral(den))) { std::cout << "\n****bad input in mk_norm_div_add\n"; }
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,
npr_l.first, den_neq_zero, npr_l.second, npr_r.second});
@ -743,9 +807,8 @@ expr norm_num_context::mk_norm_add_div(expr & s_lhs, expr & s_rhs, expr & rhs) {
auto npr_l = mk_norm(new_lhs);
auto npr_r = mk_norm(mk_mul(type, den, rhs));
lean_assert(to_mpq(npr_l.first) == to_mpq(npr_r.first));
if (!(is_numeral(den))) { std::cout << "\n****bad input in mk_norm_add_div\n"; }
expr den_neq_zero = mk_nonzero_prf(den);
return mk_app({mk_const(*g_add_div), type, mk_field(type), num, den, s_rhs, rhs,
return mk_app({mk_const(*g_add_div), type, mk_field(type), num, den, s_lhs, rhs,
npr_l.first, den_neq_zero, npr_l.second, npr_r.second});
}
@ -754,12 +817,15 @@ expr norm_num_context::mk_nonzero_prf(expr const & e) {
buffer<expr> args;
expr f = get_app_args(e, args);
if (const_name(f) == *g_neg) {
return mk_app({mk_const(*g_nonzero_neg), args[0], mk_lin_ord_ring(args[0]), args[2], mk_pos_prf(args[2])});
return mk_app({mk_const(*g_nonzero_neg), args[0], mk_lin_ord_ring(args[0]),
args[2], mk_nonzero_prf(args[2])});
} else if (const_name(f) == *g_div) {
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], args[3], num_pr, den_pr});
return mk_app({mk_const(*g_nonzero_div), args[0], mk_field(args[0]), args[2],
args[3], num_pr, den_pr});
} else {
return mk_app({mk_const(*g_nonzero_pos), args[0], mk_lin_ord_semiring(args[0]), e, mk_pos_prf(e)});
return mk_app({mk_const(*g_nonzero_pos), args[0], mk_lin_ord_semiring(args[0]),
e, mk_pos_prf(e)});
}
}
@ -778,7 +844,6 @@ expr norm_num_context::mk_pos_prf(expr const & e) {
} else if (is_one(e)) {
return mk_app({mk_const(*g_zero_lt_one), type, mk_lin_ord_semiring(type)});
} else {
std::cout << "bad call to mk_pos_prf: " << e << "\n";
throw exception("mk_pos_proof called on zero or non_numeral");
}
}
@ -797,9 +862,9 @@ expr norm_num_context::mk_nonneg_prf(expr const & e) {
} else if (is_one(e)) {
return mk_app({mk_const(*g_zero_le_one), type, mk_lin_ord_ring(type)});
} else if (is_zero(e)) {
return mk_app({mk_const(*g_le_refl), type, mk_wk_order(type), mk_app({mk_const(get_zero_name()), type, mk_has_zero(type)})});
return mk_app({mk_const(*g_le_refl), type, mk_wk_order(type),
mk_app({mk_const(get_zero_name()), type, mk_has_zero(type)})});
} else {
std::cout << "bad call to mk_nonneg_prf: " << e << "\n";
throw exception("mk_nonneg_proof called on zero or non_numeral");
}
}
@ -812,9 +877,9 @@ expr norm_num_context::mk_norm_div_mul(expr & s_lhs, expr & s_rhs, expr & rhs) {
expr new_num = mk_mul(type, args[2], s_rhs);
auto prf = mk_norm(mk_div(type, new_num, args[3]));
lean_assert(to_mpq(prf.first) == to_mpq(rhs));
if (!(is_numeral(args[3]))) { std::cout << "\n****bad input in mk_norm_div_mul\n"; }
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, rhs, den_ne_zero, prf.second});
return mk_app({mk_const(*g_div_mul), type, mk_field(type), args[2], args[3], s_rhs,
rhs, den_ne_zero, prf.second});
}
expr norm_num_context::mk_norm_mul_div(expr & s_lhs, expr & s_rhs, expr & rhs) {
@ -824,13 +889,12 @@ expr norm_num_context::mk_norm_mul_div(expr & s_lhs, expr & s_rhs, expr & rhs) {
expr new_num = mk_mul(type, s_lhs, args[2]);
auto prf = mk_norm(mk_div(type, new_num, args[3]));
lean_assert(to_mpq(prf.first) == to_mpq(rhs));
if (!(is_numeral(args[3]))) { std::cout << "\n****bad input in mk_norm_mul_div\n"; }
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], rhs, den_ne_zero, prf.second});
return mk_app({mk_const(*g_mul_div), type, mk_field(type), s_lhs, args[2], args[3],
rhs, den_ne_zero, prf.second});
}
pair<expr, expr> norm_num_context::mk_norm(expr const & e) {
//std::cout << "mk_norm: " << e << "\n";
buffer<expr> args;
expr f = get_app_args(e, args);
if (!is_constant(f) || args.size() == 0) {
@ -838,6 +902,10 @@ pair<expr, expr> norm_num_context::mk_norm(expr const & e) {
}
m_lvls = const_levels(f);
expr type = args[0];
if (is_numeral(e)) {
expr prf = mk_app({mk_const(*g_mk_eq), type, e});
return pair<expr, expr>(e, prf);
}
mpq val = mpq_of_expr(e);
expr nval; // e = nval
if (val >= 0) {
@ -849,11 +917,7 @@ pair<expr, expr> norm_num_context::mk_norm(expr const & e) {
expr prf;
auto lhs_p = mk_norm(args[2]);
auto rhs_p = mk_norm(args[3]);
if (is_div(lhs_p.first)) {
prf = mk_norm_div_add(lhs_p.first, rhs_p.first, nval);
} else if (is_div(rhs_p.first)) {
prf = mk_norm_add_div(lhs_p.first, rhs_p.first, nval);
} else if (is_neg_app(lhs_p.first)) {
if (is_neg_app(lhs_p.first)) {
if (is_neg_app(rhs_p.first)) {
prf = mk_norm_eq_neg_add_neg(lhs_p.first, rhs_p.first, nval);
} else {
@ -863,7 +927,13 @@ pair<expr, expr> norm_num_context::mk_norm(expr const & e) {
if (is_neg_app(rhs_p.first)) {
prf = mk_norm_eq_pos_add_neg(lhs_p.first, rhs_p.first, nval);
} else {
prf = mk_norm_eq_pos_add_pos(lhs_p.first, rhs_p.first, nval);
if (is_div(lhs_p.first)) {
prf = mk_norm_div_add(lhs_p.first, rhs_p.first, nval);
} else if (is_div(rhs_p.first)) {
prf = mk_norm_add_div(lhs_p.first, rhs_p.first, nval);
} else {
prf = mk_norm_eq_pos_add_pos(lhs_p.first, rhs_p.first, nval);
}
}
}
expr rprf = mk_app({mk_const(*g_subst_sum), type, mk_has_add(type), args[2], args[3],
@ -873,25 +943,27 @@ pair<expr, expr> norm_num_context::mk_norm(expr const & e) {
} else if (const_name(f) == *g_sub && args.size() == 4) {
expr sum = mk_add(args[0], args[2], mk_neg(args[0], args[3]));
auto anprf = mk_norm(sum);
expr rprf = mk_app({mk_const(*g_subst_subtr), type, mk_add_group(type), args[2], args[3], anprf.first, anprf.second});
expr rprf = mk_app({mk_const(*g_subst_subtr), type, mk_add_group(type), args[2],
args[3], anprf.first, anprf.second});
return pair<expr, expr>(nval, rprf);
} else if (const_name(f) == *g_neg && args.size() == 3) {
auto prf = mk_norm(args[2]);
/*std::cout << "in mk_norm. const is neg. e: " << e << "\n";
std::cout << " val: ";
std::cout << val;
std::cout << "\n nval: ";
std::cout << nval << "\n";*/
lean_assert(mpq_of_expr(prf.first) == neg(val));
if (is_zero(prf.first)) {
expr rprf = mk_app({mk_const(*g_neg_zero), type, mk_add_group(type), args[2],
prf.second});
return pair<expr, expr>(prf.first, rprf);
}
if (is_neg_app(nval)) {
buffer<expr> nval_args;
get_app_args(nval, nval_args);
expr rprf = mk_cong(mk_app(f, args[0], args[1]), type, args[2], nval_args[2], prf.second);
// std::cout << " RETURNING: (" << nval << ", " << rprf << "\n";
expr rprf = mk_cong(mk_app(f, args[0], args[1]), type, args[2],
nval_args[2], prf.second);
return pair<expr, expr>(nval, rprf);
} else {
expr rprf = mk_app({mk_const(*g_neg_neg), type, mk_add_group(type), args[2], nval, prf.second});
expr rprf = mk_app({mk_const(*g_neg_neg), type, mk_add_group(type),
args[2], nval, prf.second});
return pair<expr, expr>(nval, rprf);
}
} else if (const_name(f) == *g_mul && args.size() == 4) {
@ -920,13 +992,11 @@ pair<expr, expr> norm_num_context::mk_norm(expr const & e) {
expr rprf = mk_app({mk_const(*g_subst_prod), type, mk_has_mul(args[0]), args[2], args[3],
lhs_p.first, rhs_p.first, nval, lhs_p.second, rhs_p.second, prf});
return pair<expr, expr>(nval, rprf);
} else if (const_name(f) == get_division_name() && args.size() == 4) {
} else if (const_name(f) == *g_div && args.size() == 4) {
auto lhs_p = mk_norm(args[2]);
auto rhs_p = mk_norm(args[3]);
//std::cout << "div. lhs, rhs:" << lhs_p.first << ",\n" << rhs_p.first << ".\n";
expr prf;
if (is_div(nval)) {
// std::cout << "nval is div. (" << nval << ")\n";
buffer<expr> nval_args;
get_app_args(nval, nval_args);
expr nval_num = nval_args[2], nval_den = nval_args[3];
@ -934,7 +1004,9 @@ pair<expr, expr> norm_num_context::mk_norm(expr const & e) {
auto rhs_mul = mk_norm(mk_mul(type, nval_num, rhs_p.first));
expr den_nonzero = mk_nonzero_prf(rhs_p.first);
expr nval_den_nonzero = mk_nonzero_prf(nval_den);
prf = mk_app({mk_const(*g_div_eq_div_helper), type, mk_field(type), lhs_p.first, rhs_p.first, nval_num, nval_den, lhs_mul.first, lhs_mul.second, rhs_mul.second, den_nonzero, nval_den_nonzero});
prf = mk_app({mk_const(*g_div_eq_div_helper), type, mk_field(type),
lhs_p.first, rhs_p.first, nval_num, nval_den, lhs_mul.first,
lhs_mul.second, rhs_mul.second, den_nonzero, nval_den_nonzero});
} else {
auto prod = mk_norm(mk_mul(type, nval, rhs_p.first));
auto val1 = to_mpq(prod.first), val2 = to_mpq(lhs_p.first);
@ -942,9 +1014,12 @@ pair<expr, expr> norm_num_context::mk_norm(expr const & e) {
lean_assert(*val1 == *val2);
}
expr den_nonzero = mk_nonzero_prf(rhs_p.first);
prf = mk_app({mk_const(*g_div_helper), type, mk_field(type), lhs_p.first, rhs_p.first, nval, den_nonzero, prod.second});
prf = mk_app({mk_const(*g_div_helper), type, mk_field(type),
lhs_p.first, rhs_p.first, nval, den_nonzero, prod.second});
}
expr rprf = mk_app({mk_const(*g_subst_div), type, mk_has_div(type), lhs_p.first, rhs_p.first, args[2], args[3], nval, prf, lhs_p.second, rhs_p.second});
expr rprf = mk_app({mk_const(*g_subst_div), type, mk_has_div(type),
lhs_p.first, rhs_p.first, args[2], args[3], nval, prf,
lhs_p.second, rhs_p.second});
return pair<expr, expr>(nval, rprf);
} else if (const_name(f) == get_bit0_name() && args.size() == 3) {
lean_assert(is_bit0(nval));
@ -958,96 +1033,96 @@ pair<expr, expr> norm_num_context::mk_norm(expr const & e) {
buffer<expr> nval_args;
get_app_args(nval, nval_args);
auto prf = mk_norm(args[3]);
auto rprf = mk_cong(mk_app(f, args[0], args[1], args[2]), type, args[3], nval_args[3], prf.second);
auto rprf = mk_cong(mk_app(f, args[0], args[1], args[2]), type, args[3],
nval_args[3], prf.second);
return pair<expr, expr>(nval, rprf);
} else if ((const_name(f) == get_zero_name() || const_name(f) == get_one_name()) && args.size() == 2) {
auto p = pair<expr, expr>(e, mk_app({mk_const(*g_mk_eq), args[0], e}));
// return pair<expr, expr>(e, mk_app({mk_const(*g_mk_eq), args[0], e}));
return p;
} else if ((const_name(f) == get_zero_name() || const_name(f) == get_one_name())
&& args.size() == 2) {
return pair<expr, expr>(e, mk_app({mk_const(*g_mk_eq), args[0], e}));
} else {
std::cout << "error with name " << const_name(f) << " and size " << args.size() << ".\n";
throw exception("mk_norm found unrecognized combo ");
}
}
void initialize_norm_num() {
g_add = new name("add");
g_add1 = new name("add1");
g_mul = new name("mul");
g_sub = new name("sub");
g_neg = new name("neg");
g_div = new name("division");
g_bit0_add_bit0 = new name("bit0_add_bit0_helper");
g_bit1_add_bit0 = new name("bit1_add_bit0_helper");
g_bit0_add_bit1 = new name("bit0_add_bit1_helper");
g_bit1_add_bit1 = new name("bit1_add_bit1_helper");
g_bin_add_0 = new name("bin_add_zero");
g_bin_0_add = new name("bin_zero_add");
g_bin_add_1 = new name("bin_add_one");
g_1_add_bit0 = new name("one_add_bit0");
g_bit0_add_1 = new name("bit0_add_one");
g_bit1_add_1 = new name("bit1_add_one_helper");
g_1_add_bit1 = new name("one_add_bit1_helper");
g_one_add_one = new name("one_add_one");
g_add1_bit0 = new name("add1_bit0");
g_add1_bit1 = new name("add1_bit1_helper");
g_add1_zero = new name("add1_zero");
g_add1_one = new name("add1_one");
g_subst_sum = new name("subst_into_sum");
g_subst_subtr = new name("subst_into_subtr");
g_subst_prod = new name("subst_into_prod");
g_mk_cong = new name("mk_cong");
g_mk_eq = new name("mk_eq");
g_zero_mul = new name("zero_mul");
g_mul_zero = new name("mul_zero");
g_mul_one = new name("mul_one");
g_mul_bit0 = new name("mul_bit0_helper");
g_mul_bit1 = new name("mul_bit1_helper");
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("algebra", "add_monoid");
g_ring = new name("algebra", "ring");
g_add_monoid = new name("algebra", "add_monoid");
g_ring = new name("algebra", "ring");
g_monoid = new name("algebra", "monoid");
g_add_comm = new name("algebra", "add_comm_semigroup");
g_add_group = new name("algebra", "add_group");
g_mul_zero_class = new name("algebra", "mul_zero_class");
g_add_group = new name("algebra", "add_group");
g_mul_zero_class= new name("algebra", "mul_zero_class");
g_distrib = new name("algebra", "distrib");
g_has_neg = new name("has_neg"); //"algebra",
g_has_neg = new name("has_neg");
g_has_sub = new name("has_sub");
g_has_div = new name("has_division");
g_has_div = new name("has_div");
g_semiring = new name("algebra", "semiring");
g_lin_ord_ring = new name("algebra", "linear_ordered_ring");
g_lin_ord_semiring = new name("algebra", "linear_ordered_semiring");
g_lin_ord_ring = new name("algebra", "linear_ordered_ring");
g_lin_ord_semiring = new name("algebra", "linear_ordered_semiring");
g_eq_neg_of_add_eq_zero = new name("algebra", "eq_neg_of_add_eq_zero");
g_neg_add_neg_eq = new name("neg_add_neg_helper");
g_neg_add_pos1 = new name("neg_add_pos_helper1");
g_neg_add_pos2 = new name("neg_add_pos_helper2");
g_pos_add_neg = new name("pos_add_neg_helper");
g_neg_mul_neg = new name("neg_mul_neg_helper");
g_neg_mul_pos = new name("neg_mul_pos_helper");
g_pos_mul_neg = new name("pos_mul_neg_helper");
g_sub_eq_add_neg = new name("sub_eq_add_neg_helper");
g_pos_add_pos = new name("pos_add_pos_helper");
g_neg_neg = new name("neg_neg_helper");
g_add_comm_group = new name("algebra", "add_comm_group");
g_add_div = new name("add_div_helper");
g_div_add = new name("div_add_helper");
g_bit0_nonneg = new name("nonneg_bit0_helper");
g_bit1_nonneg = new name("nonneg_bit1_helper");
g_zero_le_one = new name("algebra", "zero_le_one");
g_le_refl = new name("algebra", "le.refl");
g_bit0_pos = new name("pos_bit0_helper");
g_bit1_pos = new name("pos_bit1_helper");
g_zero_lt_one = new name("algebra", "zero_lt_one");
g_wk_order = new name("algebra", "weak_order");
g_field = new name("algebra", "field");
g_nonzero_neg = new name("nonzero_of_neg_helper");
g_nonzero_pos = new name("nonzero_of_pos_helper");
g_mul_div = new name("mul_div_helper");
g_div_mul = new name("div_mul_helper");
g_div_helper = new name("div_helper");
g_div_eq_div_helper = new name("div_eq_div_helper");
g_subst_div = new name("subst_into_div");
g_nonzero_div = new name("nonzero_of_div_helper");
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("algebra", "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("algebra", "zero_le_one");
g_le_refl = new name("algebra", "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("algebra", "zero_lt_one");
g_wk_order = new name("algebra", "weak_order");
g_field = new name("algebra", "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() {
@ -1122,5 +1197,6 @@ void finalize_norm_num() {
delete g_div_eq_div_helper;
delete g_mul_div;
delete g_nonzero_div;
delete g_neg_zero;
}
}

19
src/library/norm_num.h
View file

@ -9,8 +9,17 @@ Author: Robert Y. Lewis
#include "library/num.h"
#include "library/class_instance_resolution.h"
#include "util/numerics/mpq.h"
#include <unordered_map>
#include <string>
namespace lean {
struct hash_name {
size_t operator() (const name &n) const {
return std::hash<std::string>()(n.to_string());
}
};
class norm_num_context {
environment m_env;
local_context m_ctx;
@ -18,8 +27,6 @@ class norm_num_context {
pair<expr, expr> mk_norm_add(expr const &, expr const &);
pair<expr, expr> mk_norm_add1(expr const &);
pair<expr, expr> mk_norm_mul(expr const &, expr const &);
pair<expr, expr> mk_norm_div(expr const &, expr const &);
pair<expr, expr> mk_norm_sub(expr const &, expr const &);
expr mk_const(name const & n);
expr mk_cong(expr const &, expr const &, expr const &, expr const &, expr const &);
expr mk_has_add(expr const &);
@ -48,7 +55,7 @@ class norm_num_context {
expr mk_add_comm_group(expr const &);
expr mk_pos_prf(expr const &);
expr mk_nonneg_prf(expr const &);
expr mk_norm_eq_neg_add_neg(expr &,expr &,expr &);
expr mk_norm_eq_neg_add_neg(expr &, expr &, expr &);
expr mk_norm_eq_neg_add_pos(expr &, expr &, expr &);
expr mk_norm_eq_pos_add_neg(expr &, expr &, expr &);
expr mk_norm_eq_pos_add_pos(expr &, expr &, expr &);
@ -56,16 +63,13 @@ class norm_num_context {
expr mk_norm_eq_neg_mul_pos(expr &, expr &, expr &);
expr mk_norm_eq_pos_mul_neg(expr &, expr &, expr &);
expr mk_norm_eq_pos_mul_pos(expr &, expr &, expr &);
//pair<expr, expr> mk_norm_div_over_div(expr &, expr &);
//pair<expr, expr> mk_norm_div_over_num(expr &, expr &);
//pair<expr, expr> mk_norm_num_over_div(expr &, expr &);
//pair<expr, expr> mk_norm_num_over_num(expr &, expr &);
expr mk_norm_div_add(expr &, expr &, expr &);
expr mk_norm_add_div(expr &, expr &, expr &);
expr mk_norm_div_mul(expr &, expr &, expr &);
expr mk_norm_mul_div(expr &, expr &, expr &);
expr mk_nonzero_prf(expr const & e);
pair<expr, expr> get_type_and_arg_of_neg(expr &);
std::unordered_map<name, expr, hash_name> instances;
public:
norm_num_context(environment const & env, local_context const & ctx):m_env(env), m_ctx(ctx) {}
@ -74,7 +78,6 @@ public:
bool is_neg_app(expr const &) const;
bool is_div(expr const &) const;
pair<expr, expr> mk_norm(expr const & e);
//pair<expr, expr> mk_norm_expr(expr const & e);
expr mk_norm_eq(expr const &, expr const &);
mpz num_of_expr(expr const & e);
mpq mpq_of_expr(expr const & e);

7
src/library/tactic/norm_num_tactic.cpp
View file

@ -31,10 +31,8 @@ tactic norm_num_tactic() {
buffer<expr> hyps;
g.get_hyps(hyps);
local_context ctx(to_list(hyps));
//std::cout << "\nnum of lhs: " << mpq_of_expr(env, ctx, lhs) << "\n";
try {
pair<expr, expr> p = mk_norm_num(env, ctx, lhs);
//std::cout << "checkpt 0";
expr new_lhs = p.first;
expr new_lhs_pr = p.second;
pair<expr, expr> p2 = mk_norm_num(env, ctx, rhs);
@ -42,20 +40,15 @@ tactic norm_num_tactic() {
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);
if (v_lhs == v_rhs) {
// std::cout << "checkpt 1\n";
type_checker tc(env);
//std::cout << "checkpt 2: " << new_lhs_pr << ", \n" << new_rhs_pr << "\n";
expr g_prf = mk_trans(tc, new_lhs_pr, mk_symm(tc, new_rhs_pr));
//std::cout << "checkpt 3\n";
substitution new_subst = s.get_subst();
assign(new_subst, g, g_prf);
return some_proof_state(proof_state(s, tail(gs), new_subst));
} else {
std::cout << "lhs: " << new_lhs << ", rhs: " << new_rhs << "\n";
throw_tactic_exception_if_enabled(s, "norm_num tactic failed, lhs doesn't match rhs");
return none_proof_state();
}
} catch (exception & ex) {
throw_tactic_exception_if_enabled(s, ex.what());
return none_proof_state();

87
tests/lean/extra/num_norm1.lean
View file

@ -1,9 +1,12 @@
import algebra.numeral algebra.field data.nat
open algebra
import algebra.numeral data.real
open algebra real
/-
variable {A : Type}
variable [s : linear_ordered_field A]
include s
include s-/
notation `A` := real
example : (-1 :A) * 1 = -1 := by norm_num
example : (-2 :A) * 1 = -2 := by norm_num
@ -78,3 +81,81 @@ example : (0 : A) / 3 = 0 := by norm_num
example : (9 * 9 * 9) * (12 : A) / 27 = 81 * (2 + 2) := by norm_num
example : (-2 : A) * 4 / 3 = -8 / 3 := by norm_num
example : - (-4 / 3) = 1 / (3 / (4 : A)) := by norm_num
-- auto gen tests
example : ((25 * (1 / 1)) + (30 - 16)) = (39 : A) := by norm_num
example : ((19 * (- 2 - 3)) / 6) = (-95/6 : A) := by norm_num
example : - (3 * 28) = (-84 : A) := by norm_num
example : - - (16 / ((11 / (- - (6 * 19) + 12)) * 21)) = (96/11 : A) := by norm_num
example : (- (- 21 + 24) - - (- - (28 + (- 21 / - (16 / ((1 * 26) * ((0 * - 11) + 13))))) * 21)) = (79209/8 : A) := by norm_num
example : (27 * (((16 + - (12 + 4)) + (22 - - 19)) - 23)) = (486 : A) := by norm_num
example : - (13 * (- 30 / ((7 / 24) + - 7))) = (-9360/161 : A) := by norm_num
example : - (0 + 20) = (-20 : A) := by norm_num
example : (- 2 - (27 + (((2 / 14) - (7 + 21)) + (16 - - - 14)))) = (-22/7 : A) := by norm_num
example : (25 + ((8 - 2) + 16)) = (47 : A) := by norm_num
example : (- - 26 / 27) = (26/27 : A) := by norm_num
example : ((((16 * (22 / 14)) - 18) / 11) + 30) = (2360/77 : A) := by norm_num
example : (((- 28 * 28) / (29 - 24)) * 24) = (-18816/5 : A) := by norm_num
example : ((- (18 - ((- - (10 + - 2) - - (23 / 5)) / 5)) - (21 * 22)) - (((20 / - ((((19 + 18) + 15) + 3) + - 22)) + 14) / 17)) = (-394571/825 : A) := by norm_num
example : ((3 + 25) - - 4) = (32 : A) := by norm_num
example : ((1 - 0) - 22) = (-21 : A) := by norm_num
example : (((- (8 / 7) / 14) + 20) + 22) = (2054/49 : A) := by norm_num
example : ((21 / 20) - 29) = (-559/20 : A) := by norm_num
example : - - 20 = (20 : A) := by norm_num
example : (24 - (- 9 / 4)) = (105/4 : A) := by norm_num
example : (((7 / ((23 * 19) + (27 * 10))) - ((28 - - 15) * 24)) + (9 / - (10 * - 3))) = (-1042007/1010 : A) := by norm_num
example : (26 - (- 29 + (12 / 25))) = (1363/25 : A) := by norm_num
example : ((11 * 27) / (4 - 5)) = (-297 : A) := by norm_num
example : (24 - (9 + 15)) = (0 : A) := by norm_num
example : (- 9 - - 0) = (-9 : A) := by norm_num
example : (- 10 / (30 + 10)) = (-1/4 : A) := by norm_num
example : (22 - (6 * (28 * - 8))) = (1366 : A) := by norm_num
example : ((- - 2 * (9 * - 3)) + (22 / 30)) = (-799/15 : A) := by norm_num
example : - (26 / ((3 + 7) / - (27 * (12 / - 16)))) = (-1053/20 : A) := by norm_num
example : ((- 29 / 1) + 28) = (-1 : A) := by norm_num
example : ((21 * ((10 - (((17 + 28) - - 0) + 20)) + 26)) + ((17 + - 16) * 7)) = (-602 : A) := by norm_num
example : (((- 5 - ((24 + - - 8) + 3)) + 20) + - 23) = (-43 : A) := by norm_num
example : ((- ((14 - 15) * (14 + 8)) + ((- (18 - 27) - 0) + 12)) - 11) = (32 : A) := by norm_num
example : (((15 / 17) * (26 / 27)) + 28) = (4414/153 : A) := by norm_num
example : (14 - ((- 16 - 3) * - (20 * 19))) = (-7206 : A) := by norm_num
example : (21 - - - (28 - (12 * 11))) = (125 : A) := by norm_num
example : ((0 + (7 + (25 + 8))) * - (11 * 27)) = (-11880 : A) := by norm_num
example : (19 * - 5) = (-95 : A) := by norm_num
example : (29 * - 8) = (-232 : A) := by norm_num
example : ((22 / 9) - 29) = (-239/9 : A) := by norm_num
example : (3 + (19 / 12)) = (55/12 : A) := by norm_num
example : - (13 + 30) = (-43 : A) := by norm_num
example : - - - (((21 * - - ((- 25 - (- (30 - 5) / (- 5 - 5))) / (((6 + ((25 * - 13) + 22)) - 3) / 2))) / (- 3 / 10)) * (- 8 - 0)) = (-308/3 : A) := by norm_num
example : - (2 * - (- 24 * 22)) = (-1056 : A) := by norm_num
example : - - (((28 / - ((- 13 * - 5) / - (((7 - 30) / 16) + 6))) * 0) - 24) = (-24 : A) := by norm_num
example : ((13 + 24) - (27 / (21 * 13))) = (3358/91 : A) := by norm_num
example : ((3 / - 21) * 25) = (-25/7 : A) := by norm_num
example : (17 - (29 - 18)) = (6 : A) := by norm_num
example : ((28 / 20) * 15) = (21 : A) := by norm_num
example : ((((26 * (- (23 - 13) - 3)) / 20) / (14 - (10 + 20))) / ((16 / 6) / (16 * - (3 / 28)))) = (-1521/2240 : A) := by norm_num
example : (46 / (- ((- 17 * 28) - 77) + 87)) = (23/320 : A) := by norm_num
example : (73 * - (67 - (74 * - - 11))) = (54531 : A) := by norm_num
example : ((8 * (25 / 9)) + 59) = (731/9 : A) := by norm_num
example : - ((59 + 85) * - 70) = (10080 : A) := by norm_num
example : (66 + (70 * 58)) = (4126 : A) := by norm_num
example : (- - 49 * 0) = (0 : A) := by norm_num
example : ((- 78 - 69) * 9) = (-1323 : A) := by norm_num
example : - - (7 - - (50 * 79)) = (3957 : A) := by norm_num
example : - (85 * (((4 * 93) * 19) * - 31)) = (18624180 : A) := by norm_num
example : (21 + (- 5 / ((74 * 85) / 45))) = (26373/1258 : A) := by norm_num
example : (42 - ((27 + 64) + 26)) = (-75 : A) := by norm_num
example : (- ((38 - - 17) + 86) - (74 + 58)) = (-273 : A) := by norm_num
example : ((29 * - (75 + - 68)) + (- 41 / 28)) = (-5725/28 : A) := by norm_num
example : (- - (40 - 11) - (68 * 86)) = (-5819 : A) := by norm_num
example : (6 + ((65 - 14) + - 89)) = (-32 : A) := by norm_num
example : (97 * - (29 * 35)) = (-98455 : A) := by norm_num
example : - (66 / 33) = (-2 : A) := by norm_num
example : - ((94 * 89) + (79 - (23 - (((- 1 / 55) + 95) * (28 - (54 / - - - 22)))))) = (-1369070/121 : A) := by norm_num
example : (- 23 + 61) = (38 : A) := by norm_num
example : - (93 / 69) = (-31/23 : A) := by norm_num
example : (- - ((68 / (39 + (((45 * - (59 - (37 + 35))) / (53 - 75)) - - (100 + - (50 / (- 30 - 59)))))) - (69 - (23 * 30))) / (57 + 17)) = (137496481/16368578 : A) := by norm_num
example : (- 19 * - - (75 * - - 41)) = (-58425 : A) := by norm_num
example : ((3 / ((- 28 * 45) * (19 + ((- (- 88 - (- (- 1 + 90) + 8)) + 87) * 48)))) + 1) = (1903019/1903020 : A) := by norm_num
example : ((- - (28 + 48) / 75) + ((- 59 - 14) - 0)) = (-5399/75 : A) := by norm_num
example : (- ((- (((66 - 86) - 36) / 94) - 3) / - - (77 / (56 - - - 79))) + 87) = (312254/3619 : A) := by norm_num