From f4b1413cee697c7e2078179e0034f4ad9fe3d905 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 22 Nov 2016 15:14:10 -0800 Subject: [PATCH] feat(library/comp_val): add mk_nat_val_lt_proof and mk_nat_val_le_proof --- src/library/comp_val.cpp | 55 +++++++++++++++++++++++++++++++++------ src/library/comp_val.h | 13 ++++++++- src/library/constants.cpp | 44 +++++++++++++++++++++++++++++++ src/library/constants.h | 11 ++++++++ src/library/constants.txt | 11 ++++++++ 5 files changed, 125 insertions(+), 9 deletions(-) diff --git a/src/library/comp_val.cpp b/src/library/comp_val.cpp index a1dd59321c..460c8c686e 100644 --- a/src/library/comp_val.cpp +++ b/src/library/comp_val.cpp @@ -9,13 +9,6 @@ Author: Leonardo de Moura #include "library/constants.h" namespace lean { -optional is_nat_succ(expr const & e) { - if (is_app_of(e, get_nat_succ_name(), 1)) - return some_expr(app_arg(e)); - else - return none_expr(); -} - optional mk_nat_val_ne_proof(expr const & a, expr const & b) { if (a == b) return none_expr(); if (auto a1 = is_bit0(a)) { @@ -57,7 +50,7 @@ optional mk_nat_val_ne_proof(expr const & a, expr const & b) { if (auto b1 = is_bit0(b)) { return some_expr(mk_app(mk_constant(get_nat_one_ne_bit0_name()), *b1)); } else if (auto b1 = is_bit1(b)) { - if (auto pr = mk_nat_val_ne_proof(*b1, mk_nat_one())) + if (auto pr = mk_nat_val_ne_proof(*b1, mk_nat_zero())) return some_expr(mk_app(mk_constant(get_nat_one_ne_bit1_name()), *b1, *pr)); } else if (is_zero(b)) { return some_expr(mk_constant(get_nat_one_ne_zero_name())); @@ -67,4 +60,50 @@ optional mk_nat_val_ne_proof(expr const & a, expr const & b) { } return none_expr(); } + +optional mk_nat_val_lt_proof(expr const & a, expr const & b) { + if (a == b) return none_expr(); + if (auto a1 = is_bit0(a)) { + if (auto b1 = is_bit0(b)) { + if (auto pr = mk_nat_val_lt_proof(*a1, *b1)) + return some_expr(mk_app(mk_constant(get_nat_bit0_lt_name()), *a1, *b1, *pr)); + } else if (auto b1 = is_bit1(b)) { + if (auto pr = mk_nat_val_lt_proof(*a1, *b1)) + return some_expr(mk_app(mk_constant(get_nat_bit0_lt_bit1_name()), *a1, *b1, *pr)); + } + } else if (auto a1 = is_bit1(a)) { + if (auto b1 = is_bit0(b)) { + if (auto pr = mk_nat_val_lt_proof(*a1, *b1)) + return some_expr(mk_app(mk_constant(get_nat_bit1_lt_bit0_name()), *a1, *b1, *pr)); + } else if (auto b1 = is_bit1(b)) { + if (auto pr = mk_nat_val_lt_proof(*a1, *b1)) + return some_expr(mk_app(mk_constant(get_nat_bit1_lt_name()), *a1, *b1, *pr)); + } + } else if (is_zero(a)) { + if (auto b1 = is_bit0(b)) { + if (auto pr = mk_nat_val_ne_proof(*b1, a)) + return some_expr(mk_app(mk_constant(get_nat_zero_lt_bit0_name()), *b1, *pr)); + } else if (auto b1 = is_bit1(b)) { + return some_expr(mk_app(mk_constant(get_nat_zero_lt_bit1_name()), *b1)); + } else if (is_one(b)) { + return some_expr(mk_constant(get_nat_zero_lt_one_name())); + } + } else if (is_one(a)) { + if (auto b1 = is_bit0(b)) { + if (auto pr = mk_nat_val_ne_proof(*b1, mk_nat_zero())) + return some_expr(mk_app(mk_constant(get_nat_one_lt_bit0_name()), *b1, *pr)); + } else if (auto b1 = is_bit1(b)) { + if (auto pr = mk_nat_val_ne_proof(*b1, mk_nat_zero())) + return some_expr(mk_app(mk_constant(get_nat_one_lt_bit1_name()), *b1, *pr)); + } + } +} + +optional mk_nat_val_le_proof(expr const & a, expr const & b) { + if (a == b) + return some_expr(mk_app(mk_constant(get_nat_le_refl_name()), a)); + if (auto pr = mk_nat_val_lt_proof(a, b)) + return some_expr(mk_app(mk_constant(get_nat_le_of_lt_name()), a, b, *pr)); + return none_expr(); +} } diff --git a/src/library/comp_val.h b/src/library/comp_val.h index c148e402a2..a346824c92 100644 --- a/src/library/comp_val.h +++ b/src/library/comp_val.h @@ -14,6 +14,17 @@ namespace lean { \remark This function assumes 'a' and 'b' have type nat. \remark A natural number value is any expression built using - bit0, bit1, zero, one, nat.succ and nat.zero */ + bit0, bit1, zero, one and nat.zero */ optional mk_nat_val_ne_proof(expr const & a, expr const & b); + +/** \brief If 'a' and 'b' are two natural number values s.t. a < b, + then return a proof for a < b. Otherwise return none. + + \remark This function assumes 'a' and 'b' have type nat. + + \remark A natural number value is any expression built using + bit0, bit1, zero, one and nat.zero */ +optional mk_nat_val_lt_proof(expr const & a, expr const & b); +/* Same for a <= b */ +optional mk_nat_val_le_proof(expr const & a, expr const & b); } diff --git a/src/library/constants.cpp b/src/library/constants.cpp index 25f9c13c22..d77427d1d4 100644 --- a/src/library/constants.cpp +++ b/src/library/constants.cpp @@ -213,6 +213,17 @@ name const * g_nat_zero_ne_bit1 = nullptr; name const * g_nat_one_ne_zero = nullptr; name const * g_nat_one_ne_bit0 = nullptr; name const * g_nat_one_ne_bit1 = nullptr; +name const * g_nat_bit0_lt = nullptr; +name const * g_nat_bit1_lt = nullptr; +name const * g_nat_bit0_lt_bit1 = nullptr; +name const * g_nat_bit1_lt_bit0 = nullptr; +name const * g_nat_zero_lt_one = nullptr; +name const * g_nat_zero_lt_bit1 = nullptr; +name const * g_nat_zero_lt_bit0 = nullptr; +name const * g_nat_one_lt_bit0 = nullptr; +name const * g_nat_one_lt_bit1 = nullptr; +name const * g_nat_le_of_lt = nullptr; +name const * g_nat_le_refl = nullptr; name const * g_neg = nullptr; name const * g_norm_num_add1 = nullptr; name const * g_norm_num_add1_bit0 = nullptr; @@ -619,6 +630,17 @@ void initialize_constants() { g_nat_one_ne_zero = new name{"nat", "one_ne_zero"}; g_nat_one_ne_bit0 = new name{"nat", "one_ne_bit0"}; g_nat_one_ne_bit1 = new name{"nat", "one_ne_bit1"}; + g_nat_bit0_lt = new name{"nat", "bit0_lt"}; + g_nat_bit1_lt = new name{"nat", "bit1_lt"}; + g_nat_bit0_lt_bit1 = new name{"nat", "bit0_lt_bit1"}; + g_nat_bit1_lt_bit0 = new name{"nat", "bit1_lt_bit0"}; + g_nat_zero_lt_one = new name{"nat", "zero_lt_one"}; + g_nat_zero_lt_bit1 = new name{"nat", "zero_lt_bit1"}; + g_nat_zero_lt_bit0 = new name{"nat", "zero_lt_bit0"}; + g_nat_one_lt_bit0 = new name{"nat", "one_lt_bit0"}; + g_nat_one_lt_bit1 = new name{"nat", "one_lt_bit1"}; + g_nat_le_of_lt = new name{"nat", "le_of_lt"}; + g_nat_le_refl = new name{"nat", "le_refl"}; g_neg = new name{"neg"}; g_norm_num_add1 = new name{"norm_num", "add1"}; g_norm_num_add1_bit0 = new name{"norm_num", "add1_bit0"}; @@ -1026,6 +1048,17 @@ void finalize_constants() { delete g_nat_one_ne_zero; delete g_nat_one_ne_bit0; delete g_nat_one_ne_bit1; + delete g_nat_bit0_lt; + delete g_nat_bit1_lt; + delete g_nat_bit0_lt_bit1; + delete g_nat_bit1_lt_bit0; + delete g_nat_zero_lt_one; + delete g_nat_zero_lt_bit1; + delete g_nat_zero_lt_bit0; + delete g_nat_one_lt_bit0; + delete g_nat_one_lt_bit1; + delete g_nat_le_of_lt; + delete g_nat_le_refl; delete g_neg; delete g_norm_num_add1; delete g_norm_num_add1_bit0; @@ -1432,6 +1465,17 @@ name const & get_nat_zero_ne_bit1_name() { return *g_nat_zero_ne_bit1; } name const & get_nat_one_ne_zero_name() { return *g_nat_one_ne_zero; } name const & get_nat_one_ne_bit0_name() { return *g_nat_one_ne_bit0; } name const & get_nat_one_ne_bit1_name() { return *g_nat_one_ne_bit1; } +name const & get_nat_bit0_lt_name() { return *g_nat_bit0_lt; } +name const & get_nat_bit1_lt_name() { return *g_nat_bit1_lt; } +name const & get_nat_bit0_lt_bit1_name() { return *g_nat_bit0_lt_bit1; } +name const & get_nat_bit1_lt_bit0_name() { return *g_nat_bit1_lt_bit0; } +name const & get_nat_zero_lt_one_name() { return *g_nat_zero_lt_one; } +name const & get_nat_zero_lt_bit1_name() { return *g_nat_zero_lt_bit1; } +name const & get_nat_zero_lt_bit0_name() { return *g_nat_zero_lt_bit0; } +name const & get_nat_one_lt_bit0_name() { return *g_nat_one_lt_bit0; } +name const & get_nat_one_lt_bit1_name() { return *g_nat_one_lt_bit1; } +name const & get_nat_le_of_lt_name() { return *g_nat_le_of_lt; } +name const & get_nat_le_refl_name() { return *g_nat_le_refl; } name const & get_neg_name() { return *g_neg; } 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; } diff --git a/src/library/constants.h b/src/library/constants.h index 296fec94bf..0321572bdb 100644 --- a/src/library/constants.h +++ b/src/library/constants.h @@ -215,6 +215,17 @@ name const & get_nat_zero_ne_bit1_name(); name const & get_nat_one_ne_zero_name(); name const & get_nat_one_ne_bit0_name(); name const & get_nat_one_ne_bit1_name(); +name const & get_nat_bit0_lt_name(); +name const & get_nat_bit1_lt_name(); +name const & get_nat_bit0_lt_bit1_name(); +name const & get_nat_bit1_lt_bit0_name(); +name const & get_nat_zero_lt_one_name(); +name const & get_nat_zero_lt_bit1_name(); +name const & get_nat_zero_lt_bit0_name(); +name const & get_nat_one_lt_bit0_name(); +name const & get_nat_one_lt_bit1_name(); +name const & get_nat_le_of_lt_name(); +name const & get_nat_le_refl_name(); name const & get_neg_name(); name const & get_norm_num_add1_name(); name const & get_norm_num_add1_bit0_name(); diff --git a/src/library/constants.txt b/src/library/constants.txt index 8d0c374811..ef40ac9eed 100644 --- a/src/library/constants.txt +++ b/src/library/constants.txt @@ -208,6 +208,17 @@ nat.zero_ne_bit1 nat.one_ne_zero nat.one_ne_bit0 nat.one_ne_bit1 +nat.bit0_lt +nat.bit1_lt +nat.bit0_lt_bit1 +nat.bit1_lt_bit0 +nat.zero_lt_one +nat.zero_lt_bit1 +nat.zero_lt_bit0 +nat.one_lt_bit0 +nat.one_lt_bit1 +nat.le_of_lt +nat.le_refl neg norm_num.add1 norm_num.add1_bit0