feat(library/tactic): add 'exfalso' tactic

see issue #500

hott/init/tactic.hlean

@@ -43,6 +43,7 @@ opaque definition beta        : tactic := builtin
 opaque definition info        : tactic := builtin
 opaque definition whnf        : tactic := builtin
 opaque definition contradiction : tactic := builtin
+opaque definition exfalso : tactic := builtin
 opaque definition rotate_left (k : num) := builtin
 opaque definition rotate_right (k : num) := builtin
 definition rotate (k : num) := rotate_left k

library/init/tactic.lean

@@ -43,6 +43,7 @@ opaque definition beta        : tactic := builtin
 opaque definition info        : tactic := builtin
 opaque definition whnf        : tactic := builtin
 opaque definition contradiction : tactic := builtin
+opaque definition exfalso : tactic := builtin
 opaque definition rotate_left (k : num) := builtin
 opaque definition rotate_right (k : num) := builtin
 definition rotate (k : num) := rotate_left k

src/emacs/lean-syntax.el

@@ -135,7 +135,7 @@
                 "apply" "fapply" "rename" "intro" "intros" "all_goals" "fold"
                 "generalize" "generalizes" "clear" "clears" "revert" "reverts" "back" "beta" "done" "exact" "rexact"
                 "refine" "repeat" "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "rewrite" "esimp"
-                "unfold" "change" "check_expr" "contradiction"))
+                "unfold" "change" "check_expr" "contradiction" "exfalso"))
            word-end)
       (1 'font-lock-constant-face))
      ;; Types

src/library/tactic/CMakeLists.txt

@@ -4,6 +4,7 @@ exact_tactic.cpp generalize_tactic.cpp
 inversion_tactic.cpp whnf_tactic.cpp revert_tactic.cpp
 assert_tactic.cpp clear_tactic.cpp expr_to_tactic.cpp location.cpp
 rewrite_tactic.cpp util.cpp class_instance_synth.cpp init_module.cpp
-change_tactic.cpp check_expr_tactic.cpp let_tactic.cpp contradiction_tactic.cpp)
+change_tactic.cpp check_expr_tactic.cpp let_tactic.cpp contradiction_tactic.cpp
+exfalso_tactic.cpp)
 
 target_link_libraries(tactic ${LEAN_LIBS})

src/library/tactic/exfalso_tactic.cpp

@@ -0,0 +1,44 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "kernel/inductive/inductive.h"
+#include "library/constants.h"
+#include "library/util.h"
+#include "library/reducible.h"
+#include "library/tactic/intros_tactic.h"
+#include "library/tactic/expr_to_tactic.h"
+#include "kernel/kernel_exception.h"
+
+namespace lean {
+tactic exfalso_tactic() {
+    auto fn = [=](environment const & env, io_state const &, proof_state const & s) {
+        goals const & gs = s.get_goals();
+        if (empty(gs)) {
+            throw_no_goal_if_enabled(s);
+            return optional<proof_state>();
+        }
+        goal const & g      = head(gs);
+        expr const & t      = g.get_type();
+        substitution subst  = s.get_subst();
+        name_generator ngen = s.get_ngen();
+        auto tc             = mk_type_checker(env, ngen.mk_child(), s.relax_main_opaque());
+        expr false_expr     = mk_false(env);
+        expr new_meta       = g.mk_meta(ngen.next(), false_expr);
+        goal new_goal(new_meta, false_expr);
+        assign(subst, g, mk_false_rec(*tc, new_meta, t));
+        return some(proof_state(s, goals(new_goal, tail(gs)), subst, ngen));
+    };
+    return tactic01(fn);
+}
+void initialize_exfalso_tactic() {
+    register_tac(name{"tactic", "exfalso"},
+                 [](type_checker &, elaborate_fn const &, expr const &, pos_info_provider const *) {
+                     return exfalso_tactic();
+                 });
+}
+void finalize_exfalso_tactic() {
+}
+}

src/library/tactic/exfalso_tactic.h

@@ -0,0 +1,11 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+namespace lean {
+void initialize_exfalso_tactic();
+void finalize_exfalso_tactic();
+}

src/library/tactic/init_module.cpp

@@ -24,6 +24,7 @@ Author: Leonardo de Moura
 #include "library/tactic/check_expr_tactic.h"
 #include "library/tactic/let_tactic.h"
 #include "library/tactic/contradiction_tactic.h"
+#include "library/tactic/exfalso_tactic.h"
 
 namespace lean {
 void initialize_tactic_module() {
@@ -47,9 +48,11 @@ void initialize_tactic_module() {
     initialize_check_expr_tactic();
     initialize_let_tactic();
     initialize_contradiction_tactic();
+    initialize_exfalso_tactic();
 }
 
 void finalize_tactic_module() {
+    finalize_exfalso_tactic();
     finalize_contradiction_tactic();
     finalize_let_tactic();
     finalize_check_expr_tactic();

src/library/util.cpp

@@ -244,6 +244,18 @@ expr to_telescope(type_checker & tc, expr type, buffer<expr> & telescope, option
     return to_telescope(tc, type, telescope, binfo, cs);
 }
 
+expr mk_false() {
+    return mk_constant(get_false_name());
+}
+
+expr mk_empty() {
+    return mk_constant(get_empty_name(), {mk_level_zero()});
+}
+
+expr mk_false(environment const & env) {
+    return is_standard(env) ? mk_false() : mk_empty();
+}
+
 bool is_false(expr const & e) {
     return is_constant(e) && const_name(e) == get_false_name();
 }

src/library/util.h

@@ -126,6 +126,10 @@ expr mk_pair(type_checker & tc, expr const & a, expr const & b, bool prop);
 expr mk_pr1(type_checker & tc, expr const & p, bool prop);
 expr mk_pr2(type_checker & tc, expr const & p, bool prop);
 
+expr mk_false();
+expr mk_empty();
+/** \brief Return false (in standard mode) and empty (in HoTT) mode */
+expr mk_false(environment const & env);
 
 bool is_false(expr const & e);
 bool is_empty(expr const & e);

tests/lean/hott/exfalso1.hlean

@@ -0,0 +1,9 @@
+open nat
+
+example (a b : nat) : a = 0 → b = 1 → a = b → a + b * b ≤ 10000 :=
+begin
+  intro a0 b1 ab,
+  exfalso, state,
+  rewrite [a0 at ab, b1 at ab],
+  contradiction
+end

tests/lean/run/exfalso1.lean

@@ -0,0 +1,9 @@
+open nat
+
+example (a b : nat) : a = 0 → b = 1 → a = b → a + b * b ≤ 10000 :=
+begin
+  intro a0 b1 ab,
+  exfalso, state,
+  rewrite [a0 at ab, b1 at ab],
+  contradiction
+end