feat(library/tactic): add whnf tactic, closes #270

library/tools/tactic.lean

@@ -37,6 +37,7 @@ opaque definition fail        : tactic := builtin
 opaque definition id          : tactic := builtin
 opaque definition beta        : tactic := builtin
 opaque definition info        : tactic := builtin
+opaque definition whnf        : tactic := builtin
 
 -- This is just a trick to embed expressions into tactics.
 -- The nested expressions are "raw". They tactic should

src/emacs/lean-syntax.el

@@ -119,7 +119,7 @@
      ;; tactics
      (,(rx (not (any "\.")) word-start
            (or "\\b.*_tac" "Cond" "or_else" "then" "try" "when" "assumption" "eassumption" "rapply" "apply" "rename" "intro" "intros"
-               "generalize" "back" "beta" "done" "exact" "repeat")
+               "generalize" "back" "beta" "done" "exact" "repeat" "whnf")
            word-end)
       . 'font-lock-constant-face)
      ;; Types

src/library/tactic/CMakeLists.txt

@@ -1,6 +1,6 @@
 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
+exact_tactic.cpp unfold_tactic.cpp generalize_tactic.cpp whnf_tactic.cpp
 expr_to_tactic.cpp util.cpp init_module.cpp)
 
 target_link_libraries(tactic ${LEAN_LIBS})

src/library/tactic/elaborate.cpp

@@ -9,6 +9,26 @@ Author: Leonardo de Moura
 #include "library/tactic/elaborate.h"
 
 namespace lean {
+bool solve_constraints(environment const & env, io_state const & ios, proof_state & ps, constraint_seq const & cs) {
+    if (!cs)
+        return true;
+    unifier_config cfg(ios.get_options());
+    buffer<constraint> cs_buffer;
+    cs.linearize(cs_buffer);
+    to_buffer(ps.get_postponed(), cs_buffer);
+    name_generator ngen   = ps.get_ngen();
+    substitution subst    = ps.get_subst();
+    unify_result_seq rseq = unify(env, cs_buffer.size(), cs_buffer.data(), ngen.mk_child(), subst, cfg);
+    if (auto p = rseq.pull()) {
+        substitution new_subst     = p->first.first;
+        constraints  new_postponed = p->first.second;
+        ps = proof_state(ps.get_goals(), new_subst, ngen, new_postponed);
+        return true;
+    } else {
+        return false;
+    }
+}
+
 optional<expr> elaborate_with_respect_to(environment const & env, io_state const & ios, elaborate_fn const & elab,
                                          proof_state & s, expr const & e, optional<expr> const & expected_type) {
     name_generator ngen = s.get_ngen();

src/library/tactic/elaborate.h

@@ -8,6 +8,8 @@ Author: Leonardo de Moura
 #include "library/tactic/tactic.h"
 
 namespace lean {
+bool solve_constraints(environment const & env, io_state const & ios, proof_state & ps, constraint_seq const & cs);
+
 /** \brief Function for elaborating expressions nested in tactics.
     Some tactics contain nested expression (aka pre-terms) that need to be elaborated.
 */

src/library/tactic/init_module.cpp

@@ -14,6 +14,7 @@ Author: Leonardo de Moura
 #include "library/tactic/exact_tactic.h"
 #include "library/tactic/unfold_tactic.h"
 #include "library/tactic/generalize_tactic.h"
+#include "library/tactic/whnf_tactic.h"
 
 namespace lean {
 void initialize_tactic_module() {
@@ -27,9 +28,11 @@ void initialize_tactic_module() {
     initialize_exact_tactic();
     initialize_unfold_tactic();
     initialize_generalize_tactic();
+    initialize_whnf_tactic();
 }
 
 void finalize_tactic_module() {
+    finalize_whnf_tactic();
     finalize_generalize_tactic();
     finalize_unfold_tactic();
     finalize_exact_tactic();

src/library/tactic/whnf_tactic.cpp

@@ -0,0 +1,43 @@
+/*
+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 "library/reducible.h"
+#include "library/tactic/expr_to_tactic.h"
+#include "library/tactic/elaborate.h"
+#include "library/tactic/whnf_tactic.h"
+
+namespace lean {
+tactic whnf_tactic(bool relax_main_opaque) {
+    return tactic01([=](environment const & env, io_state const & ios, proof_state const & ps) {
+            goals const & gs = ps.get_goals();
+            if (empty(gs))
+                return none_proof_state();
+            name_generator ngen = ps.get_ngen();
+            auto tc             = mk_type_checker(env, ngen.mk_child(), relax_main_opaque);
+            goal  g             = head(gs);
+            goals tail_gs       = tail(gs);
+            expr  type          = g.get_type();
+            auto t_cs           = tc->whnf(type);
+            goals new_gs(goal(g.get_meta(), t_cs.first), tail_gs);
+            proof_state new_ps(ps, new_gs, ngen);
+            if (solve_constraints(env, ios, new_ps, t_cs.second)) {
+                return some_proof_state(new_ps);
+            } else {
+                return none_proof_state();
+            }
+        });
+}
+
+void initialize_whnf_tactic() {
+    register_tac(name({"tactic", "whnf"}),
+                 [](type_checker &, elaborate_fn const &, expr const &, pos_info_provider const *) {
+                     return whnf_tactic();
+                 });
+}
+
+void finalize_whnf_tactic() {
+}
+}

src/library/tactic/whnf_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 whnf_tactic(bool relax_main_opaque = true);
+void initialize_whnf_tactic();
+void finalize_whnf_tactic();
+}

tests/lean/whnf_tac.lean

@@ -0,0 +1,11 @@
+import logic
+
+definition id {A : Type} (a : A) := a
+
+theorem tst (a : Prop) : a → id a :=
+begin
+  intro Ha,
+  whnf,
+  state,
+  apply Ha
+end

tests/lean/whnf_tac.lean.expected.out

@@ -0,0 +1,4 @@
+whnf_tac.lean:9:2: proof state
+a : Prop,
+Ha : a
+⊢ a