feat(library/init/meta/interactive): merge ginduction and induction

This commit is based on 638b34b16de6443.
The changes were applied manually to make sure all changes are
compatible with our plans to `induction`.

doc/changes.md

@@ -117,6 +117,8 @@ master branch (aka work in progress branch)
   In this case, `apply t` behaves as `apply t _ ... _` where `n` `_` have been added, independently of the goal target type.
   The new behavior is useful when using `apply` with eliminator-like definitions.
 
+- `ginduction t with h h1 h2` is now `induction h : t with h1 h2`.
+
 *API name changes*
 
 v3.3.0 (14 September 2017)

library/init/data/bool/lemmas.lean

@@ -126,7 +126,7 @@ theorem of_to_bool_ff {p : Prop} [decidable p] : to_bool p = ff → ¬p := (to_b
 
 theorem to_bool_congr {p q : Prop} [decidable p] [decidable q] (h : p ↔ q) : to_bool p = to_bool q :=
 begin
-  ginduction to_bool q with h',
+  induction h' : to_bool q,
   exact to_bool_ff (mt h.1 $ of_to_bool_ff h'),
   exact to_bool_true (h.2 $ of_to_bool_true h')
 end

library/init/data/list/qsort.lean

@@ -14,7 +14,7 @@ def qsort.F {α} (lt : α → α → bool) : Π (x : list α),
   (Π (y : list α), length y < length x → list α) → list α
 | []     IH := []
 | (h::t) IH := begin
-    ginduction partition (λ x, lt h x = tt) t with e large small,
+    induction e : partition (λ x, lt h x = tt) t with large small,
     have : length small < length (h::t) ∧ length large < length (h::t),
     { rw partition_eq_filter_filter at e,
       injection e,
@@ -38,7 +38,7 @@ by rw [qsort, well_founded.fix_eq, qsort.F]
   qsort lt small ++ h :: qsort lt large :=
 begin
   rw [qsort, well_founded.fix_eq, qsort.F],
-  ginduction partition (λ x, lt h x = tt) t with e large small,
+  induction e : partition (λ x, lt h x = tt) t with large small,
   simp [e], rw [e]
 end
 

library/init/data/nat/bitwise.lean

@@ -235,7 +235,7 @@ lemma bitwise_bit_aux {f : bool → bool → bool} (h : f ff ff = ff) :
 begin
   funext n,
   apply bit_cases_on n, intros b n, rw [binary_rec_eq],
-  { cases b; try {rw h}; ginduction f ff tt with fft; simp [cond]; refl },
+  { cases b; try {rw h}; induction fft : f ff tt; simp [cond]; refl },
   { rw [h, show cond (f ff tt) 0 0 = 0, by cases f ff tt; refl,
            show cond (f tt ff) (bit ff 0) 0 = 0, by cases f tt ff; refl]; refl }
 end
@@ -258,7 +258,7 @@ by rw bitwise_zero_left; cases f ff tt; refl
 begin
   unfold bitwise,
   rw [binary_rec_eq, binary_rec_eq],
-  { ginduction f tt ff with ftf; dsimp [cond],
+  { induction ftf : f tt ff; dsimp [cond],
     rw [show f a ff = ff, by cases a; assumption],
     apply @congr_arg _ _ _ 0 (bit ff), tactic.swap,
     rw [show f a ff = a, by cases a; assumption],

library/init/data/nat/lemmas.lean

@@ -894,7 +894,7 @@ theorem succ_inj {n m : ℕ} (H : succ n = succ m) : n = m :=
 nat.succ.inj_arrow H id
 
 theorem discriminate {B : Sort u} {n : ℕ} (H1: n = 0 → B) (H2 : ∀m, n = succ m → B) : B :=
-by ginduction n with h; [exact H1 h, exact H2 _ h]
+by induction h : n; [exact H1 h, exact H2 _ h]
 
 theorem one_succ_zero : 1 = succ 0 := rfl
 

library/init/meta/interactive.lean

@@ -378,6 +378,44 @@ do e_type ← infer_type e >>= whnf,
    (const I ls) ← return $ get_app_fn e_type,
    return I
 
+private meta def generalize_arg_p_aux : pexpr → parser (pexpr × name)
+| (app (app (macro _ [const `eq _ ]) h) (local_const x _ _ _)) := pure (h, x)
+| _ := fail "parse error"
+
+
+private meta def generalize_arg_p : parser (pexpr × name) :=
+with_desc "expr = id" $ parser.pexpr 0 >>= generalize_arg_p_aux
+
+/--
+`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?) (_ : parse $ tk ":") (p : parse 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 x >> target),
+     to_expr ``(Π x, %%e = x → %%(tgt'.binding_body.lift_vars 0 1))
+   } <|> to_expr ``(Π x, %%e = x → %%tgt),
+   t ← assert h tgt',
+   swap,
+   exact ``(%%t %%e rfl),
+   intro x,
+   intro h
+
+meta def cases_arg_p : parser (option name × pexpr) :=
+with_desc "(id :)? expr" $ do
+  t ← texpr,
+  match t with
+  | (local_const x _ _ _) :=
+    (tk ":" *> do t ← texpr, pure (some x, t)) <|> pure (none, t)
+  | _ := pure (none, t)
+  end
+
 precedence `generalizing` : 0
 
 /--
@@ -392,14 +430,24 @@ For example, given `n : nat` and a goal with a hypothesis `h : P n` and target `
 `induction e using r` allows the user to specify the principle of induction that should be used. Here `r` should be a theorem whose result type must be of the form `C t`, where `C` is a bound variable and `t` is a (possibly empty) sequence of bound variables
 
 `induction e generalizing z₁ ... zₙ`, where `z₁ ... zₙ` are variables in the local context, generalizes over `z₁ ... zₙ` before applying the induction but then introduces them in each goal. In other words, the net effect is that each inductive hypothesis is generalized.
+
+`induction h : t` will introduce an equality of the form `h : t = C x y`, asserting that the input term is equal to the current constructor case, to the context.
 -/
-meta def induction (p : parse texpr) (rec_name : parse using_ident) (ids : parse with_ident_list)
+meta def induction (hp : parse cases_arg_p) (rec_name : parse using_ident) (ids : parse with_ident_list)
   (revert : parse $ (tk "generalizing" *> ident*)?) : tactic unit :=
-do e ← i_to_expr p,
+do
+    -- process `h : t` case
+    e ← match hp with
+       | (some h, p) := do
+         x ← mk_fresh_name,
+         generalize h () (p, x),
+         get_local x
+       | (none, p) := i_to_expr p
+       end,
 
    -- generalize major premise
    e ← if e.is_local_constant then pure e
-   else generalize e >> intro1,
+       else tactic.generalize e >> intro1,
 
    -- generalize major premise args
    (e, newvars, locals) ← do {
@@ -534,50 +582,6 @@ For example, given `n : nat` and a goal with a hypothesis `h : P n` and target `
 meta def destruct (p : parse texpr) : tactic unit :=
 i_to_expr p >>= tactic.destruct
 
-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"
-
-/--
-`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 x >> target),
-     to_expr ``(Π x, %%e = x → %%(tgt'.binding_body.lift_vars 0 1))
-   } <|> to_expr ``(Π x, %%e = x → %%tgt),
-   t ← assert h tgt',
-   swap,
-   exact ``(%%t %%e rfl),
-   intro x,
-   intro h
-
-meta def ginduction (p : parse texpr) (rec_name : parse using_ident) (ids : parse with_ident_list) : tactic unit :=
-do x ← mk_fresh_name,
-   let (h, hs) := (match ids with
-   | []        := (`_h, [])
-   | (h :: hs) := (h, hs)
-   end : name × list name),
-   generalize h (p, x),
-   t ← get_local x,
-   induction (to_pexpr t) rec_name hs ([] : list name)
-
-private meta def cases_arg_p : parser (option name × pexpr) :=
-with_desc "(id :)? expr" $ do
-  t ← texpr,
-  match t with
-  | (local_const x _ _ _) :=
-    (tk ":" *> do t ← texpr, pure (some x, t)) <|> pure (none, t)
-  | _ := pure (none, t)
-  end
-
 /--
 Assuming `x` is a variable in the local context with an inductive type, `cases x` splits the main goal, producing one goal for each constructor of the inductive type, in which the target is replaced by a general instance of that constructor. If the type of an element in the local context depends on `x`, that element is reverted and reintroduced afterward, so that the case split affects that hypothesis as well.
 
@@ -595,7 +599,7 @@ meta def cases : parse cases_arg_p → parse with_ident_list → tactic unit
   tactic.cases e ids
 | (some h, p) ids := do
   x   ← mk_fresh_name,
-  generalize h (p, x),
+  generalize h () (p, x),
   hx  ← get_local x,
   tactic.cases hx ids
 

library/init/meta/smt/interactive.lean

@@ -229,7 +229,7 @@ smt_tactic.iterate t
 meta def all_goals (t : itactic) : smt_tactic unit :=
 smt_tactic.all_goals t
 
-meta def induction (p : parse texpr) (rec_name : parse using_ident) (ids : parse with_ident_list)
+meta def induction (p : parse tactic.interactive.cases_arg_p) (rec_name : parse using_ident) (ids : parse with_ident_list)
   (revert : parse $ (tk "generalizing" *> ident*)?) : smt_tactic unit :=
 slift (tactic.interactive.induction p rec_name ids revert)