feat(library/init/meta/simp_tactic): cleanup dunfold

Here are modifications:
- It fails if no definition is unfolded.
  See comment #1694 (comment)
  at issue #1694

- Users can provide configuration parameters.

- `dunfold_occs` was deleted.

doc/changes.md

@@ -44,7 +44,13 @@ For more details, see discussion [here](https://github.com/leanprover/lean/pull/
 * Add configuration object `rewrite_cfg` to `rw`/`rewrite` tactic. It now has support for `auto_param` and `opt_param`.
   The new goals are ordered using the same strategies available for `apply`.
 
-* All `dsimp` tactics fail if they did not change anything. We can simulate the v3.2.0 by using `dsimp {fail_if_unchaged := ff}`.
+* All `dsimp` tactics fail if they did not change anything.
+  We can simulate the v3.2.0 using `dsimp {fail_if_unchaged := ff}` or `try dsimp`.
+
+* All `dunfold` and `unfold` tactics fail if they did not unfold anything.
+  We can simulate the v3.2.0 using `unfold f {fail_if_unchaged := ff}` or `try {unfold f}`.
+
+* `dunfold_occs` was deleted, the new `conv` tactical should be used instead.
 
 v3.2.0 (18 June 2017)
 -------------

library/data/bitvec.lean

@@ -171,7 +171,7 @@ section conversion
     revert x, simp,
     induction xs with x xs ; intro y,
     { simp, unfold list.foldl add_lsb, simp [nat.mul_succ] },
-    { simp, unfold list.foldl, apply ih_1 }
+    { simp, apply ih_1 }
   end
 
   theorem bits_to_nat_to_bool (n : ℕ)

library/data/buffer/parser.lean

@@ -40,8 +40,8 @@ begin
 apply funext, intro input,
 apply funext, intro pos,
 dunfold parser.bind,
-cases (p input pos); dunfold bind,
-cases (q result input pos_1); dunfold bind,
+cases (p input pos); try {dunfold bind},
+cases (q result input pos_1); try {dunfold bind},
 all_goals {refl}
 end
 

library/init/data/int/bitwise.lean

@@ -183,7 +183,7 @@ namespace int
     all_goals {
       unfold cond, rw nat.bitwise_bit,
       repeat { rw bit_coe_nat <|> rw bit_neg_succ <|> rw bnot_bnot } },
-    all_goals { unfold bnot; rw h; refl }
+    all_goals { unfold bnot {fail_if_unchaged := ff}; rw h; refl }
   end
 
   @[simp] lemma lor_bit (a m b n) : lor (bit a m) (bit b n) = bit (a || b) (lor m n) :=

library/init/meta/interactive.lean

@@ -874,39 +874,28 @@ private meta def to_qualified_names : list name → tactic (list name)
 | []      := return []
 | (c::cs) := do new_c ← to_qualified_name c, new_cs ← to_qualified_names cs, return (new_c::new_cs)
 
-private meta def dunfold_hyps : list name → list name → tactic unit
-| cs []      := skip
-| cs (h::hs) := get_local h >>= dunfold_at cs >> dunfold_hyps cs hs
+private meta def dunfold_hyps (cs : list name) (cfg : dunfold_config) : list name → tactic unit
+| []      := skip
+| (h::hs) := do h' ← get_local h, dunfold_at cs h' cfg,  dunfold_hyps hs
 
-meta def dunfold : parse ident* → parse location → tactic unit
-| cs (loc.ns [])    := do new_cs ← to_qualified_names cs, tactic.dunfold new_cs
-| cs (loc.ns hs)    := do new_cs ← to_qualified_names cs, dunfold_hyps new_cs hs
-| cs (loc.wildcard) := do ls ← tactic.local_context,
+meta def dunfold (cs : parse ident*) (l : parse location) (cfg : dunfold_config := {}) : tactic unit :=
+match l with
+| (loc.ns [])    := do new_cs ← to_qualified_names cs, tactic.dunfold new_cs cfg
+| (loc.ns hs)    := do new_cs ← to_qualified_names cs, dunfold_hyps new_cs cfg hs
+| (loc.wildcard) := do ls ← tactic.local_context,
                           n ← revert_lst ls,
                           new_cs ← to_qualified_names cs,
-                          tactic.dunfold new_cs,
+                          tactic.dunfold new_cs cfg,
                           intron n
+end
 
 /- TODO(Leo): add support for non-refl lemmas -/
-meta def unfold : parse ident* → parse location → tactic unit :=
-dunfold
-
-private meta def dunfold_hyps_occs : name → occurrences → list name → tactic unit
-| c occs []  := skip
-| c occs (h::hs) := get_local h >>= dunfold_core_at occs [c] >> dunfold_hyps_occs c occs hs
-
-meta def dunfold_occs : parse ident → parse location → list nat → tactic unit
-| c (loc.ns []) ps    := do new_c ← to_qualified_name c, tactic.dunfold_occs_of ps new_c
-| c (loc.ns hs) ps    := do new_c ← to_qualified_name c, dunfold_hyps_occs new_c (occurrences.pos ps) hs
-| c (loc.wildcard) ps := fail "wildcard not allowed when unfolding occurences"
-
-/- TODO(Leo): add support for non-refl lemmas -/
-meta def unfold_occs : parse ident → parse location → list nat → tactic unit :=
-dunfold_occs
+meta def unfold (cs : parse ident*) (l : parse location) (cfg : dunfold_config := {}) : tactic unit :=
+dunfold cs l cfg
 
 private meta def delta_hyps : list name → list name → tactic unit
 | cs []      := skip
-| cs (h::hs) := get_local h >>= delta_at cs >> dunfold_hyps cs hs
+| cs (h::hs) := get_local h >>= delta_at cs >> delta_hyps cs hs
 
 meta def delta : parse ident* → parse location → tactic unit
 | cs (loc.ns [])    := do new_cs ← to_qualified_names cs, tactic.delta new_cs

library/init/meta/simp_tactic.lean

@@ -107,30 +107,22 @@ meta def dsimplify
                        (λ u e, do r ← post e, return (u, r)) e,
         return new_e
 
-meta constant dunfold_expr_core : transparency → expr → tactic expr
-
 /- Remark: we use transparency.instances by default to make sure that we
    can unfold projections of type classes. Example:
 
-          dunfold_expr (@has_add.add nat nat.has_add a b)
+          (@has_add.add nat nat.has_add a b)
 -/
 
-meta def dunfold_expr : expr → tactic expr :=
-dunfold_expr_core transparency.instances
-
-meta constant unfold_projection_core : transparency → expr → tactic expr
+/-- If `e` is a projection application, try to unfold it, otherwise fail. -/
+meta constant unfold_projection (e : expr) (md : transparency := transparency.instances) : tactic expr
 
-meta def unfold_projection : expr → tactic expr :=
-unfold_projection_core transparency.instances
+structure dunfold_config extends dsimp_config :=
+(md := transparency.instances)
 
-meta constant dunfold_occs_core (m : transparency) (max_steps : nat) (occs : occurrences) (cs : list name) (e : expr) : tactic expr
-meta constant dunfold_core (m : transparency) (max_steps : nat) (cs : list name) (e : expr) : tactic expr
+meta constant dunfold_core (cs : list name) (e : expr) (cfg : dunfold_config := {}) : tactic expr
 
-meta def dunfold : list name → tactic unit :=
-λ cs, target >>= dunfold_core transparency.instances default_max_steps cs >>= unsafe_change
-
-meta def dunfold_occs_of (occs : list nat) (c : name) : tactic unit :=
-target >>= dunfold_occs_core transparency.instances default_max_steps (occurrences.pos occs) [c] >>= unsafe_change
+meta def dunfold (cs : list name) (cfg : dunfold_config := {}) : tactic unit :=
+do t ← target, dunfold_core cs t cfg >>= unsafe_change
 
 meta def revert_and_transform (transform : expr → tactic expr) (h : expr) : tactic unit :=
 do num_reverted : ℕ ← revert h,
@@ -146,11 +138,8 @@ do num_reverted : ℕ ← revert h,
    end,
    intron num_reverted
 
-meta def dunfold_core_at (occs : occurrences) (cs : list name) : expr → tactic unit :=
-revert_and_transform (dunfold_occs_core transparency.instances default_max_steps occs cs)
-
-meta def dunfold_at (cs : list name) : expr → tactic unit :=
-revert_and_transform (dunfold_core transparency.instances default_max_steps cs)
+meta def dunfold_at (cs : list name) (h : expr) (cfg : dunfold_config := {}) : tactic unit :=
+revert_and_transform (λ e, dunfold_core cs e cfg) h
 
 structure delta_config :=
 (max_steps       := default_max_steps)
@@ -164,7 +153,7 @@ cs.any (λ c,
        f.is_constant && f.const_name.is_internal && (f.const_name.get_prefix = c))
 
 /-- Delta reduce the given constant names -/
-meta def delta_core (cfg : delta_config) (cs : list name) (e : expr) : tactic expr :=
+meta def delta_expr (cs : list name) (e : expr) (cfg : delta_config) : tactic expr :=
 let unfold (u : unit) (e : expr) : tactic (unit × expr × bool) := do
   guard (is_delta_target e cs),
   (expr.const f_name f_lvls) ← return e.get_app_fn,
@@ -177,23 +166,23 @@ in do (c, new_e) ← dsimplify_core () (λ c e, failed) unfold e {max_steps := c
       return new_e
 
 meta def delta (cs : list name) : tactic unit :=
-target >>= delta_core {} cs >>= unsafe_change
+do t ← target, delta_expr cs t {} >>= unsafe_change
 
 meta def delta_at (cs : list name) : expr → tactic unit :=
-revert_and_transform (delta_core {} cs)
+revert_and_transform (λ e, delta_expr cs e {})
 
-meta def unfold_projections_core (m : transparency) (max_steps : nat) (e : expr) : tactic expr :=
+meta def unfold_projections_core (e : expr) (md := transparency.instances) (max_steps : nat := default_max_steps) : tactic expr :=
 let unfold (changed : bool) (e : expr) : tactic (bool × expr × bool) := do
-  new_e ← unfold_projection_core m e,
+  new_e ← unfold_projection e md,
   return (tt, new_e, tt)
-in do (tt, new_e) ← dsimplify_core ff (λ c e, failed) unfold e | fail "no projections to unfold",
+in do (tt, new_e) ← dsimplify_core ff (λ c e, failed) unfold e {max_steps := max_steps, md := md} | fail "no projections to unfold",
       return new_e
 
-meta def unfold_projections : tactic unit :=
-target >>= unfold_projections_core semireducible default_max_steps >>= change
+meta def unfold_projections (md := transparency.instances) (max_steps : nat := default_max_steps) : tactic unit :=
+do t ← target, unfold_projections_core t md max_steps >>= unsafe_change
 
-meta def unfold_projections_at : expr → tactic unit :=
-revert_and_transform (unfold_projections_core semireducible default_max_steps)
+meta def unfold_projections_at (h : expr) (md := transparency.instances) (max_steps : nat := default_max_steps) : tactic unit :=
+revert_and_transform (λ e, unfold_projections_core e md max_steps) h
 
 structure simp_config :=
 (max_steps : nat           := default_max_steps)

library/init/meta/well_founded_tactics.lean

@@ -36,7 +36,7 @@ meta def clear_internals : tactic unit :=
 local_context >>= clear_wf_rec_goal_aux
 
 meta def unfold_wf_rel : tactic unit :=
-dunfold [``has_well_founded.r]
+dunfold [``has_well_founded.r] {fail_if_unchaged := ff}
 
 meta def is_psigma_mk : expr → tactic (expr × expr)
 | `(psigma.mk %%a %%b) := return (a, b)
@@ -57,7 +57,7 @@ meta def process_lex : tactic unit → tactic unit
      tac
 
 private meta def unfold_sizeof_measure : tactic unit :=
-dunfold [``sizeof_measure, ``measure, ``inv_image]
+dunfold [``sizeof_measure, ``measure, ``inv_image] {fail_if_unchaged := ff}
 
 private meta def add_simps : simp_lemmas → list name → tactic simp_lemmas
 | s []      := return s
@@ -77,7 +77,7 @@ e.mfold simp_lemmas.mk $ λ c d s,
 
 private meta def unfold_sizeof_loop : tactic unit :=
 do
-  dunfold [``sizeof, ``has_sizeof.sizeof],
+  dunfold [``sizeof, ``has_sizeof.sizeof] {fail_if_unchaged := ff},
   S ← target >>= collect_sizeof_lemmas,
   (simplify_goal S >> unfold_sizeof_loop)
   <|>

src/library/tactic/unfold_tactic.cpp

@@ -18,7 +18,7 @@ Author: Leonardo de Moura
 #include "library/tactic/dsimplify.h"
 
 namespace lean {
-vm_obj tactic_unfold_projection_core(vm_obj const & m, vm_obj const & _e, vm_obj const & _s) {
+vm_obj tactic_unfold_projection(vm_obj const & _e, vm_obj const & m, vm_obj const & _s) {
     expr const & e = to_expr(_e);
     tactic_state const & s = tactic::to_state(_s);
     try {
@@ -60,42 +60,6 @@ optional<expr> dunfold(type_context & ctx, expr const & e) {
     }
 }
 
-vm_obj tactic_dunfold_expr_core(vm_obj const & m, vm_obj const & _e, vm_obj const & _s) {
-    expr const & e = to_expr(_e);
-    tactic_state const & s = tactic::to_state(_s);
-    try {
-        environment const & env = s.env();
-        expr const & fn = get_app_fn(e);
-        if (!is_constant(fn))
-            return tactic::mk_exception("dunfold_expr failed, expression is not a constant nor a constant application", s);
-        if (is_projection(s.env(), const_name(fn))) {
-            type_context ctx = mk_type_context_for(s, to_transparency_mode(m));
-            if (auto new_e = ctx.reduce_projection(e))
-                return tactic::mk_success(to_obj(*new_e), s);
-            return tactic::mk_exception("dunfold_expr failed, failed to unfold projection", s);
-        } else if (has_eqn_lemmas(env, const_name(fn))) {
-            type_context ctx = mk_type_context_for(s, to_transparency_mode(m));
-            if (auto new_e = dunfold(ctx, e)) {
-                return tactic::mk_success(to_obj(*new_e), s);
-            } else {
-                return tactic::mk_exception("dunfold_expr failed, none of the rfl lemmas is applicable", s);
-            }
-        } else if (auto new_e = unfold_term(env, e)) {
-            return tactic::mk_success(to_obj(*new_e), s);
-        } else {
-            return tactic::mk_exception("dunfold_expr failed, failed to unfold", s);
-        }
-    } catch (exception & ex) {
-        return tactic::mk_exception(ex, s);
-    }
-}
-
-static dsimp_config mk_dsimp_cfg(unsigned max_steps) {
-    dsimp_config cfg;
-    cfg.m_max_steps = max_steps;
-    return cfg;
-}
-
 class unfold_core_fn : public dsimplify_core_fn {
 protected:
     name_set    m_cs;
@@ -125,12 +89,12 @@ class unfold_core_fn : public dsimplify_core_fn {
             return none();
         if (!check_occ())
             return none();
-        return optional<pair<expr, bool>>(*new_e, true);
+        return optional<pair<expr, bool>>(*new_e, !m_cfg.m_single_pass);
     }
 
 public:
-    unfold_core_fn(type_context & ctx, defeq_canonizer::state & dcs, unsigned max_steps, list<name> const & cs):
-        dsimplify_core_fn(ctx, dcs, mk_dsimp_cfg(max_steps)),
+    unfold_core_fn(type_context & ctx, defeq_canonizer::state & dcs, list<name> const & cs, dsimp_config const & cfg):
+        dsimplify_core_fn(ctx, dcs, cfg),
         m_cs(to_name_set(cs)) {
     }
 };
@@ -140,69 +104,38 @@ class unfold_fn : public unfold_core_fn {
         return unfold_step(e);
     }
 public:
-    unfold_fn(type_context & ctx, defeq_canonizer::state & dcs, unsigned max_steps, list<name> const & cs):
-        unfold_core_fn(ctx, dcs, max_steps, cs) {
-    }
-};
-
-class unfold_occs_fn : public unfold_core_fn {
-    occurrences m_occs;
-    unsigned    m_counter{1};
-
-    virtual bool check_occ() override {
-        bool r = m_occs.contains(m_counter);
-        m_counter++;
-        return r;
-    }
-
-    virtual optional<pair<expr, bool>> pre(expr const & e) override {
-        return unfold_step(e);
-    }
-
-public:
-    unfold_occs_fn(type_context & ctx, defeq_canonizer::state & dcs, unsigned max_steps,
-                   occurrences const & occs, list<name> const & cs):
-        unfold_core_fn(ctx, dcs, max_steps, cs),
-        m_occs(occs) {
+    unfold_fn(type_context & ctx, defeq_canonizer::state & dcs, list<name> const & cs, dsimp_config const & cfg):
+        unfold_core_fn(ctx, dcs, cs, cfg) {
     }
 };
 
-vm_obj tactic_dunfold_core(vm_obj const & m, vm_obj const & max_steps, vm_obj const & cs, vm_obj const & _e, vm_obj const & _s) {
+vm_obj tactic_dunfold_core(vm_obj const & cs, vm_obj const & _e, vm_obj const & _cfg, vm_obj const & _s) {
     expr const & e         = to_expr(_e);
     tactic_state const & s = tactic::to_state(_s);
     defeq_can_state dcs    = s.dcs();
-    type_context ctx       = mk_type_context_for(s, to_transparency_mode(m));
-    unfold_fn F(ctx, dcs, force_to_unsigned(max_steps), to_list_name(cs));
+    /*
+       structure dunfold_config extends dsimp_config :=
+       (md := transparency.instances) -- this is not a new field.
+    */
+    dsimp_config cfg(_cfg);
+    type_context ctx       = mk_type_context_for(s, cfg.m_md);
+    unfold_fn F(ctx, dcs, to_list_name(cs), cfg);
     try {
         expr new_e         = F(e);
         tactic_state new_s = set_mctx_dcs(s, F.mctx(), dcs);
-        return tactic::mk_success(to_obj(new_e), new_s);
-    } catch (exception & ex) {
-        return tactic::mk_exception(ex, s);
-    }
-}
-
-vm_obj tactic_dunfold_occs_core(vm_obj const & m, vm_obj const & max_steps, vm_obj const & occs, vm_obj const & cs,
-                                vm_obj const & _e, vm_obj const & _s) {
-    expr const & e         = to_expr(_e);
-    tactic_state const & s = tactic::to_state(_s);
-    defeq_can_state dcs    = s.dcs();
-    type_context ctx       = mk_type_context_for(s, to_transparency_mode(m));
-    unfold_occs_fn F(ctx, dcs, force_to_unsigned(max_steps), to_occurrences(occs), to_list_name(cs));
-    try {
-        expr new_e         = F(e);
-        tactic_state new_s = set_mctx_dcs(s, F.mctx(), dcs);
-        return tactic::mk_success(to_obj(new_e), new_s);
+        if (cfg.m_fail_if_unchanged && e == new_e) {
+            return tactic::mk_exception("dunfold tactic failed to unfold", s);
+        } else {
+            return tactic::mk_success(to_obj(new_e), new_s);
+        }
     } catch (exception & ex) {
         return tactic::mk_exception(ex, s);
     }
 }
 
 void initialize_unfold_tactic() {
-    DECLARE_VM_BUILTIN(name({"tactic", "unfold_projection_core"}), tactic_unfold_projection_core);
-    DECLARE_VM_BUILTIN(name({"tactic", "dunfold_expr_core"}),      tactic_dunfold_expr_core);
-    DECLARE_VM_BUILTIN(name({"tactic", "dunfold_core"}),           tactic_dunfold_core);
-    DECLARE_VM_BUILTIN(name({"tactic", "dunfold_occs_core"}),      tactic_dunfold_occs_core);
+    DECLARE_VM_BUILTIN(name({"tactic", "unfold_projection"}),  tactic_unfold_projection);
+    DECLARE_VM_BUILTIN(name({"tactic", "dunfold_core"}),       tactic_dunfold_core);
 }
 
 void finalize_unfold_tactic() {