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

test(simplifier11.lean): add rule for (not P)

Browse source
This commit is contained in:
Daniel Selsam 2015-11-16 16:40:54 -08:00
parent a02459fe5e
commit 6ba42bb7bc
2 changed files with 15 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/library/blast/simplifier.cpp
View file

@ -191,6 +191,9 @@ class simplifier {
simp_rule_sets srss = _srss; simp_rule_sets srss = _srss;
for (unsigned i = 0; i < ls.size(); i++) { for (unsigned i = 0; i < ls.size(); i++) {
expr & l = ls[i]; expr & l = ls[i];
if (m_trace) {
ios().get_diagnostic_channel() << "Local: " << l << " : " << mlocal_type(l) << "\n";
}
tmp_type_context tctx(env(), ios()); tmp_type_context tctx(env(), ios());
srss = add(tctx, srss, mlocal_name(l), tctx.infer(l), l); srss = add(tctx, srss, mlocal_name(l), tctx.infer(l), l);
} }
@ -593,6 +596,14 @@ result simplifier::rewrite(expr const & e, simp_rule_sets const & srss) {
result simplifier::rewrite(expr const & e, simp_rule const & sr) { result simplifier::rewrite(expr const & e, simp_rule const & sr) {
blast_tmp_type_context tmp_tctx(sr.get_num_umeta(), sr.get_num_emeta()); blast_tmp_type_context tmp_tctx(sr.get_num_umeta(), sr.get_num_emeta());
if (m_trace) {
expr new_lhs = tmp_tctx->instantiate_uvars_mvars(sr.get_lhs());
expr new_rhs = tmp_tctx->instantiate_uvars_mvars(sr.get_rhs());
ios().get_diagnostic_channel()
<< "TRYREW(" << sr.get_id() << ") "
<< "[" << new_lhs << " =?= " << new_rhs << "]\n";
}
if (!tmp_tctx->is_def_eq(e, sr.get_lhs())) return result(e); if (!tmp_tctx->is_def_eq(e, sr.get_lhs())) return result(e);
if (m_trace) { if (m_trace) {

4
tests/lean/simplifier11.lean
View file

@ -1,6 +1,10 @@
-- Conditional congruence -- Conditional congruence
import logic.connectives logic.quantifiers import logic.connectives logic.quantifiers
-- TODO(dhs): either add this to the library or add a `ceqv` rule for
-- ¬ c ==> (¬ c ↔ true) in addition to (c ↔ false)
lemma not_workaround [simp] : ∀ (P : Prop), (P ↔ false) → (¬ P ↔ true) := sorry
namespace if_congr namespace if_congr
constants {A : Type} {b c : Prop} (dec_b : decidable b) (dec_c : decidable c) constants {A : Type} {b c : Prop} (dec_b : decidable b) (dec_c : decidable c)
{x y u v : A} (h_c : b ↔ c) (h_t : x = u) (h_e : y = v) {x y u v : A} (h_c : b ↔ c) (h_t : x = u) (h_e : y = v)