feat(library/blast/actions): by_contradiction action

src/library/blast/actions/CMakeLists.txt

@@ -1,3 +1,3 @@
 add_library(blast_actions OBJECT init_module.cpp simple_actions.cpp
   intros_action.cpp subst_action.cpp no_confusion_action.cpp
-  recursor_action.cpp assert_cc_action.cpp)
+  recursor_action.cpp assert_cc_action.cpp by_contradiction_action.cpp)

src/library/blast/actions/by_contradiction_action.cpp

@@ -0,0 +1,48 @@
+/*
+Copyright (c) 2015 Daniel Selsam. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Daniel Selsam
+*/
+#include "library/constants.h"
+#include "library/blast/blast.h"
+#include "library/blast/blast_exception.h"
+#include "library/blast/actions/intros_action.h"
+#include "library/blast/proof_expr.h"
+#include "library/blast/trace.h"
+#include "library/blast/util.h"
+
+namespace lean {
+namespace blast {
+
+struct by_contradiction_proof_step_cell : public proof_step_cell {
+    expr m_href;
+    by_contradiction_proof_step_cell(expr const & href): m_href(href) {}
+    virtual ~by_contradiction_proof_step_cell() {}
+    virtual action_result resolve(expr const & pf) const override {
+        expr new_pf = mk_proof_lambda(curr_state(), m_href, pf);
+        return action_result::solved(mk_proof_app(get_decidable_by_contradiction_name(), 1, &new_pf));
+    }
+    virtual bool is_silent() const override { return true; }
+};
+
+action_result by_contradiction_action() {
+    state &  s  = curr_state();
+    expr target = whnf(s.get_target());
+    if (!is_prop(target)) return action_result::failed();
+    if (blast::is_false(target)) return action_result::failed();
+    expr not_target;
+    if (is_not(target, not_target)) {
+        s.set_target(mk_arrow(not_target, mk_constant(get_false_name())));
+        return intros_action(1);
+    }
+    blast_tmp_type_context tmp_tctx;
+    optional<expr> target_decidable = tmp_tctx->mk_class_instance(mk_app(mk_constant(get_decidable_name()), target));
+    if (!target_decidable) return action_result::failed();
+    expr href = s.mk_hypothesis(get_app_builder().mk_not(target));
+    auto pcell = new by_contradiction_proof_step_cell(href);
+    s.push_proof_step(pcell);
+    s.set_target(mk_constant(get_false_name()));
+    trace_action("by_contradiction");
+    return action_result::new_branch();
+}
+}}

src/library/blast/actions/by_contradiction_action.h

@@ -0,0 +1,11 @@
+/*
+Copyright (c) 2015 Daniel Selsam. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Daniel Selsam
+*/
+#pragma once
+#include "library/blast/action_result.h"
+namespace lean {
+namespace blast {
+action_result by_contradiction_action();
+}}

src/library/blast/strategies/simple_strategy.cpp

@@ -20,6 +20,7 @@ Author: Leonardo de Moura
 #include "library/blast/actions/intros_action.h"
 #include "library/blast/actions/subst_action.h"
 #include "library/blast/actions/recursor_action.h"
+#include "library/blast/actions/by_contradiction_action.h"
 #include "library/blast/actions/assert_cc_action.h"
 #include "library/blast/actions/no_confusion_action.h"
 
@@ -70,6 +71,7 @@ class simple_strategy : public strategy {
         Try(recursor_action());
         Try(constructor_action());
         Try(ematch_action());
+        Try(by_contradiction_action());
         TryStrategy(apply_backward_strategy());
         Try(qfc_action(list<gexpr>()));
 

src/library/constants.cpp

@@ -24,6 +24,7 @@ name const * g_congr = nullptr;
 name const * g_congr_arg = nullptr;
 name const * g_congr_fun = nullptr;
 name const * g_decidable = nullptr;
+name const * g_decidable_by_contradiction = nullptr;
 name const * g_dite = nullptr;
 name const * g_div = nullptr;
 name const * g_empty = nullptr;
@@ -210,6 +211,7 @@ void initialize_constants() {
     g_congr_arg = new name{"congr_arg"};
     g_congr_fun = new name{"congr_fun"};
     g_decidable = new name{"decidable"};
+    g_decidable_by_contradiction = new name{"decidable", "by_contradiction"};
     g_dite = new name{"dite"};
     g_div = new name{"div"};
     g_empty = new name{"empty"};
@@ -397,6 +399,7 @@ void finalize_constants() {
     delete g_congr_arg;
     delete g_congr_fun;
     delete g_decidable;
+    delete g_decidable_by_contradiction;
     delete g_dite;
     delete g_div;
     delete g_empty;
@@ -583,6 +586,7 @@ name const & get_congr_name() { return *g_congr; }
 name const & get_congr_arg_name() { return *g_congr_arg; }
 name const & get_congr_fun_name() { return *g_congr_fun; }
 name const & get_decidable_name() { return *g_decidable; }
+name const & get_decidable_by_contradiction_name() { return *g_decidable_by_contradiction; }
 name const & get_dite_name() { return *g_dite; }
 name const & get_div_name() { return *g_div; }
 name const & get_empty_name() { return *g_empty; }

src/library/constants.h

@@ -26,6 +26,7 @@ name const & get_congr_name();
 name const & get_congr_arg_name();
 name const & get_congr_fun_name();
 name const & get_decidable_name();
+name const & get_decidable_by_contradiction_name();
 name const & get_dite_name();
 name const & get_div_name();
 name const & get_empty_name();

src/library/constants.txt

@@ -19,6 +19,7 @@ congr
 congr_arg
 congr_fun
 decidable
+decidable.by_contradiction
 dite
 div
 empty

tests/lean/run/blast_by_contradiction.lean

@@ -0,0 +1,16 @@
+constants P Q : Prop
+
+namespace with_classical
+open classical
+
+example : Q → (Q → ¬ P → false) → P := by blast
+example : Q → (Q → P → false) → ¬ P := by blast
+end with_classical
+
+namespace with_decidable
+constant P_dec : decidable P
+attribute P_dec [instance]
+
+definition foo : Q → (Q → ¬ P → false) → P := by blast
+example : Q → (Q → P → false) → ¬ P := by blast
+end with_decidable