refactor(init/meta/tactic): use dite instead of cases in by_cases

This fixes the issue in PR #1752 by using `dite`, which is essentially nondependent cases, so that the decidable instances are not substituted.

library/init/data/array/lemmas.lean

@@ -129,12 +129,10 @@ def read_foreach_aux (f : fin n → α → α) (ai : array α n) :
 | (i+1) hi a ⟨j, hj⟩ ji := begin
   dsimp [iterate_aux], dsimp at ji,
   change ite _ _ _ = _,
-  by_cases (⟨i, hi⟩ : fin _) = ⟨j, hj⟩ with e,
-  { simp [e, if_pos] },
-  { simp [if_neg e],
-    rw [read_foreach_aux _ _ _ ⟨j, hj⟩],
-    exact (lt_or_eq_of_le (nat.le_of_lt_succ ji)).resolve_right
-      (ne.symm $ mt (@fin.eq_of_veq _ ⟨i, hi⟩ ⟨j, hj⟩) e) }
+  by_cases (⟨i, hi⟩ : fin _) = ⟨j, hj⟩ with e; simp [e],
+  rw [read_foreach_aux _ _ _ ⟨j, hj⟩],
+  exact (lt_or_eq_of_le (nat.le_of_lt_succ ji)).resolve_right
+    (ne.symm $ mt (@fin.eq_of_veq _ ⟨i, hi⟩ ⟨j, hj⟩) e)
 end
 
 def read_foreach (a : array α n) (f : fin n → α → α) (i : fin n) :

library/init/data/nat/bitwise.lean

@@ -5,7 +5,7 @@ Author: Mario Carneiro
 -/
 
 prelude
-import .lemmas init.meta.well_founded_tactics
+import init.data.nat.lemmas init.meta.well_founded_tactics
 
 universe u
 
@@ -203,19 +203,17 @@ 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 [dif_pos 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 },
-    {simp [dif_neg h'],
-     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 [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 }
   end
 
   lemma bitwise_bit_aux {f : bool → bool → bool} (h : f ff ff = ff) :

library/init/meta/tactic.lean

@@ -1004,8 +1004,10 @@ do tgt : expr ← target,
 meta def by_cases (e : expr) (h : name) : tactic unit :=
 do dec_e ← (mk_app `decidable [e] <|> fail "by_cases tactic failed, type is not a proposition"),
    inst  ← (mk_instance dec_e <|> fail "by_cases tactic failed, type of given expression is not decidable"),
-   em    ← mk_app `decidable.em [e, inst],
-   cases em [h, h]
+   t     ← target,
+   tm    ← (mk_mapp `dite [some e, some inst, some t] <|>
+     fail "by_cases tactic failed, type of given expression is not decidable"),
+   seq (apply tm) (intro h >> skip)
 
 private meta def get_undeclared_const (env : environment) (base : name) : ℕ → name | i :=
 let n := base <.> ("_aux_" ++ repr i) in