fix(library/init/meta/injection_tactic): fixes #1805

doc/changes.md

@@ -128,6 +128,9 @@ For more details, see discussion [here](https://github.com/leanprover/lean/pull/
   `strict_order`, `order_pair`, and `strong_order_pair`.  The `linear_order`
   class corresponds to `linear_order_pair`, and `linear_strong_order_pair`.
 
+* `injection` and `injections` tactics generate fresh names when user does not provide names.
+  The fresh names are of the form `h_<idx>`. See discussion [here](https://github.com/leanprover/lean/issues/1805).
+
 *API name changes*
 
 * `list.dropn` => `list.drop`

library/init/data/string/lemmas.lean

@@ -14,8 +14,8 @@ lemma str_ne_empty (c : char) (s : string) : str s c ≠ empty :=
 begin cases s, unfold str empty, intro h, injection h, contradiction end
 
 lemma str_ne_str_left {c₁ c₂ : char} (s₁ s₂ : string) : c₁ ≠ c₂ → str s₁ c₁ ≠ str s₂ c₂ :=
-begin cases s₁, cases s₂, intros h₁ h₂, unfold str at h₂, injection h₂, injection h, contradiction end
+begin cases s₁, cases s₂, intros h₁ h₂, unfold str at h₂, injection h₂ with h, injection h, contradiction end
 
 lemma str_ne_str_right (c₁ c₂ : char) {s₁ s₂ : string} : s₁ ≠ s₂ → str s₁ c₁ ≠ str s₂ c₂ :=
-begin cases s₁, cases s₂, intros h₁ h₂, unfold str at h₂, injection h₂, injection h, subst data, contradiction end
+begin cases s₁, cases s₂, intros h₁ h₂, unfold str at h₂, injection h₂ with h, injection h, subst data, contradiction end
 end string

library/init/meta/injection_tactic.lean

@@ -14,18 +14,25 @@ private meta def at_end₂ (e₁ e₂ : expr) : ℕ → tactic (list (option exp
 | (n+3) :=  (λ xs, none :: xs) <$> at_end₂ (n+2)
 | _ := fail "at_end expected arity > 1"
 
--- Auxiliary function for introducing the new equalities produced by the
--- injection tactic
-private meta def injection_intro : expr → list name → tactic (list expr × list name)
-| (pi n bi b d) ns := do
-  let hname := @head _ ⟨`h⟩ ns,
+private meta def mk_next_name : name → nat → tactic (name × nat)
+| n i := do
+  let n' := n.append_after i,
+  (get_local n' >> mk_next_name n (i+1))
+  <|>
+  (return (n', i+1))
+
+/- Auxiliary function for introducing the new equalities produced by the
+   injection tactic. -/
+private meta def injection_intro : expr → nat → list name → tactic (list expr × list name)
+| (pi n bi b d) i ns := do
+  (hname, i) ← if ns.empty then mk_next_name `h i else return (head ns, i),
   h ← intro hname,
-  (l, ns') ← injection_intro d (tail ns),
+  (l, ns') ← injection_intro d i (tail ns),
   return (h :: l, ns')
-| e  ns           := return ([], ns)
+| e  i ns            := return ([], ns)
 
--- Tries to decompose the given expression by constructor injectivity.
--- Returns the list of new hypotheses, and the remaining names from the given list.
+/- Tries to decompose the given expression by constructor injectivity.
+   Returns the list of new hypotheses, and the remaining names from the given list. -/
 meta def injection_with (h : expr) (ns : list name) : tactic (list expr × list name) :=
 do
   ht ← infer_type h,
@@ -46,7 +53,7 @@ do
       pr_type ← infer_type pr,
       pr_type ← whnf pr_type,
       eapply pr,
-      injection_intro (binding_domain pr_type) ns
+      injection_intro (binding_domain pr_type) 1 ns
     else fail "injection tactic failed, argument must be an equality proof where lhs and rhs are of the form (c ...), where c is a constructor"
   else do
     tgt ← target,

tests/lean/run/1805.lean

@@ -0,0 +1,20 @@
+example (x y z x' y' z': ℕ)  (h : (x, y, z) = (x', y', z')) : false :=
+begin
+  injection h,
+  guard_hyp h_1 := x = x',
+  guard_hyp h_2 := (y, z) = (y', z'),
+  injection h_2,
+  guard_hyp h_3 := y = y',
+  guard_hyp h_4 := z = z',
+  admit
+end
+
+example (x y z x' y' z': ℕ)  (h : (x, y, z) = (x', y', z')) : false :=
+begin
+  injections,
+  guard_hyp h_1 := x = x',
+  guard_hyp h_2 := (y, z) = (y', z'),
+  guard_hyp h_3 := y = y',
+  guard_hyp h_4 := z = z',
+  admit
+end