max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(library/comp_val): add mk_nat_val_lt_proof and mk_nat_val_le_proof

Browse source
This commit is contained in:
Leonardo de Moura 2016-11-22 15:14:10 -08:00
parent 207bc0ecad
commit f4b1413cee
5 changed files with 125 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

55
src/library/comp_val.cpp
View file

@ -9,13 +9,6 @@ Author: Leonardo de Moura
#include "library/constants.h"
namespace lean {
optional<expr> 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<expr> 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<expr> 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<expr> mk_nat_val_ne_proof(expr const & a, expr const & b) {
}
return none_expr();
}
optional<expr> 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<expr> 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();
}
}

13
src/library/comp_val.h
View file

@ -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<expr> 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<expr> mk_nat_val_lt_proof(expr const & a, expr const & b);
/* Same for a <= b */
optional<expr> mk_nat_val_le_proof(expr const & a, expr const & b);
}

44
src/library/constants.cpp
View file

@ -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; }

11
src/library/constants.h
View file

@ -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();

11
src/library/constants.txt
View file

@ -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