fix(library/init/meta/tactic): use zeta reduction by default in the abstract tactic

Abstracting let-exprs may produce type errors.
In the future we may consider another strategy for `abstract`.
First, we try to abstract the `let`, then if it fails, we expand.
Not sure if this is a good idea.

library/data/hash_map.lean

@@ -16,10 +16,11 @@ structure hash_map (α : Type u) [decidable_eq α] (β : α → Type v) :=
 
 def mk_hash_map {α : Type u} [decidable_eq α] {β : α → Type v} (hash_fn : α → nat) (nbuckets := 8) : hash_map α β :=
 let n := if nbuckets = 0 then 8 else nbuckets in
-{hash_fn := hash_fn, size := 0, nbuckets := n,
- -- TODO(Leo): abstract doesn't work in the followin line
- nz_buckets := by {dsimp, cases nbuckets, {simp, tactic.comp_val}, simp [if_pos, nat.succ_ne_zero], apply nat.zero_lt_succ},
- buckets := mk_array n [] }
+{hash_fn    := hash_fn,
+ size       := 0,
+ nbuckets   := n,
+ nz_buckets := by abstract {dsimp, cases nbuckets, {simp, tactic.comp_val}, simp [if_pos, nat.succ_ne_zero], apply nat.zero_lt_succ},
+ buckets    := mk_array n [] }
 
 namespace hash_map
 variables {α : Type u} {β : α → Type v} {δ : Type w}

library/init/meta/tactic.lean

@@ -898,10 +898,10 @@ private meta def mk_aux_decl_name : option name → tactic name
 | none          := new_aux_decl_name
 | (some suffix) := do p ← decl_name, return $ p ++ suffix
 
-meta def abstract (tac : tactic unit) (suffix : option name := none) : tactic unit :=
+meta def abstract (tac : tactic unit) (suffix : option name := none) (zeta_reduce := tt) : tactic unit :=
 do fail_if_no_goals,
    gs ← get_goals,
-   type ← target,
+   type ← if zeta_reduce then target >>= zeta else target,
    is_lemma ← is_prop type,
    m ← mk_meta_var type,
    set_goals [m],
@@ -910,6 +910,7 @@ do fail_if_no_goals,
    when (n ≠ 0) (fail "abstract tactic failed, there are unsolved goals"),
    set_goals gs,
    val ← instantiate_mvars m,
+   val ← if zeta_reduce then zeta val else return val,
    c   ← mk_aux_decl_name suffix,
    e   ← add_aux_decl c type val is_lemma,
    exact e

tests/lean/1293.lean.expected.out

@@ -4,7 +4,7 @@ state:
 1293.lean:5:21: error: tactic 'whnf' failed, given expression should not contain de-Bruijn variables, they should be replaced with local constants before using this tactic
 state:
 ⊢ true
-1293.lean:7:21: error: tactic 'zeta' failed, given expression should not contain de-Bruijn variables, they should be replaced with local constants before using this tactic
+1293.lean:7:21: error: tactic 'head_zeta' failed, given expression should not contain de-Bruijn variables, they should be replaced with local constants before using this tactic
 state:
 ⊢ true
 1293.lean:9:21: error: tactic 'unify' failed, given expression should not contain de-Bruijn variables, they should be replaced with local constants before using this tactic