From dbc100cc2e508953a64da323bc9667008117615a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 23 Jan 2014 17:28:14 -0800 Subject: [PATCH] feat(library/simplifier): cast elimination in the simplifier Signed-off-by: Leonardo de Moura --- src/builtin/CMakeLists.txt | 3 +- src/builtin/lean2h.lean | 2 +- src/kernel/kernel.h | 2 +- src/kernel/kernel_decls.h | 18 +++++----- src/library/CMakeLists.txt | 2 +- src/library/arith/Int_decls.h | 20 +++++------ src/library/arith/Nat_decls.h | 8 ++--- src/library/arith/Real_decls.h | 14 ++++---- src/library/cast_decls.cpp | 15 ++++++++ src/library/cast_decls.h | 27 ++++++++++++++ src/library/heq_decls.h | 2 +- src/library/simplifier/simplifier.cpp | 52 ++++++++++++++++++++++++--- tests/lean/simp18.lean | 29 +++++++++++++++ tests/lean/simp18.lean.expected.out | 21 +++++++++++ 14 files changed, 175 insertions(+), 40 deletions(-) create mode 100644 src/library/cast_decls.cpp create mode 100644 src/library/cast_decls.h create mode 100644 tests/lean/simp18.lean create mode 100644 tests/lean/simp18.lean.expected.out diff --git a/src/builtin/CMakeLists.txt b/src/builtin/CMakeLists.txt index c85d1695f..f56537fe9 100644 --- a/src/builtin/CMakeLists.txt +++ b/src/builtin/CMakeLists.txt @@ -101,4 +101,5 @@ update_interface("Nat.olean" "library/arith" "-n") update_interface("Int.olean" "library/arith" "") update_interface("Real.olean" "library/arith" "") update_interface("if_then_else.olean" "library" "") -update_interface("heq.olean" "library" "") \ No newline at end of file +update_interface("heq.olean" "library" "") +update_interface("cast.olean" "library" "") \ No newline at end of file diff --git a/src/builtin/lean2h.lean b/src/builtin/lean2h.lean index d9a226294..6752ce425 100644 --- a/src/builtin/lean2h.lean +++ b/src/builtin/lean2h.lean @@ -41,7 +41,7 @@ name_to_cpp_decl(obj:get_name()) io.write("(expr const & e) { return is_app(e) && is_"); name_to_cpp_decl(obj:get_name()) - print("_fn(arg(e, 0)); }") + print("_fn(arg(e, 0)) && num_args(e) == " .. (arity+1) .. "; }") end if is_fn then io.write("inline expr mk_") diff --git a/src/kernel/kernel.h b/src/kernel/kernel.h index 777fb8a1b..a58b91b9f 100644 --- a/src/kernel/kernel.h +++ b/src/kernel/kernel.h @@ -36,7 +36,7 @@ bool is_false(expr const & e); expr mk_eq_fn(); bool is_eq_fn(expr const & e); inline expr mk_eq(expr const & A, expr const & lhs, expr const & rhs) { return mk_app(mk_eq_fn(), A, lhs, rhs); } -inline bool is_eq(expr const & e) { return is_app(e) && is_eq_fn(arg(e, 0)); } +inline bool is_eq(expr const & e) { return is_app(e) && is_eq_fn(arg(e, 0)) && num_args(e) == 4; } inline expr Implies(expr const & e1, expr const & e2) { return mk_implies(e1, e2); } inline expr And(expr const & e1, expr const & e2) { return mk_and(e1, e2); } diff --git a/src/kernel/kernel_decls.h b/src/kernel/kernel_decls.h index 303ab92f7..459979b38 100644 --- a/src/kernel/kernel_decls.h +++ b/src/kernel/kernel_decls.h @@ -11,35 +11,35 @@ expr mk_Bool(); bool is_Bool(expr const & e); expr mk_not_fn(); bool is_not_fn(expr const & e); -inline bool is_not(expr const & e) { return is_app(e) && is_not_fn(arg(e, 0)); } +inline bool is_not(expr const & e) { return is_app(e) && is_not_fn(arg(e, 0)) && num_args(e) == 2; } inline expr mk_not(expr const & e1) { return mk_app({mk_not_fn(), e1}); } expr mk_or_fn(); bool is_or_fn(expr const & e); -inline bool is_or(expr const & e) { return is_app(e) && is_or_fn(arg(e, 0)); } +inline bool is_or(expr const & e) { return is_app(e) && is_or_fn(arg(e, 0)) && num_args(e) == 3; } inline expr mk_or(expr const & e1, expr const & e2) { return mk_app({mk_or_fn(), e1, e2}); } expr mk_and_fn(); bool is_and_fn(expr const & e); -inline bool is_and(expr const & e) { return is_app(e) && is_and_fn(arg(e, 0)); } +inline bool is_and(expr const & e) { return is_app(e) && is_and_fn(arg(e, 0)) && num_args(e) == 3; } inline expr mk_and(expr const & e1, expr const & e2) { return mk_app({mk_and_fn(), e1, e2}); } expr mk_implies_fn(); bool is_implies_fn(expr const & e); -inline bool is_implies(expr const & e) { return is_app(e) && is_implies_fn(arg(e, 0)); } +inline bool is_implies(expr const & e) { return is_app(e) && is_implies_fn(arg(e, 0)) && num_args(e) == 3; } inline expr mk_implies(expr const & e1, expr const & e2) { return mk_app({mk_implies_fn(), e1, e2}); } expr mk_neq_fn(); bool is_neq_fn(expr const & e); -inline bool is_neq(expr const & e) { return is_app(e) && is_neq_fn(arg(e, 0)); } +inline bool is_neq(expr const & e) { return is_app(e) && is_neq_fn(arg(e, 0)) && num_args(e) == 4; } inline expr mk_neq(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_neq_fn(), e1, e2, e3}); } expr mk_iff_fn(); bool is_iff_fn(expr const & e); -inline bool is_iff(expr const & e) { return is_app(e) && is_iff_fn(arg(e, 0)); } +inline bool is_iff(expr const & e) { return is_app(e) && is_iff_fn(arg(e, 0)) && num_args(e) == 3; } inline expr mk_iff(expr const & e1, expr const & e2) { return mk_app({mk_iff_fn(), e1, e2}); } expr mk_exists_fn(); bool is_exists_fn(expr const & e); -inline bool is_exists(expr const & e) { return is_app(e) && is_exists_fn(arg(e, 0)); } +inline bool is_exists(expr const & e) { return is_app(e) && is_exists_fn(arg(e, 0)) && num_args(e) == 3; } inline expr mk_exists(expr const & e1, expr const & e2) { return mk_app({mk_exists_fn(), e1, e2}); } expr mk_nonempty_fn(); bool is_nonempty_fn(expr const & e); -inline bool is_nonempty(expr const & e) { return is_app(e) && is_nonempty_fn(arg(e, 0)); } +inline bool is_nonempty(expr const & e) { return is_app(e) && is_nonempty_fn(arg(e, 0)) && num_args(e) == 2; } inline expr mk_nonempty(expr const & e1) { return mk_app({mk_nonempty_fn(), e1}); } expr mk_nonempty_intro_fn(); bool is_nonempty_intro_fn(expr const & e); @@ -64,7 +64,7 @@ bool is_allext_fn(expr const & e); inline expr mk_allext_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_allext_fn(), e1, e2, e3, e4}); } expr mk_eps_fn(); bool is_eps_fn(expr const & e); -inline bool is_eps(expr const & e) { return is_app(e) && is_eps_fn(arg(e, 0)); } +inline bool is_eps(expr const & e) { return is_app(e) && is_eps_fn(arg(e, 0)) && num_args(e) == 4; } inline expr mk_eps(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_eps_fn(), e1, e2, e3}); } expr mk_eps_ax_fn(); bool is_eps_ax_fn(expr const & e); diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index cf1b7486a..18d005588 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -1,6 +1,6 @@ add_library(library kernel_bindings.cpp deep_copy.cpp context_to_lambda.cpp placeholder.cpp expr_lt.cpp substitution.cpp fo_unify.cpp bin_op.cpp equality.cpp io_state_stream.cpp printer.cpp - hop_match.cpp ite.cpp heq_decls.cpp) + hop_match.cpp ite.cpp heq_decls.cpp cast_decls.cpp) target_link_libraries(library ${LEAN_LIBS}) diff --git a/src/library/arith/Int_decls.h b/src/library/arith/Int_decls.h index 77b1583e6..985a5bc20 100644 --- a/src/library/arith/Int_decls.h +++ b/src/library/arith/Int_decls.h @@ -9,42 +9,42 @@ expr mk_Int(); bool is_Int(expr const & e); expr mk_Int_ge_fn(); bool is_Int_ge_fn(expr const & e); -inline bool is_Int_ge(expr const & e) { return is_app(e) && is_Int_ge_fn(arg(e, 0)); } +inline bool is_Int_ge(expr const & e) { return is_app(e) && is_Int_ge_fn(arg(e, 0)) && num_args(e) == 3; } inline expr mk_Int_ge(expr const & e1, expr const & e2) { return mk_app({mk_Int_ge_fn(), e1, e2}); } expr mk_Int_lt_fn(); bool is_Int_lt_fn(expr const & e); -inline bool is_Int_lt(expr const & e) { return is_app(e) && is_Int_lt_fn(arg(e, 0)); } +inline bool is_Int_lt(expr const & e) { return is_app(e) && is_Int_lt_fn(arg(e, 0)) && num_args(e) == 3; } inline expr mk_Int_lt(expr const & e1, expr const & e2) { return mk_app({mk_Int_lt_fn(), e1, e2}); } expr mk_Int_gt_fn(); bool is_Int_gt_fn(expr const & e); -inline bool is_Int_gt(expr const & e) { return is_app(e) && is_Int_gt_fn(arg(e, 0)); } +inline bool is_Int_gt(expr const & e) { return is_app(e) && is_Int_gt_fn(arg(e, 0)) && num_args(e) == 3; } inline expr mk_Int_gt(expr const & e1, expr const & e2) { return mk_app({mk_Int_gt_fn(), e1, e2}); } expr mk_Int_sub_fn(); bool is_Int_sub_fn(expr const & e); -inline bool is_Int_sub(expr const & e) { return is_app(e) && is_Int_sub_fn(arg(e, 0)); } +inline bool is_Int_sub(expr const & e) { return is_app(e) && is_Int_sub_fn(arg(e, 0)) && num_args(e) == 3; } inline expr mk_Int_sub(expr const & e1, expr const & e2) { return mk_app({mk_Int_sub_fn(), e1, e2}); } expr mk_Int_neg_fn(); bool is_Int_neg_fn(expr const & e); -inline bool is_Int_neg(expr const & e) { return is_app(e) && is_Int_neg_fn(arg(e, 0)); } +inline bool is_Int_neg(expr const & e) { return is_app(e) && is_Int_neg_fn(arg(e, 0)) && num_args(e) == 2; } inline expr mk_Int_neg(expr const & e1) { return mk_app({mk_Int_neg_fn(), e1}); } expr mk_Int_mod_fn(); bool is_Int_mod_fn(expr const & e); -inline bool is_Int_mod(expr const & e) { return is_app(e) && is_Int_mod_fn(arg(e, 0)); } +inline bool is_Int_mod(expr const & e) { return is_app(e) && is_Int_mod_fn(arg(e, 0)) && num_args(e) == 3; } inline expr mk_Int_mod(expr const & e1, expr const & e2) { return mk_app({mk_Int_mod_fn(), e1, e2}); } expr mk_Int_divides_fn(); bool is_Int_divides_fn(expr const & e); -inline bool is_Int_divides(expr const & e) { return is_app(e) && is_Int_divides_fn(arg(e, 0)); } +inline bool is_Int_divides(expr const & e) { return is_app(e) && is_Int_divides_fn(arg(e, 0)) && num_args(e) == 3; } inline expr mk_Int_divides(expr const & e1, expr const & e2) { return mk_app({mk_Int_divides_fn(), e1, e2}); } expr mk_Int_abs_fn(); bool is_Int_abs_fn(expr const & e); -inline bool is_Int_abs(expr const & e) { return is_app(e) && is_Int_abs_fn(arg(e, 0)); } +inline bool is_Int_abs(expr const & e) { return is_app(e) && is_Int_abs_fn(arg(e, 0)) && num_args(e) == 2; } inline expr mk_Int_abs(expr const & e1) { return mk_app({mk_Int_abs_fn(), e1}); } expr mk_Nat_sub_fn(); bool is_Nat_sub_fn(expr const & e); -inline bool is_Nat_sub(expr const & e) { return is_app(e) && is_Nat_sub_fn(arg(e, 0)); } +inline bool is_Nat_sub(expr const & e) { return is_app(e) && is_Nat_sub_fn(arg(e, 0)) && num_args(e) == 3; } inline expr mk_Nat_sub(expr const & e1, expr const & e2) { return mk_app({mk_Nat_sub_fn(), e1, e2}); } expr mk_Nat_neg_fn(); bool is_Nat_neg_fn(expr const & e); -inline bool is_Nat_neg(expr const & e) { return is_app(e) && is_Nat_neg_fn(arg(e, 0)); } +inline bool is_Nat_neg(expr const & e) { return is_app(e) && is_Nat_neg_fn(arg(e, 0)) && num_args(e) == 2; } inline expr mk_Nat_neg(expr const & e1) { return mk_app({mk_Nat_neg_fn(), e1}); } } diff --git a/src/library/arith/Nat_decls.h b/src/library/arith/Nat_decls.h index 1df8d744a..ee5cedf27 100644 --- a/src/library/arith/Nat_decls.h +++ b/src/library/arith/Nat_decls.h @@ -9,19 +9,19 @@ expr mk_Nat(); bool is_Nat(expr const & e); expr mk_Nat_ge_fn(); bool is_Nat_ge_fn(expr const & e); -inline bool is_Nat_ge(expr const & e) { return is_app(e) && is_Nat_ge_fn(arg(e, 0)); } +inline bool is_Nat_ge(expr const & e) { return is_app(e) && is_Nat_ge_fn(arg(e, 0)) && num_args(e) == 3; } inline expr mk_Nat_ge(expr const & e1, expr const & e2) { return mk_app({mk_Nat_ge_fn(), e1, e2}); } expr mk_Nat_lt_fn(); bool is_Nat_lt_fn(expr const & e); -inline bool is_Nat_lt(expr const & e) { return is_app(e) && is_Nat_lt_fn(arg(e, 0)); } +inline bool is_Nat_lt(expr const & e) { return is_app(e) && is_Nat_lt_fn(arg(e, 0)) && num_args(e) == 3; } inline expr mk_Nat_lt(expr const & e1, expr const & e2) { return mk_app({mk_Nat_lt_fn(), e1, e2}); } expr mk_Nat_gt_fn(); bool is_Nat_gt_fn(expr const & e); -inline bool is_Nat_gt(expr const & e) { return is_app(e) && is_Nat_gt_fn(arg(e, 0)); } +inline bool is_Nat_gt(expr const & e) { return is_app(e) && is_Nat_gt_fn(arg(e, 0)) && num_args(e) == 3; } inline expr mk_Nat_gt(expr const & e1, expr const & e2) { return mk_app({mk_Nat_gt_fn(), e1, e2}); } expr mk_Nat_id_fn(); bool is_Nat_id_fn(expr const & e); -inline bool is_Nat_id(expr const & e) { return is_app(e) && is_Nat_id_fn(arg(e, 0)); } +inline bool is_Nat_id(expr const & e) { return is_app(e) && is_Nat_id_fn(arg(e, 0)) && num_args(e) == 2; } inline expr mk_Nat_id(expr const & e1) { return mk_app({mk_Nat_id_fn(), e1}); } expr mk_Nat_succ_nz_fn(); bool is_Nat_succ_nz_fn(expr const & e); diff --git a/src/library/arith/Real_decls.h b/src/library/arith/Real_decls.h index b792be274..23c2a705d 100644 --- a/src/library/arith/Real_decls.h +++ b/src/library/arith/Real_decls.h @@ -9,30 +9,30 @@ expr mk_Real(); bool is_Real(expr const & e); expr mk_nat_to_real_fn(); bool is_nat_to_real_fn(expr const & e); -inline bool is_nat_to_real(expr const & e) { return is_app(e) && is_nat_to_real_fn(arg(e, 0)); } +inline bool is_nat_to_real(expr const & e) { return is_app(e) && is_nat_to_real_fn(arg(e, 0)) && num_args(e) == 2; } inline expr mk_nat_to_real(expr const & e1) { return mk_app({mk_nat_to_real_fn(), e1}); } expr mk_Real_ge_fn(); bool is_Real_ge_fn(expr const & e); -inline bool is_Real_ge(expr const & e) { return is_app(e) && is_Real_ge_fn(arg(e, 0)); } +inline bool is_Real_ge(expr const & e) { return is_app(e) && is_Real_ge_fn(arg(e, 0)) && num_args(e) == 3; } inline expr mk_Real_ge(expr const & e1, expr const & e2) { return mk_app({mk_Real_ge_fn(), e1, e2}); } expr mk_Real_lt_fn(); bool is_Real_lt_fn(expr const & e); -inline bool is_Real_lt(expr const & e) { return is_app(e) && is_Real_lt_fn(arg(e, 0)); } +inline bool is_Real_lt(expr const & e) { return is_app(e) && is_Real_lt_fn(arg(e, 0)) && num_args(e) == 3; } inline expr mk_Real_lt(expr const & e1, expr const & e2) { return mk_app({mk_Real_lt_fn(), e1, e2}); } expr mk_Real_gt_fn(); bool is_Real_gt_fn(expr const & e); -inline bool is_Real_gt(expr const & e) { return is_app(e) && is_Real_gt_fn(arg(e, 0)); } +inline bool is_Real_gt(expr const & e) { return is_app(e) && is_Real_gt_fn(arg(e, 0)) && num_args(e) == 3; } inline expr mk_Real_gt(expr const & e1, expr const & e2) { return mk_app({mk_Real_gt_fn(), e1, e2}); } expr mk_Real_sub_fn(); bool is_Real_sub_fn(expr const & e); -inline bool is_Real_sub(expr const & e) { return is_app(e) && is_Real_sub_fn(arg(e, 0)); } +inline bool is_Real_sub(expr const & e) { return is_app(e) && is_Real_sub_fn(arg(e, 0)) && num_args(e) == 3; } inline expr mk_Real_sub(expr const & e1, expr const & e2) { return mk_app({mk_Real_sub_fn(), e1, e2}); } expr mk_Real_neg_fn(); bool is_Real_neg_fn(expr const & e); -inline bool is_Real_neg(expr const & e) { return is_app(e) && is_Real_neg_fn(arg(e, 0)); } +inline bool is_Real_neg(expr const & e) { return is_app(e) && is_Real_neg_fn(arg(e, 0)) && num_args(e) == 2; } inline expr mk_Real_neg(expr const & e1) { return mk_app({mk_Real_neg_fn(), e1}); } expr mk_Real_abs_fn(); bool is_Real_abs_fn(expr const & e); -inline bool is_Real_abs(expr const & e) { return is_app(e) && is_Real_abs_fn(arg(e, 0)); } +inline bool is_Real_abs(expr const & e) { return is_app(e) && is_Real_abs_fn(arg(e, 0)) && num_args(e) == 2; } inline expr mk_Real_abs(expr const & e1) { return mk_app({mk_Real_abs_fn(), e1}); } } diff --git a/src/library/cast_decls.cpp b/src/library/cast_decls.cpp new file mode 100644 index 000000000..57b52a09f --- /dev/null +++ b/src/library/cast_decls.cpp @@ -0,0 +1,15 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +*/ +// Automatically generated file, DO NOT EDIT +#include "kernel/environment.h" +#include "kernel/decl_macros.h" +namespace lean { +MK_CONSTANT(cast_fn, name("cast")); +MK_CONSTANT(cast_heq_fn, name("cast_heq")); +MK_CONSTANT(cast_app_fn, name("cast_app")); +MK_CONSTANT(cast_eq_fn, name("cast_eq")); +MK_CONSTANT(cast_trans_fn, name("cast_trans")); +MK_CONSTANT(cast_pull_fn, name("cast_pull")); +} diff --git a/src/library/cast_decls.h b/src/library/cast_decls.h new file mode 100644 index 000000000..c492859d5 --- /dev/null +++ b/src/library/cast_decls.h @@ -0,0 +1,27 @@ +/* +Copyright (c) 2013 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +*/ +// Automatically generated file, DO NOT EDIT +#include "kernel/expr.h" +namespace lean { +expr mk_cast_fn(); +bool is_cast_fn(expr const & e); +inline bool is_cast(expr const & e) { return is_app(e) && is_cast_fn(arg(e, 0)) && num_args(e) == 5; } +inline expr mk_cast(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_cast_fn(), e1, e2, e3, e4}); } +expr mk_cast_heq_fn(); +bool is_cast_heq_fn(expr const & e); +inline expr mk_cast_heq_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_cast_heq_fn(), e1, e2, e3, e4}); } +expr mk_cast_app_fn(); +bool is_cast_app_fn(expr const & e); +inline expr mk_cast_app_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7, expr const & e8) { return mk_app({mk_cast_app_fn(), e1, e2, e3, e4, e5, e6, e7, e8}); } +expr mk_cast_eq_fn(); +bool is_cast_eq_fn(expr const & e); +inline expr mk_cast_eq_th(expr const & e1, expr const & e2, expr const & e3) { return mk_app({mk_cast_eq_fn(), e1, e2, e3}); } +expr mk_cast_trans_fn(); +bool is_cast_trans_fn(expr const & e); +inline expr mk_cast_trans_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6) { return mk_app({mk_cast_trans_fn(), e1, e2, e3, e4, e5, e6}); } +expr mk_cast_pull_fn(); +bool is_cast_pull_fn(expr const & e); +inline expr mk_cast_pull_th(expr const & e1, expr const & e2, expr const & e3, expr const & e4, expr const & e5, expr const & e6, expr const & e7) { return mk_app({mk_cast_pull_fn(), e1, e2, e3, e4, e5, e6, e7}); } +} diff --git a/src/library/heq_decls.h b/src/library/heq_decls.h index f22e4e518..70a4766c7 100644 --- a/src/library/heq_decls.h +++ b/src/library/heq_decls.h @@ -7,7 +7,7 @@ Released under Apache 2.0 license as described in the file LICENSE. namespace lean { expr mk_heq_fn(); bool is_heq_fn(expr const & e); -inline bool is_heq(expr const & e) { return is_app(e) && is_heq_fn(arg(e, 0)); } +inline bool is_heq(expr const & e) { return is_app(e) && is_heq_fn(arg(e, 0)) && num_args(e) == 5; } inline expr mk_heq(expr const & e1, expr const & e2, expr const & e3, expr const & e4) { return mk_app({mk_heq_fn(), e1, e2, e3, e4}); } expr mk_heq_eq_fn(); bool is_heq_eq_fn(expr const & e); diff --git a/src/library/simplifier/simplifier.cpp b/src/library/simplifier/simplifier.cpp index 02b79bd2e..4c47156c2 100644 --- a/src/library/simplifier/simplifier.cpp +++ b/src/library/simplifier/simplifier.cpp @@ -17,6 +17,7 @@ Author: Leonardo de Moura #include "kernel/kernel.h" #include "kernel/max_sharing.h" #include "library/heq_decls.h" +#include "library/cast_decls.h" #include "library/kernel_bindings.h" #include "library/expr_pair.h" #include "library/hop_match.h" @@ -120,6 +121,7 @@ class simplifier_fn { ro_environment m_env; type_checker m_tc; bool m_has_heq; + bool m_has_cast; context m_ctx; rule_sets m_rule_sets; cache m_cache; @@ -300,6 +302,38 @@ class simplifier_fn { } result simplify_app(expr const & e) { + if (m_has_cast && is_cast(e)) { + // e is of the form (cast A B H a) + expr A = arg(e, 1); + expr B = arg(e, 2); + expr H = arg(e, 3); + expr a = arg(e, 4); + if (m_proofs_enabled) { + result res_a = simplify(a); + expr c = res_a.m_out; + if (res_a.m_proof) { + expr Hec; + expr Hac = *res_a.m_proof; + if (!res_a.m_heq_proof) { + Hec = ::lean::mk_htrans_th(A, B, B, e, a, c, + update_app(e, 0, mk_cast_heq_fn()), // cast A B H a == a + mk_to_heq_th(B, a, c, Hac)); // a == c + } else { + Hec = ::lean::mk_htrans_th(A, B, infer_type(c), e, a, c, + update_app(e, 0, mk_cast_heq_fn()), // cast A B H a == a + Hac); // a == c + } + return result(c, Hec, true); + + } else { + // c is definitionally equal to a + // So, we use cast_heq theorem cast_heq : cast A B H a == a + return result(c, update_app(e, 0, mk_cast_heq_fn()), true); + } + } else { + return simplify(arg(e, 4)); + } + } if (m_contextual) { expr const & f = arg(e, 0); for (auto congr_th : m_congr_thms) { @@ -496,10 +530,13 @@ class simplifier_fn { if (i == 0) { pr = *(proofs[0]); heq_proof = m_has_heq && heq_proofs[0]; - } else if (m_has_heq && heq_proofs[i]) { + } else if (m_has_heq && (heq_proofs[i] || !is_arrow(f_types[i-1]))) { expr f = mk_app_prefix(i, new_args); + expr pr_i = *proofs[i]; + if (!heq_proofs[i]) + pr_i = mk_to_heq_th(abst_domain(f_types[i-1]), arg(e, i), new_args[i], pr_i); pr = mk_hcongr_th(f_types[i-1], f_types[i-1], f, f, arg(e, i), new_args[i], - mk_hrefl_th(f_types[i-1], f), *(proofs[i])); + mk_hrefl_th(f_types[i-1], f), pr_i); heq_proof = true; } else { expr f = mk_app_prefix(i, new_args); @@ -510,13 +547,17 @@ class simplifier_fn { expr f = mk_app_prefix(i, e); expr new_f = mk_app_prefix(i, new_args); if (proofs[i]) { + expr pr_i = *proofs[i]; if (m_has_heq && heq_proofs[i]) { if (!heq_proof) pr = mk_to_heq_th(f_types[i], f, new_f, pr); - pr = mk_hcongr_th(f_types[i-1], new_f_types[i-1], f, new_f, arg(e, i), new_args[i], pr, *(proofs[i])); + pr = mk_hcongr_th(f_types[i-1], new_f_types[i-1], f, new_f, arg(e, i), new_args[i], pr, pr_i); heq_proof = true; + } else if (heq_proof) { + pr_i = mk_to_heq_th(abst_domain(f_types[i-1]), arg(e, i), new_args[i], pr_i); + pr = mk_hcongr_th(f_types[i-1], new_f_types[i-1], f, new_f, arg(e, i), new_args[i], pr, pr_i); } else { - pr = mk_congr_th(f_types[i-1], f, new_f, arg(e, i), new_args[i], pr, *(proofs[i])); + pr = mk_congr_th(f_types[i-1], f, new_f, arg(e, i), new_args[i], pr, pr_i); } } else if (heq_proof) { pr = mk_hcongr_th(f_types[i-1], new_f_types[i-1], f, new_f, arg(e, i), arg(e, i), @@ -916,7 +957,8 @@ class simplifier_fn { public: simplifier_fn(ro_environment const & env, options const & o, unsigned num_rs, rewrite_rule_set const * rs): m_env(env), m_tc(env) { - m_has_heq = m_env->imported("heq"); + m_has_heq = m_env->imported("heq"); + m_has_cast = m_env->imported("cast"); set_options(o); if (m_contextual) { // add a set of rewrite rules for contextual rewriting diff --git a/tests/lean/simp18.lean b/tests/lean/simp18.lean new file mode 100644 index 000000000..b33e78550 --- /dev/null +++ b/tests/lean/simp18.lean @@ -0,0 +1,29 @@ +import cast +variable vec : Nat → Type +variable concat {n m : Nat} (v : vec n) (w : vec m) : vec (n + m) +infixl 65 ; : concat +axiom concat_assoc {n1 n2 n3 : Nat} (v1 : vec n1) (v2 : vec n2) (v3 : vec n3) : + (v1 ; v2) ; v3 = cast (congr2 vec (symm (Nat::add_assoc n1 n2 n3))) + (v1 ; (v2 ; v3)) +variable empty : vec 0 +axiom concat_empty {n : Nat} (v : vec n) : + v ; empty = cast (congr2 vec (symm (Nat::add_zeror n))) + v + +rewrite_set simple +add_rewrite concat_assoc concat_empty Nat::add_assoc Nat::add_zeror : simple + +variable n : Nat +variable v : vec n +variable w : vec n + +(* +local t = parse_lean([[ (v ; w) ; empty ; (v ; empty) ]]) +print(t) +print("===>") +local t2, pr = simplify(t, "simple") +print(t2) +print(pr) +get_environment():type_check(pr) +*) + diff --git a/tests/lean/simp18.lean.expected.out b/tests/lean/simp18.lean.expected.out new file mode 100644 index 000000000..deab11cf4 --- /dev/null +++ b/tests/lean/simp18.lean.expected.out @@ -0,0 +1,21 @@ + Set: pp::colors + Set: pp::unicode + Imported 'cast' + Assumed: vec + Assumed: concat + Assumed: concat_assoc + Assumed: empty + Assumed: concat_empty + Assumed: n + Assumed: v + Assumed: w +v ; w ; empty ; (v ; empty) +===> +v ; (w ; v) +htrans (htrans (hcongr (hcongr (hcongr (hcongr (hrefl @concat) (to_heq (Nat::add_zeror (n + n)))) + (to_heq (Nat::add_zeror n))) + (htrans (to_heq (concat_empty (v ; w))) + (cast_heq (congr2 vec (symm (Nat::add_zeror (n + n)))) (v ; w)))) + (htrans (to_heq (concat_empty v)) (cast_heq (congr2 vec (symm (Nat::add_zeror n))) v))) + (to_heq (concat_assoc v w v))) + (cast_heq (congr2 vec (symm (Nat::add_assoc n n n))) (v ; (w ; v)))