feat(library/tactic): add 'assert' tactic, closes #349

library/tools/tactic.lean

@@ -83,6 +83,9 @@ notation `clears` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)`
 opaque definition revert_lst (ids : expr_list) : tactic := builtin
 notation `reverts` `(` l:(foldr `,` (h t, expr_list.cons h t) expr_list.nil) `)` := revert_lst l
 
+opaque definition assert_hypothesis (id : expr) (e : expr) : tactic := builtin
+notation `assert` `(` id `:` ty `)` := assert_hypothesis id ty
+
 infixl `;`:15 := and_then
 notation `[` h:10 `|`:10 r:(foldl:10 `|` (e r, or_else r e) h) `]` := r
 

src/emacs/lean-syntax.el

@@ -124,7 +124,7 @@
      (,(rx (not (any "\.")) word-start
            (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "eassumption" "rapply" "apply" "fapply" "rename" "intro" "intros"
                "generalize" "generalizes" "clear" "clears" "revert" "reverts" "back" "beta" "done" "exact" "repeat"
-               "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases")
+               "whnf" "rotate" "rotate_left" "rotate_right" "inversion" "cases" "assert")
            word-end)
       . 'font-lock-constant-face)
      ;; Types

src/library/tactic/CMakeLists.txt

@@ -2,6 +2,7 @@ add_library(tactic goal.cpp proof_state.cpp tactic.cpp elaborate.cpp
 apply_tactic.cpp intros_tactic.cpp rename_tactic.cpp trace_tactic.cpp
 exact_tactic.cpp unfold_tactic.cpp generalize_tactic.cpp
 inversion_tactic.cpp whnf_tactic.cpp revert_tactic.cpp
-clear_tactic.cpp expr_to_tactic.cpp util.cpp init_module.cpp)
+assert_tactic.cpp clear_tactic.cpp expr_to_tactic.cpp util.cpp
+init_module.cpp)
 
 target_link_libraries(tactic ${LEAN_LIBS})

src/library/tactic/assert_tactic.cpp

@@ -0,0 +1,58 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "kernel/abstract.h"
+#include "library/tactic/tactic.h"
+#include "library/tactic/elaborate.h"
+#include "library/tactic/expr_to_tactic.h"
+
+namespace lean {
+tactic assert_tactic(elaborate_fn const & elab, name const & id, expr const & e) {
+    return tactic01([=](environment const & env, io_state const & ios, proof_state const & s) {
+            proof_state new_s = s;
+            goals const & gs  = new_s.get_goals();
+            if (!gs)
+                return none_proof_state();
+            bool report_unassigned = true;
+            if (auto new_e = elaborate_with_respect_to(env, ios, elab, new_s, e, none_expr(), report_unassigned)) {
+                goals const & gs   = new_s.get_goals();
+                goal const & g     = head(gs);
+                if (g.find_hyp(id)) {
+                    // goal already has a hypothesis named id
+                    return none_proof_state();
+                }
+                name_generator ngen = new_s.get_ngen();
+                expr new_meta1      = g.mk_meta(ngen.next(), *new_e);
+                goal new_goal1(new_meta1, *new_e);
+                expr new_local      = mk_local(ngen.next(), id, *new_e, binder_info());
+                buffer<expr> hyps;
+                g.get_hyps(hyps);
+                hyps.push_back(new_local);
+                expr new_mvar2      = mk_metavar(ngen.next(), Pi(hyps, g.get_type()));
+                hyps.pop_back();
+                expr new_meta2_core = mk_app(new_mvar2, hyps);
+                expr new_meta2      = mk_app(new_meta2_core, new_local);
+                goal new_goal2(new_meta2, g.get_type());
+                expr val            = g.abstract(mk_app(new_meta2_core, new_meta1));
+                substitution new_subst = new_s.get_subst();
+                new_subst.assign(g.get_name(), val);
+                return some_proof_state(proof_state(new_s, cons(new_goal1, cons(new_goal2, tail(gs))), new_subst, ngen));
+            }
+            return none_proof_state();
+        });
+}
+
+void initialize_assert_tactic() {
+    register_tac(name{"tactic", "assert_hypothesis"},
+                 [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
+                     name id = tactic_expr_to_id(app_arg(app_fn(e)), "invalid 'assert' tactic, argument must be an identifier");
+                     check_tactic_expr(app_arg(e), "invalid 'assert' tactic, argument must be an expression");
+                     return assert_tactic(fn, id, get_tactic_expr_expr(app_arg(e)));
+                 });
+}
+void finalize_assert_tactic() {
+}
+}

src/library/tactic/assert_tactic.h

@@ -0,0 +1,14 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "library/tactic/tactic.h"
+
+namespace lean {
+tactic assert_tactic(elaborate_fn const & elab, name const & id, expr const & e);
+void initialize_assert_tactic();
+void finalize_assert_tactic();
+}

src/library/tactic/init_module.cpp

@@ -18,6 +18,7 @@ Author: Leonardo de Moura
 #include "library/tactic/clear_tactic.h"
 #include "library/tactic/revert_tactic.h"
 #include "library/tactic/inversion_tactic.h"
+#include "library/tactic/assert_tactic.h"
 
 namespace lean {
 void initialize_tactic_module() {
@@ -35,9 +36,11 @@ void initialize_tactic_module() {
     initialize_clear_tactic();
     initialize_revert_tactic();
     initialize_inversion_tactic();
+    initialize_assert_tactic();
 }
 
 void finalize_tactic_module() {
+    finalize_assert_tactic();
     finalize_inversion_tactic();
     finalize_revert_tactic();
     finalize_clear_tactic();

tests/lean/run/assert_tac.lean

@@ -0,0 +1,12 @@
+import logic
+
+variables {A : Type} {a a' : A}
+
+definition to_eq (H : a == a') : a = a' :=
+begin
+  assert (H₁ : ∀ (Ht : A = A), eq.rec_on Ht a = a),
+  intro Ht,
+    exact (eq.refl (eq.rec_on Ht a)),
+  show a = a', from
+    heq.rec_on H H₁ (eq.refl A)
+end