From 3238c7e2a063259d333e7ed134eb15cf49d7c487 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 15 Jan 2014 19:53:52 -0800 Subject: [PATCH] feat(library/simplifier): add is_permutation_ceq predicate Signed-off-by: Leonardo de Moura --- src/library/simplifier/ceq.cpp | 70 +++++++++++++++++++++ src/library/simplifier/ceq.h | 7 ++- tests/lua/ceq1.lua | 112 +++++++++++++++++---------------- 3 files changed, 133 insertions(+), 56 deletions(-) diff --git a/src/library/simplifier/ceq.cpp b/src/library/simplifier/ceq.cpp index 75dfd8f7c..de62cb6b5 100644 --- a/src/library/simplifier/ceq.cpp +++ b/src/library/simplifier/ceq.cpp @@ -156,6 +156,70 @@ bool is_ceq(ro_environment const & env, expr e) { } } +static bool is_permutation(expr const & lhs, expr const & rhs, unsigned offset, buffer> & p) { + if (lhs.kind() != rhs.kind()) + return false; + switch (lhs.kind()) { + case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: case expr_kind::MetaVar: + return lhs == rhs; + case expr_kind::Var: + if (var_idx(lhs) < offset) { + return lhs == rhs; // locally bound variable + } else if (var_idx(lhs) - offset < p.size()) { + if (p[var_idx(lhs) - offset]) { + return *(p[var_idx(lhs) - offset]) == var_idx(rhs); + } else { + p[var_idx(lhs) - offset] = var_idx(rhs); + return true; + } + } else { + return lhs == rhs; // free variable + } + case expr_kind::Lambda: case expr_kind::Pi: + return + is_permutation(abst_domain(lhs), abst_domain(rhs), offset, p) && + is_permutation(abst_body(lhs), abst_body(rhs), offset+1, p); + case expr_kind::HEq: + return + is_permutation(heq_lhs(lhs), heq_lhs(rhs), offset, p) && + is_permutation(heq_rhs(lhs), heq_rhs(rhs), offset, p); + case expr_kind::App: + if (num_args(lhs) == num_args(rhs)) { + for (unsigned i = 0; i < num_args(lhs); i++) { + if (!is_permutation(arg(lhs, i), arg(rhs, i), offset, p)) + return false; + } + return true; + } else { + return false; + } + case expr_kind::Let: + if (static_cast(let_type(lhs)) != static_cast(let_type(rhs))) + return false; + if (static_cast(let_type(lhs)) && !is_permutation(*let_type(lhs), *let_type(rhs), offset, p)) + return false; + return + is_permutation(let_value(lhs), let_value(rhs), offset, p) && + is_permutation(let_body(lhs), let_value(rhs), offset+1, p); + } + lean_unreachable(); +} + +bool is_permutation_ceq(expr e) { + unsigned num_args = 0; + while (is_pi(e)) { + e = abst_body(e); + num_args++; + } + if (!is_eq(e)) + return false; + expr lhs = arg(e, 2); + expr rhs = arg(e, 3); + buffer> permutation; + permutation.resize(num_args); + return is_permutation(lhs, rhs, 0, permutation); +} + static int to_ceqs(lua_State * L) { ro_shared_environment env(L, 1); auto r = to_ceqs(env, to_expr(L, 2), to_expr(L, 3)); @@ -179,8 +243,14 @@ static int is_ceq(lua_State * L) { return 1; } +static int is_permutation_ceq(lua_State * L) { + lua_pushboolean(L, is_permutation_ceq(to_expr(L, 1))); + return 1; +} + void open_ceq(lua_State * L) { SET_GLOBAL_FUN(to_ceqs, "to_ceqs"); SET_GLOBAL_FUN(is_ceq, "is_ceq"); + SET_GLOBAL_FUN(is_permutation_ceq, "is_permutation_ceq"); } } diff --git a/src/library/simplifier/ceq.h b/src/library/simplifier/ceq.h index 01adbe95a..ac4527ae5 100644 --- a/src/library/simplifier/ceq.h +++ b/src/library/simplifier/ceq.h @@ -41,7 +41,10 @@ list to_ceqs(ro_environment const & env, expr const & e, expr const & when \c A is not a proposition. */ bool is_ceq(ro_environment const & env, expr e); +/** + \brief Return true iff the lhs is identical to the rhs modulo a + permutation of the conditional equation arguments. +*/ +bool is_permutation_ceq(expr e); void open_ceq(lua_State * L); } - - diff --git a/tests/lua/ceq1.lua b/tests/lua/ceq1.lua index dcedf3ca6..fce48baac 100644 --- a/tests/lua/ceq1.lua +++ b/tests/lua/ceq1.lua @@ -3,17 +3,22 @@ assert(env:find_object("neq_elim")) function show_ceqs(ceqs) for i = 1, #ceqs do - print(ceqs[i][1], ceqs[i][2]) + print(ceqs[i][1], ceqs[i][2], is_permutation_ceq(ceqs[i][1])) env:type_check(ceqs[i][2]) assert(is_ceq(env, ceqs[i][1])) end end -function test_ceq(name, expected) +function test_ceq(name, expected, is_perm) local obj = env:find_object(name) local r = to_ceqs(env, obj:get_type(), Const(name)) show_ceqs(r) assert(#r == expected) + if is_perm ~= nil then + for i = 1, #r do + assert(is_permutation_ceq(r[i][1]) == is_perm) + end + end end parse_lean_cmds([[ @@ -35,55 +40,54 @@ test_ceq("Ax4", 0) test_ceq("Ax5", 1) test_ceq("Ax6", 1) test_ceq("eta", 1) -test_ceq("not_not_eq", 1) -test_ceq("or_comm", 1) -test_ceq("or_assoc", 1) -test_ceq("or_id", 1) -test_ceq("or_falsel", 1) -test_ceq("or_falser", 1) -test_ceq("or_truel", 1) -test_ceq("or_truer", 1) -test_ceq("or_tauto", 1) -test_ceq("and_comm", 1) -test_ceq("and_assoc", 1) -test_ceq("and_id", 1) -test_ceq("and_falsel", 1) -test_ceq("and_falser", 1) -test_ceq("and_truel", 1) -test_ceq("and_truer", 1) -test_ceq("and_absurd", 1) -test_ceq("imp_truer", 1) -test_ceq("imp_truel", 1) -test_ceq("imp_falser", 1) -test_ceq("imp_falsel", 1) -test_ceq("not_and", 1) -test_ceq("not_or", 1) -test_ceq("not_iff", 1) -test_ceq("not_implies", 1) -test_ceq("or_left_comm", 1) -test_ceq("and_left_comm", 1) -test_ceq("forall_or_distributer", 1) -test_ceq("forall_or_distributel", 1) -test_ceq("forall_and_distribute", 1) -test_ceq("exists_and_distributer", 1) -test_ceq("exists_and_distributel", 1) -test_ceq("exists_or_distribute", 1) -test_ceq({"Nat", "add_zeror"}, 1) -test_ceq({"Nat", "add_zerol"}, 1) -test_ceq({"Nat", "add_comm"}, 1) -test_ceq({"Nat", "add_assoc"}, 1) -test_ceq({"Nat", "mul_zerol"}, 1) -test_ceq({"Nat", "mul_zeror"}, 1) -test_ceq({"Nat", "mul_onel"}, 1) -test_ceq({"Nat", "mul_oner"}, 1) -test_ceq({"Nat", "mul_comm"}, 1) -test_ceq({"Nat", "mul_assoc"}, 1) -test_ceq({"Nat", "add_comm"}, 1) -test_ceq({"Nat", "add_assoc"}, 1) -test_ceq({"Nat", "distributer"}, 1) -test_ceq({"Nat", "distributel"}, 1) -test_ceq({"Nat", "le_refl"}, 1) -test_ceq({"Nat", "le_zero"}, 1) -test_ceq({"Nat", "not_lt_0"}, 1) -test_ceq({"Nat", "lt_nrefl"}, 1) - +test_ceq("not_not_eq", 1, false) +test_ceq("or_comm", 1, true) +test_ceq("or_assoc", 1, false) +test_ceq("or_id", 1, false) +test_ceq("or_falsel", 1, false) +test_ceq("or_falser", 1, false) +test_ceq("or_truel", 1, false) +test_ceq("or_truer", 1, false) +test_ceq("or_tauto", 1, false) +test_ceq("and_comm", 1, true) +test_ceq("and_assoc", 1, false) +test_ceq("and_id", 1, false) +test_ceq("and_falsel", 1, false) +test_ceq("and_falser", 1, false) +test_ceq("and_truel", 1, false) +test_ceq("and_truer", 1, false) +test_ceq("and_absurd", 1, false) +test_ceq("imp_truer", 1, false) +test_ceq("imp_truel", 1, false) +test_ceq("imp_falser", 1, false) +test_ceq("imp_falsel", 1, false) +test_ceq("not_and", 1, false) +test_ceq("not_or", 1, false) +test_ceq("not_iff", 1, false) +test_ceq("not_implies", 1, false) +test_ceq("or_left_comm", 1, true) +test_ceq("and_left_comm", 1, true) +test_ceq("forall_or_distributer", 1, false) +test_ceq("forall_or_distributel", 1, false) +test_ceq("forall_and_distribute", 1, false) +test_ceq("exists_and_distributer", 1, false) +test_ceq("exists_and_distributel", 1, false) +test_ceq("exists_or_distribute", 1, false) +test_ceq({"Nat", "add_zeror"}, 1, false) +test_ceq({"Nat", "add_zerol"}, 1, false) +test_ceq({"Nat", "add_comm"}, 1 , true) +test_ceq({"Nat", "add_assoc"}, 1, false) +test_ceq({"Nat", "mul_zerol"}, 1, false) +test_ceq({"Nat", "mul_zeror"}, 1, false) +test_ceq({"Nat", "mul_onel"}, 1, false) +test_ceq({"Nat", "mul_oner"}, 1, false) +test_ceq({"Nat", "mul_comm"}, 1, true) +test_ceq({"Nat", "mul_assoc"}, 1, false) +test_ceq({"Nat", "add_comm"}, 1, true) +test_ceq({"Nat", "add_assoc"}, 1, false) +test_ceq({"Nat", "distributer"}, 1, false) +test_ceq({"Nat", "distributel"}, 1, false) +test_ceq({"Nat", "le_refl"}, 1, false) +test_ceq({"Nat", "le_zero"}, 1, false) +test_ceq({"Nat", "not_lt_0"}, 1, false) +test_ceq({"Nat", "lt_nrefl"}, 1, false)