feat(library/init/meta/interactive): unfold is now based on the simp framework

See issue #1694.

There is an orthogonal issue. `simp` (and consequently `unfold`) cannot be used to
reduce projections (e.g., `has_add.add`). This issue has been
previously raised by @Armael, but it was not addressed yet.

doc/changes.md

@@ -59,6 +59,12 @@ For more details, see discussion [here](https://github.com/leanprover/lean/pull/
 
 * `dunfold_occs` was deleted, the new `conv` tactical should be used instead.
 
+* `unfold` tactic is now implemented on top of the `simp` tactics. So, we can use it to unfold
+   declarations defined using well founded recursion. The `unfold1` variant does not unfold recursively,
+   and it is shorthand for `unfold f {single_pass := tt}`.
+   Remark: in v3.2.0, `unfold` was just an alias for the `dunfold` tactic.
+
+
 v3.2.0 (18 June 2017)
 -------------
 

library/init/algebra/ring.lean

@@ -59,7 +59,7 @@ section semiring
   variables [semiring α]
 
   lemma one_add_one_eq_two : 1 + 1 = (2 : α) :=
-  begin unfold bit0, reflexivity end
+  by unfold bit0
 
   theorem two_mul (n : α) : 2 * n = n + n :=
   eq.trans (right_distrib 1 1 n) (by simp)

library/init/data/int/bitwise.lean

@@ -31,14 +31,14 @@ namespace int
   by cases n; simp; refl
 
   @[simp] lemma bodd_neg (n : ℤ) : bodd (-n) = bodd n :=
-  by cases n; unfold has_neg.neg; simp [int.coe_nat_eq, int.neg, bodd]
+  by cases n; dunfold has_neg.neg; simp [int.coe_nat_eq, int.neg, bodd]
 
   @[simp] lemma bodd_add (m n : ℤ) : bodd (m + n) = bxor (bodd m) (bodd n) :=
-  by cases m with m m; cases n with n n; unfold has_add.add; simp [int.add, bodd];
+  by cases m with m m; cases n with n n; dunfold has_add.add; simp [int.add, bodd];
      cases m.bodd; cases n.bodd; refl
 
   @[simp] lemma bodd_mul (m n : ℤ) : bodd (m * n) = bodd m && bodd n :=
-  by cases m with m m; cases n with n n; unfold has_mul.mul; simp [int.mul, bodd];
+  by cases m with m m; cases n with n n; dunfold has_mul.mul; simp [int.mul, bodd];
      cases m.bodd; cases n.bodd; refl
 
   theorem bodd_add_div2 : ∀ n, cond (bodd n) 1 0 + 2 * div2 n = n

library/init/meta/converter/conv.lean

@@ -16,13 +16,13 @@ meta def conv (α : Type u) :=
 tactic α
 
 meta instance : monad conv :=
-by unfold conv; apply_instance
+by dunfold conv; apply_instance
 
 meta instance : monad_fail conv :=
-by unfold conv; apply_instance
+by dunfold conv; apply_instance
 
 meta instance : alternative conv :=
-by unfold conv; apply_instance
+by dunfold conv; apply_instance
 
 namespace conv
 meta def convert (c : conv unit) (lhs : expr) (rel : name := `eq) : tactic (expr × expr) :=

library/init/meta/expr.lean

@@ -233,11 +233,11 @@ meta def ith_arg_aux : expr → nat → expr
 meta def ith_arg (e : expr) (i : nat) : expr :=
 ith_arg_aux e (get_app_num_args e - i - 1)
 
-meta def const_name : expr → name
+meta def const_name : expr elab → name
 | (const n ls) := n
 | e            := name.anonymous
 
-meta def is_constant : expr → bool
+meta def is_constant : expr elab → bool
 | (const n ls) := tt
 | e            := ff
 

library/init/meta/interactive.lean

@@ -723,9 +723,9 @@ private meta def simp_hyps (cfg : simp_config) (discharger : tactic unit) : simp
 | s []      := skip
 | s (h::hs) := simp_hyp cfg discharger s h >> simp_hyps s hs
 
-private meta def simp_core (cfg : simp_config) (discharger : tactic unit)
-                           (no_dflt : bool) (ctx : list expr) (hs : list pexpr) (attr_names : list name) (ids : list name)
-                           (locat : loc) : tactic unit :=
+meta def simp_core (cfg : simp_config) (discharger : tactic unit)
+                   (no_dflt : bool) (ctx : list expr) (hs : list pexpr) (attr_names : list name) (ids : list name)
+                   (locat : loc) : tactic unit :=
 do s ← mk_simp_set no_dflt attr_names hs ids,
    s ← s.append ctx,
    match locat : _ → tactic unit with
@@ -899,10 +899,6 @@ match l with
                           intron n
 end
 
-/- TODO(Leo): add support for non-refl lemmas -/
-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 >> delta_hyps cs hs
@@ -928,6 +924,34 @@ meta def unfold_projections : parse location → tactic unit
 | (loc.ns hs)    := unfold_projections_hyps hs
 | (loc.wildcard) := do ls ← local_context, unfold_projections_hyps (ls.map expr.local_pp_name)
 
+end interactive
+
+meta def ids_to_pexprs (tac_name : name) (cs : list name) : tactic (list pexpr) :=
+cs.mmap $ λ c, do
+  n   ← resolve_name c,
+  hs  ← get_eqn_lemmas_for ff n.const_name,
+  env ← get_env,
+  let p := env.is_projection n.const_name,
+  when (hs.empty ∧ p.is_none) (fail (sformat! "{tac_name} tactic failed, {c} does not have equational lemmas nor is a projection")),
+  return (expr.const c [])
+
+structure unfold_config extends simp_config :=
+(zeta               := ff)
+(proj               := ff)
+(eta                := ff)
+(canonize_instances := ff)
+
+namespace interactive
+open interactive interactive.types expr
+
+meta def unfold (cs : parse ident*) (locat : parse location) (cfg : unfold_config := {}) : tactic unit :=
+do es ← ids_to_pexprs "unfold" cs,
+   let no_dflt := tt,
+   simp_core cfg.to_simp_config failed no_dflt [] es [] [] locat
+
+meta def unfold1 (cs : parse ident*) (locat : parse location) (cfg : unfold_config := {single_pass := tt}) : tactic unit :=
+unfold cs locat cfg
+
 meta def apply_opt_param : tactic unit :=
 tactic.apply_opt_param
 

tests/lean/1603.lean

@@ -4,6 +4,6 @@ def some_lets : ℕ → ℕ → ℕ
 
 def some_unfolded_lets (n : ℕ) : ∃ v : ℕ , v = some_lets 5 n :=
 begin
-  unfold some_lets,
+  dunfold some_lets,
   -- admit
 end

tests/lean/1639.lean

@@ -4,7 +4,7 @@ def some_lets : ℕ → ℕ → ℕ
 
 def some_unfolded_lets (n : ℕ) : Σ' v : ℕ , v = some_lets 5 n :=
 begin
-  econstructor; unfold some_lets; econstructor
+  econstructor; dunfold some_lets; econstructor
 end
 
 meta def foo : tactic unit :=
@@ -12,7 +12,7 @@ meta def foo : tactic unit :=
      tactic.to_expr (``(1)) >>= tactic.unify g
 def some_lifted_lets (n : ℕ) : Σ' (v : ℕ), v = psigma.fst (some_unfolded_lets n) :=
 begin
-  econstructor; unfold some_unfolded_lets psigma.fst; symmetry; transitivity; symmetry;
+  econstructor; dunfold some_unfolded_lets psigma.fst; symmetry; transitivity; symmetry;
   {
     foo -- unify_reify_rhs_to_let_in
   }

tests/lean/run/and_rec_code_gen_issue.lean

@@ -60,8 +60,7 @@ do 0  ::= 1,
 lemma size_write (b : buffer nat) (i : nat) (h : i < b.size) (v : nat) : (b.write ⟨i, h⟩ v).size = b.size :=
 begin
   cases b,
-  unfold buffer.write buffer.size,
-  simp
+  unfold buffer.write buffer.size
 end
 
 open nat
@@ -75,7 +74,7 @@ lemma init_mem_inv : ∀ n (b : buffer nat), n < b.size → (init_mem n).pre b
 | (nat.succ n) b h :=
   have n < b.size, from nat.lt_of_succ_lt h,
   begin
-    unfold init_mem has_bind.and_then bind has_bind.bind hoare_state.bind, simp,
+    dunfold init_mem has_bind.and_then bind has_bind.bind hoare_state.bind, simp,
     split,
     {unfold hoare_state.assign, simp, exact h},
     {intros _ _,

tests/lean/run/dunfold3.lean

@@ -6,7 +6,7 @@ example (a b : nat) (p : nat → Prop) (h : p (g (nat.succ (nat.succ a)))) : p (
 begin
   unfold g at h,
   do { h ← get_local `h >>= infer_type, t ← to_expr ```(p (nat.succ (nat.succ a) + 5)), guard (h = t) },
-  unfold has_add.add bit0 has_one.one nat.add,
+  dunfold has_add.add bit0 has_one.one nat.add,
   unfold g,
   do { t ← target, h ← get_local `h >>= infer_type, guard (t = h) },
   assumption

tests/lean/run/inductive_nonrec_after_rec.lean

@@ -63,7 +63,7 @@ lemma ex7 {α : Type u} (t : tree α) : t ≠ leaf → tree.size t > 0 :=
 begin
   induction t,
   {intros, contradiction},
-  {intros, unfold size, apply nat.zero_lt_succ }
+  {intros, unfold tree.size, apply nat.zero_lt_succ }
 end
 
 inductive tree_list (α : Type u) : Type u

tests/lean/run/resolve_name_bug.lean

@@ -14,9 +14,7 @@ def g (a : nat) := a + 1
 
 example : g 0 = 1 :=
 begin
-  unfold g,
-  (target >>= check_expr ``(0 + 1 = 1)),
-  reflexivity
+  unfold g
 end
 
 example : f (f 0) = 2 :=

tests/lean/run/u_eq_max_u_v.lean

@@ -44,7 +44,7 @@ definition semigroup_morphism_product
     begin
       -- cf https://groups.google.com/d/msg/lean-user/bVs5FdjClp4/tfHiVjLIBAAJ
       intros,
-      unfold has_mul.mul,
+      dunfold has_mul.mul,
       dsimp,
       simp
     end

tests/lean/run/unfold_issue.lean

@@ -7,7 +7,5 @@ do e ← tactic.to_expr p, guard (t = e)
 
 example (n : nat): f (n+1) n = n + 1 :=
 begin
-  unfold f,
-  (tactic.target >>= check_expr ```((n + 1 = n + 1))),
-  reflexivity,
+  unfold f
 end