feat(frontends/lean): use rewrite tactic to implement unfold (it has a unfold step)

closes #502

hott/hit/quotient.hlean

@@ -25,7 +25,7 @@ parameters {A : Type} (R : A → A → hprop)
   ap tr (eq_of_rel H)
 
   theorem is_hset_quotient : is_hset quotient :=
-  by unfold quotient; exact _
+  begin unfold quotient, exact _ end
 
   protected definition rec {P : quotient → Type} [Pt : Πaa, is_hset (P aa)]
     (Pc : Π(a : A), P (class_of a)) (Pp : Π⦃a a' : A⦄ (H : R a a'), eq_of_rel H ▹ Pc a = Pc a')

hott/init/tactic.hlean

@@ -72,7 +72,6 @@ opaque definition intro      (e : identifier)   : tactic := builtin
 opaque definition generalize (e : expr)         : tactic := builtin
 opaque definition clear      (e : identifier)   : tactic := builtin
 opaque definition revert     (e : identifier)   : tactic := builtin
-opaque definition unfold     (e : expr)         : tactic := builtin
 opaque definition refine     (e : expr)         : tactic := builtin
 opaque definition exact      (e : expr)         : tactic := builtin
 -- Relaxed version of exact that does not enforce goal type

library/init/tactic.lean

@@ -72,7 +72,6 @@ opaque definition intro      (e : identifier)   : tactic := builtin
 opaque definition generalize (e : expr)         : tactic := builtin
 opaque definition clear      (e : identifier)   : tactic := builtin
 opaque definition revert     (e : identifier)   : tactic := builtin
-opaque definition unfold     (e : expr)         : tactic := builtin
 opaque definition refine     (e : expr)         : tactic := builtin
 opaque definition exact      (e : expr)         : tactic := builtin
 -- Relaxed version of exact that does not enforce goal type

src/frontends/lean/builtin_exprs.cpp

@@ -529,6 +529,10 @@ static expr parse_esimp_tactic_expr(parser & p, unsigned, expr const *, pos_info
     return p.save_pos(parse_esimp_tactic(p), pos);
 }
 
+static expr parse_unfold_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
+    return p.save_pos(parse_unfold_tactic(p), pos);
+}
+
 static expr parse_fold_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
     return p.save_pos(parse_fold_tactic(p), pos);
 }
@@ -605,6 +609,7 @@ parse_table init_nud_table() {
     r = r.add({transition("calc", mk_ext_action(parse_calc_expr))}, x0);
     r = r.add({transition("rewrite", mk_ext_action(parse_rewrite_tactic_expr))}, x0);
     r = r.add({transition("esimp", mk_ext_action(parse_esimp_tactic_expr))}, x0);
+    r = r.add({transition("unfold", mk_ext_action(parse_unfold_tactic_expr))}, x0);
     r = r.add({transition("fold", mk_ext_action(parse_fold_tactic_expr))}, x0);
     r = r.add({transition("#", mk_ext_action(parse_overwrite_notation))}, x0);
     r = r.add({transition("@", mk_ext_action(parse_explicit_expr))}, x0);

src/frontends/lean/parse_rewrite_tactic.cpp

@@ -153,6 +153,21 @@ expr parse_esimp_tactic(parser & p) {
     return mk_rewrite_tactic_expr(elems);
 }
 
+expr parse_unfold_tactic(parser & p) {
+    buffer<expr> elems;
+    auto pos = p.pos();
+    if (p.curr_is_identifier()) {
+        name c       = p.check_constant_next("invalid unfold tactic, identifier expected");
+        location loc = parse_tactic_location(p);
+        elems.push_back(p.save_pos(mk_rewrite_unfold(to_list(c), loc), pos));
+    } else if (p.curr_is_token(get_lbracket_tk())) {
+        elems.push_back(p.save_pos(parse_rewrite_unfold_core(p), pos));
+    } else {
+        throw parser_error("invalid unfold tactic, identifier or `[` expected", pos);
+    }
+    return mk_rewrite_tactic_expr(elems);
+}
+
 expr parse_fold_tactic(parser & p) {
     buffer<expr> elems;
     auto pos = p.pos();

src/frontends/lean/parse_rewrite_tactic.h

@@ -11,5 +11,6 @@ namespace lean {
 class parser;
 expr parse_rewrite_tactic(parser & p);
 expr parse_esimp_tactic(parser & p);
+expr parse_unfold_tactic(parser & p);
 expr parse_fold_tactic(parser & p);
 }

src/frontends/lean/token_table.cpp

@@ -80,7 +80,7 @@ void init_token_table(token_table & t) {
          {"[", g_max_prec}, {"]", 0}, {"⦃", g_max_prec}, {"⦄", 0}, {".{", 0}, {"Type", g_max_prec},
          {"{|", g_max_prec}, {"|}", 0}, {"⊢", 0}, {"⟨", g_max_prec}, {"⟩", 0}, {"^", 0}, {"↑", 0}, {"▸", 0},
          {"using", 0}, {"|", 0}, {"!", g_max_prec}, {"?", 0},  {"with", 0}, {"...", 0}, {",", 0}, {";", 1},
-         {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"rewrite", 0}, {"esimp", 0}, {"fold", 0},
+         {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {"rewrite", 0}, {"esimp", 0}, {"fold", 0}, {"unfold", 0},
          {":=", 0}, {"--", 0}, {"#", 0},
          {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec},
          {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec},

src/library/constants.cpp

@@ -111,7 +111,6 @@ name const * g_tactic_rotate_right = nullptr;
 name const * g_tactic_state = nullptr;
 name const * g_tactic_trace = nullptr;
 name const * g_tactic_try_for = nullptr;
-name const * g_tactic_unfold = nullptr;
 name const * g_tactic_whnf = nullptr;
 name const * g_trans_rel_left = nullptr;
 name const * g_trans_rel_right = nullptr;
@@ -231,7 +230,6 @@ void initialize_constants() {
     g_tactic_state = new name{"tactic", "state"};
     g_tactic_trace = new name{"tactic", "trace"};
     g_tactic_try_for = new name{"tactic", "try_for"};
-    g_tactic_unfold = new name{"tactic", "unfold"};
     g_tactic_whnf = new name{"tactic", "whnf"};
     g_trans_rel_left = new name{"trans_rel_left"};
     g_trans_rel_right = new name{"trans_rel_right"};
@@ -352,7 +350,6 @@ void finalize_constants() {
     delete g_tactic_state;
     delete g_tactic_trace;
     delete g_tactic_try_for;
-    delete g_tactic_unfold;
     delete g_tactic_whnf;
     delete g_trans_rel_left;
     delete g_trans_rel_right;
@@ -472,7 +469,6 @@ name const & get_tactic_rotate_right_name() { return *g_tactic_rotate_right; }
 name const & get_tactic_state_name() { return *g_tactic_state; }
 name const & get_tactic_trace_name() { return *g_tactic_trace; }
 name const & get_tactic_try_for_name() { return *g_tactic_try_for; }
-name const & get_tactic_unfold_name() { return *g_tactic_unfold; }
 name const & get_tactic_whnf_name() { return *g_tactic_whnf; }
 name const & get_trans_rel_left_name() { return *g_trans_rel_left; }
 name const & get_trans_rel_right_name() { return *g_trans_rel_right; }

src/library/constants.h

@@ -113,7 +113,6 @@ name const & get_tactic_rotate_right_name();
 name const & get_tactic_state_name();
 name const & get_tactic_trace_name();
 name const & get_tactic_try_for_name();
-name const & get_tactic_unfold_name();
 name const & get_tactic_whnf_name();
 name const & get_trans_rel_left_name();
 name const & get_trans_rel_right_name();

src/library/constants.txt

@@ -106,7 +106,6 @@ tactic.rotate_right
 tactic.state
 tactic.trace
 tactic.try_for
-tactic.unfold
 tactic.whnf
 trans_rel_left
 trans_rel_right

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 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

src/library/tactic/init_module.cpp

@@ -12,7 +12,6 @@ Author: Leonardo de Moura
 #include "library/tactic/intros_tactic.h"
 #include "library/tactic/trace_tactic.h"
 #include "library/tactic/exact_tactic.h"
-#include "library/tactic/unfold_tactic.h"
 #include "library/tactic/generalize_tactic.h"
 #include "library/tactic/whnf_tactic.h"
 #include "library/tactic/clear_tactic.h"
@@ -34,7 +33,6 @@ void initialize_tactic_module() {
     initialize_intros_tactic();
     initialize_trace_tactic();
     initialize_exact_tactic();
-    initialize_unfold_tactic();
     initialize_generalize_tactic();
     initialize_whnf_tactic();
     initialize_clear_tactic();
@@ -58,7 +56,6 @@ void finalize_tactic_module() {
     finalize_clear_tactic();
     finalize_whnf_tactic();
     finalize_generalize_tactic();
-    finalize_unfold_tactic();
     finalize_exact_tactic();
     finalize_trace_tactic();
     finalize_intros_tactic();

src/library/tactic/unfold_tactic.cpp

@@ -1,128 +0,0 @@
-/*
-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/instantiate.h"
-#include "library/constants.h"
-#include "library/replace_visitor.h"
-#include "library/tactic/unfold_tactic.h"
-#include "library/tactic/expr_to_tactic.h"
-
-namespace lean {
-class unfold_core_fn : public replace_visitor {
-protected:
-    bool m_unfolded;
-
-    virtual expr visit_app(expr const & e) {
-        expr const & f = get_app_fn(e);
-        if (is_constant(f)) {
-            expr new_f = visit(f);
-            bool modified = new_f != f;
-            buffer<expr> new_args;
-            get_app_args(e, new_args);
-            for (unsigned i = 0; i < new_args.size(); i++) {
-                expr arg    = new_args[i];
-                new_args[i] = visit(arg);
-                if (!modified && new_args[i] != arg)
-                    modified = true;
-            }
-            if (is_lambda(new_f)) {
-                std::reverse(new_args.begin(), new_args.end());
-                return apply_beta(new_f, new_args.size(), new_args.data());
-            } else if (modified) {
-                return mk_app(new_f, new_args);
-            } else {
-                return e;
-            }
-        } else {
-            return replace_visitor::visit_app(e);
-        }
-    }
-public:
-    unfold_core_fn():m_unfolded(false) {}
-    bool unfolded() const { return m_unfolded; }
-};
-
-class unfold_fn : public unfold_core_fn {
-protected:
-    name const &              m_name;
-    level_param_names const & m_ps;
-    expr const &              m_def;
-
-    virtual expr visit_constant(expr const & c) {
-        if (const_name(c) == m_name) {
-            m_unfolded = true;
-            return instantiate_univ_params(m_def, m_ps, const_levels(c));
-        } else {
-            return c;
-        }
-    }
-
-public:
-    unfold_fn(name const & n, level_param_names const & ps, expr const & d):m_name(n), m_ps(ps), m_def(d) {}
-};
-
-class unfold_all_fn : public unfold_core_fn {
-protected:
-    environment m_env;
-
-    virtual expr visit_constant(expr const & c) {
-        optional<declaration> d = m_env.find(const_name(c));
-        if (d && d->is_definition() && (!d->is_opaque() || d->get_module_idx() == 0)) {
-            m_unfolded = true;
-            return instantiate_value_univ_params(*d, const_levels(c));
-        } else {
-            return c;
-        }
-    }
-
-public:
-    unfold_all_fn(environment const & env):m_env(env) {}
-};
-
-optional<proof_state> unfold_tactic_core(unfold_core_fn & fn, proof_state const & s) {
-    bool reduced = false;
-    goals new_gs = map_goals(s, [&](goal const & g) -> optional<goal> {
-            expr new_meta = fn(g.get_meta());
-            expr new_type = fn(g.get_type());
-            if (new_meta != g.get_meta() || new_type != g.get_type())
-                reduced = true;
-            return some(goal(new_meta, new_type));
-        });
-    if (reduced) {
-        return some(proof_state(s, new_gs));
-    } else {
-        return none_proof_state();
-    }
-}
-
-tactic unfold_tactic(name const & n) {
-    return tactic01([=](environment const & env, io_state const &, proof_state const & s) -> optional<proof_state> {
-            optional<declaration> d = env.find(n);
-            if (!d || !d->is_definition() || (d->is_opaque() && d->get_module_idx() != 0))
-                return none_proof_state(); // tactic failed
-            unfold_fn fn(n, d->get_univ_params(), d->get_value());
-            return unfold_tactic_core(fn, s);
-        });
-}
-
-tactic unfold_tactic() {
-    return tactic01([=](environment const & env, io_state const &, proof_state const & s) -> optional<proof_state> {
-            unfold_all_fn fn(env);
-            return unfold_tactic_core(fn, s);
-        });
-}
-
-void initialize_unfold_tactic() {
-    register_tac(get_tactic_unfold_name(),
-                 [](type_checker &, elaborate_fn const &, expr const & e, pos_info_provider const *) {
-                     name const & id = tactic_expr_to_id(app_arg(e),
-                                                         "invalid 'unfold' tactic, argument must be an identifier");
-                     return unfold_tactic(id);
-                 });
-}
-void finalize_unfold_tactic() {
-}
-}

src/library/tactic/unfold_tactic.h

@@ -1,18 +0,0 @@
-/*
-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 {
-/** \brief Return a tactic that unfolds the definition named \c n. */
-tactic unfold_tactic(name const & n);
-/** \brief Return a tactic that unfolds all (non-opaque) definitions. */
-tactic unfold_tactic();
-
-void initialize_unfold_tactic();
-void finalize_unfold_tactic();
-}

tests/lean/run/466.lean

@@ -7,8 +7,6 @@ section
 
   definition bar (a : A) : foo a = refl a :=
   begin
-    unfold foo,
-    apply rfl
+    unfold foo
   end
-
 end

tests/lean/run/univ1.lean

@@ -3,18 +3,18 @@ import logic
 namespace S1
 axiom I : Type
 definition F (X : Type) : Type := (X → Prop) → Prop
-axiom unfold.{l} : I.{l} → F I.{l}
+axiom unfoldd.{l} : I.{l} → F I.{l}
 axiom foldd.{l}   : F I.{l} → I.{l}
-axiom iso1 : ∀x, foldd (unfold x) = x
+axiom iso1 : ∀x, foldd (unfoldd x) = x
 end S1
 
 namespace S2
 universe u
 axiom I : Type.{u}
 definition F (X : Type) : Type := (X → Prop) → Prop
-axiom unfold : I → F I
+axiom unfoldd : I → F I
 axiom foldd   : F I → I
-axiom iso1 : ∀x, foldd (unfold x) = x
+axiom iso1 : ∀x, foldd (unfoldd x) = x
 end S2
 
 
@@ -22,8 +22,8 @@ namespace S3
 section
   hypothesis I : Type
   definition F (X : Type) : Type := (X → Prop) → Prop
-  hypothesis unfold : I → F I
+  hypothesis unfoldd : I → F I
   hypothesis foldd   : F I → I
-  hypothesis iso1 : ∀x, foldd (unfold x) = x
+  hypothesis iso1 : ∀x, foldd (unfoldd x) = x
 end
 end S3

tests/lean/run/univ2.lean

@@ -2,9 +2,9 @@ import logic
 
 axiom I : Type
 definition F (X : Type) : Type := (X → Prop) → Prop
-axiom unfold : I → F I
+axiom unfoldd : I → F I
 axiom foldd   : F I → I
-axiom iso1 : ∀x, foldd (unfold x) = x
+axiom iso1 : ∀x, foldd (unfoldd x) = x
 
-theorem iso2 : ∀x, foldd (unfold x) = x
+theorem iso2 : ∀x, foldd (unfoldd x) = x
 := sorry

tests/lean/unfold.lean

@@ -0,0 +1,42 @@
+import data.nat
+open nat
+
+definition f (a b : nat) := a + b
+
+example (a b : nat) : f a b = 0 → f b a = 0 :=
+begin
+  intro h,
+  unfold f at h,
+  state,
+  unfold f,
+  state,
+  rewrite [add.comm],
+  exact h
+end
+
+example (a b : nat) : f a b = 0 → f b a = 0 :=
+begin
+  intro h,
+  unfold f at *,
+  state,
+  rewrite [add.comm],
+  exact h
+end
+
+example (a b c : nat) : f c c = 0 → f a b = 0 → f b a = f c c :=
+begin
+  intros [h₁, h₂],
+  unfold f at (h₁, h₂),
+  state,
+  unfold f,
+  rewrite [add.comm, h₁, h₂],
+end
+
+example (a b c : nat) : f c c = 0 → f a b = 0 → f b a = f c c :=
+begin
+  intros [h₁, h₂],
+  unfold f at * ⊢,
+  state,
+  unfold f,
+  rewrite [add.comm, h₁, h₂],
+end

tests/lean/unfold.lean.expected.out

@@ -0,0 +1,22 @@
+unfold.lean:10:2: proof state
+a b : ℕ,
+h : a + b = 0
+⊢ f b a = 0
+unfold.lean:12:2: proof state
+a b : ℕ,
+h : a + b = 0
+⊢ b + a = 0
+unfold.lean:21:2: proof state
+a b : ℕ,
+h : a + b = 0
+⊢ b + a = 0
+unfold.lean:30:2: proof state
+a b c : ℕ,
+h₁ : c + c = 0,
+h₂ : a + b = 0
+⊢ f b a = f c c
+unfold.lean:39:2: proof state
+a b c : ℕ,
+h₁ : c + c = 0,
+h₂ : a + b = 0
+⊢ f b a = f c c