feat(library/tactic/induction_tactic): clear hypothesis before introducing new ones

library/init/data/list/instances.lean

@@ -72,7 +72,7 @@ lemma mem_bind {b : β} {l : list α} {f : α → list β} {a} (al : a ∈ l) (h
 mem_bind_iff.2 ⟨a, al, h⟩
 
 instance decidable_bex : ∀ (l : list α), decidable (∃ x ∈ l, p x)
-| [] := is_false (by intro; cases a; cases a_2; cases a)
+| [] := is_false (by intro; cases a; cases a_1; cases a_1)
 | (x::xs) :=
   if hx : p x then
     is_true ⟨x, or.inl rfl, hx⟩

src/library/tactic/induction_tactic.cpp

@@ -272,9 +272,11 @@ list<expr> induction(environment const & env, options const & opts, transparency
                 unsigned nextra  = to_revert.size() - indices.size() - 1; /* extra dependencies that have been reverted */
                 expr new_M       = ctx2.mk_metavar_decl(ctx2.lctx(), annotated_head_beta_reduce(new_type));
                 expr aux_M;
+                /* Clear hypothesis in the new goal. */
+                set_clear(aux_M, ctx2, new_M, H2);
                 buffer<name> param_names; buffer<name> extra_names;
                 /* Introduce constructor parameter for new goal associated with minor premise. */
-                set_intron(aux_M, ctx2, new_M, nparams, ns, param_names, true);
+                set_intron(aux_M, ctx2, aux_M, nparams, ns, param_names, true);
                 /* Introduce hypothesis that had to be reverted because they depended on indices and/or major premise. */
                 set_intron(aux_M, ctx2, aux_M, nextra, extra_names, false);
                 local_context aux_M_lctx = ctx2.mctx().get_metavar_decl(aux_M).get_context();
@@ -294,8 +296,6 @@ list<expr> induction(environment const & env, options const & opts, transparency
                     }
                     subst_buffer.push_back(S);
                 }
-                /* Clear hypothesis in the new goal. */
-                set_clear(aux_M, ctx2, aux_M, H2);
                 new_goals.push_back(aux_M);
                 rec_arg = new_M;
             }

tests/lean/cases_induction_fresh.lean

@@ -7,6 +7,15 @@ begin
   constructor; assumption
 end
 
+example (p q r s: Prop): p ∧ q → r ∧ s → s ∧ q :=
+begin
+  intros a a_1,
+  cases a,
+  cases a_1,
+  trace_state,
+  constructor; assumption
+end
+
 #print "------------"
 
 example (p q r s: Prop): p ∧ q → r ∧ s → s ∧ q :=
@@ -17,3 +26,12 @@ begin
   trace_state,
   constructor; assumption
 end
+
+example (p q r s: Prop): p ∧ q → r ∧ s → s ∧ q :=
+begin
+  intros a a_1,
+  induction a,
+  induction a_1,
+  trace_state,
+  constructor; assumption
+end

tests/lean/cases_induction_fresh.lean.expected.out

@@ -4,6 +4,12 @@ a_1 : q,
 a_2 : r,
 a_3 : s
 ⊢ s ∧ q
+p q r s : Prop,
+a : p,
+a_2 : q,
+a_1 : r,
+a_3 : s
+⊢ s ∧ q
 ------------
 p q r s : Prop,
 a : p,
@@ -11,3 +17,9 @@ a_1 : q,
 a_2 : r,
 a_3 : s
 ⊢ s ∧ q
+p q r s : Prop,
+a : p,
+a_2 : q,
+a_1 : r,
+a_3 : s
+⊢ s ∧ q

tests/lean/run/aexp.lean

@@ -58,13 +58,13 @@ meta def not_done : tactic unit := fail_if_success done
 lemma aval_asimp_const (a : aexp) (s : state) : aval (asimp_const a) s = aval a s :=
 begin [smt]
  induction a,
- all_goals {destruct (asimp_const a_1), all_goals {destruct (asimp_const a_2), eblast}}
+ all_goals {destruct (asimp_const a_1), all_goals {destruct (asimp_const a), eblast}}
 end
 
 lemma ex2 (a : aexp) (s : state) : aval (asimp_const a) s = aval a s :=
 begin [smt]
  induction a,
- all_goals {destruct (asimp_const a_1), all_goals {destruct (asimp_const a_2), eblast_using [asimp_const, aval]}}
+ all_goals {destruct (asimp_const a_1), all_goals {destruct (asimp_const a), eblast_using [asimp_const, aval]}}
 end
 
 end imp

tests/lean/run/smt_tests3.lean

@@ -7,7 +7,7 @@ begin
   induction a,
   dsimp [f], intro x, contradiction,
   dsimp [f],
-  change nat.succ (f a_1) ≠ 0,
+  change nat.succ (f a) ≠ 0,
   apply nat.succ_ne_zero
 end