refactor(init/meta/interactive): merge generalize and generalize2 and introduce nicer syntax

doc/changes.md

@@ -90,6 +90,8 @@ For more details, see discussion [here](https://github.com/leanprover/lean/pull/
 
 * Universes `max u v + 1` and `imax u v + 1` are now parsed as `(max u v) + 1` and `(imax u v) + 1`.
 
+* Merged `generalize` and `generalize2` tactics into new `generalize id? : expr = id` tactic
+
 *API name changes*
 
 * `list.dropn` => `list.drop`

library/data/bitvec.lean

@@ -164,14 +164,14 @@ section conversion
     cases xs with xs P,
     simp [bits_to_nat_to_list], clear P,
     unfold bits_to_nat list.foldl,
-      -- the next 4 lines generalize the accumulator of foldl
-    let x := 0,
-    change _ = add_lsb x b + _,
-    generalize 0 y,
-    revert x, simp,
-    induction xs with x xs ; intro y,
-    { simp, unfold list.foldl add_lsb, simp [nat.mul_succ] },
-    { simp, apply ih_1 }
+    -- generalize the accumulator of foldl
+    have : ∀ x, list.foldl add_lsb x (xs ++ [b]) = add_lsb 0 b + list.foldl add_lsb x xs * 2, {
+      simp,
+      induction xs with x xs ; intro y,
+      { simp, unfold list.foldl add_lsb, simp [nat.mul_succ] },
+      { simp, apply ih_1 }
+    },
+    apply this
   end
 
   theorem bits_to_nat_to_bool (n : ℕ)

library/data/hash_map.lean

@@ -640,7 +640,7 @@ match (by apply_instance : decidable (contains_aux a bkt)) with
     have h : bkts'' = bkts'.as_list.foldl _ _, from bkts'.foldl_eq _ _,
     begin
       rw [← list.foldr_reverse] at h, rw h,
-      generalize bkts'.as_list.reverse l, intro l, induction l with a l IH,
+      generalize : bkts'.as_list.reverse = l, induction l with a l IH,
       { simp, rw[mk_as_list hash_fn n'], simp },
       { cases a with a'' b'', simp, rw [← IH], exact
         let B := l.foldr (λ y (x : bucket_array α β n'),

library/init/data/nat/bitwise.lean

@@ -203,17 +203,21 @@ namespace nat
     binary_rec z f (bit b n) = f b n (binary_rec z f n) :=
   begin
     rw [binary_rec],
-    by_cases bit b n = 0 with h'; simp [h'],
-    { generalize (binary_rec._main._pack._proof_1 (bit b n) h') e,
-      have bf := bodd_bit b n,
-      have n0 := div2_bit b n,
-      rw h' at bf n0,
-      simp at bf n0,
-      rw [← bf, ← n0, binary_rec_zero],
-      intros, exact h.symm },
-    { generalize (binary_rec._main._pack._proof_2 (bit b n)) e,
-      rw [bodd_bit, div2_bit],
-      intros, refl }
+    by_cases (bit b n = 0) with h',
+    {simp [dif_pos h'],
+     generalize : binary_rec._main._pack._proof_1 (bit b n) h' = e,
+     revert e,
+     have bf := bodd_bit b n,
+     have n0 := div2_bit b n,
+     rw h' at bf n0,
+     simp at bf n0,
+     rw [← bf, ← n0, binary_rec_zero],
+     intros, exact h.symm },
+    {simp [dif_neg h'],
+     generalize : binary_rec._main._pack._proof_2 (bit b n) = e,
+     revert e,
+     rw [bodd_bit, div2_bit],
+     intros, refl}
   end
 
   lemma bitwise_bit_aux {f : bool → bool → bool} (h : f ff ff = ff) :

library/init/meta/interactive.lean

@@ -455,16 +455,20 @@ do r   ← result,
 meta def destruct (p : parse texpr) : tactic unit :=
 i_to_expr p >>= tactic.destruct
 
-meta def generalize (p : parse parser.pexpr) (x : parse ident) : tactic unit :=
-do e ← i_to_expr p,
-   tactic.generalize e x
+private meta def generalize_arg_p : pexpr → parser (pexpr × name)
+| (app (app (macro _ [const `eq _ ]) h) (local_const x _ _ _)) := pure (h, x)
+| _ := fail "parse error"
 
-meta def generalize2 (p : parse parser.pexpr) (x : parse ident) (h : parse ident) : tactic unit :=
-do tgt ← target,
+/-- `generalize : e = x` replaces all occurrences of `e` in the target with a new hypothesis `x` of the same type.
+    `generalize h : e = x` in addition registers the hypothesis `h : e = x`. -/
+meta def generalize (h : parse ident?) (p : parse $ tk ":" *> with_desc "expr = id" (parser.pexpr 0 >>= generalize_arg_p)) : tactic unit :=
+do let (p, x) := p,
    e ← i_to_expr p,
+   some h ← pure h | tactic.generalize e x >> intro1 >> skip,
+   tgt ← target,
    -- if generalizing fails, fall back to not replacing anything
    tgt' ← do {
-     ⟨tgt', _⟩ ← solve_aux tgt (tactic.generalize e `_ >> target),
+     ⟨tgt', _⟩ ← solve_aux tgt (tactic.generalize e x >> target),
      to_expr ``(Π x, %%e = x → %%(tgt'.binding_body.lift_vars 0 1))
    } <|> to_expr ``(Π x, %%e = x → %%tgt),
    t ← assert h tgt',
@@ -479,7 +483,7 @@ do x ← mk_fresh_name,
    | []        := (`_h, [])
    | (h :: hs) := (h, hs)
    end : name × list name),
-   generalize2 p x h,
+   generalize h (p, x),
    t ← get_local x,
    induction (to_pexpr t) rec_name hs ([] : list name)
 

tests/lean/run/generalize_inst.lean

@@ -5,6 +5,6 @@ begin
   apply exists.intro,
   apply and.intro,
   apply rfl,
-  generalize 1 z,
-  exact nat.zero_le
+  generalize : 1 = z,
+  apply nat.zero_le
 end