refactor(library): test new tactics in the standard library

library/data/encodable.lean

@@ -21,7 +21,7 @@ assume e : encodable A,
 have inj_encode : injective encode, from
   λ (a₁ a₂ : A) (h : encode a₁ = encode a₂),
     assert aux : decode A (encode a₁) = decode A (encode a₂), by rewrite h,
-    by rewrite [*encodek at aux]; exact (option.no_confusion aux (λ e, e)),
+    by rewrite [*encodek at aux]; injection aux; assumption,
 exists.intro encode inj_encode
 
 definition encodable_fintype [instance] {A : Type} [h₁ : fintype A] [h₂ : decidable_eq A] : encodable A :=

library/data/fintype.lean

@@ -70,8 +70,7 @@ theorem all_eq_of_find_discr_eq_none {f g : A → B} : ∀ {l}, find_discr f g l
       (λ aeqx : a = x, by rewrite [-aeqx at fx_eq_gx]; exact fx_eq_gx)
       (λ ainl : a ∈ l, all_eq_of_find_discr_eq_none aux a ainl))
   (λ fx_ne_gx : f x ≠ g x,
-    have aux : some x = none, by rewrite [find_discr_cons_of_ne l fx_ne_gx at e]; exact e,
-    option.no_confusion aux)
+    by rewrite [find_discr_cons_of_ne l fx_ne_gx at e]; contradiction)
 end find_discr
 
 definition decidable_eq_fun [instance] {A B : Type} [h₁ : fintype A] [h₂ : decidable_eq B] : decidable_eq (A → B) :=

library/data/int/basic.lean

@@ -94,10 +94,10 @@ infix *  := int.mul
 /- some basic functions and properties -/
 
 theorem of_nat.inj {m n : ℕ} (H : of_nat m = of_nat n) : m = n :=
-int.no_confusion H (λe, e)
+by injection H; assumption
 
 theorem neg_succ_of_nat.inj {m n : ℕ} (H : neg_succ_of_nat m = neg_succ_of_nat n) : m = n :=
-int.no_confusion H (λe, e)
+by injection H; assumption
 
 theorem neg_succ_of_nat_eq (n : ℕ) : -[n +1] = -(n + 1) := rfl
 

library/data/list/basic.lean

@@ -65,7 +65,7 @@ theorem length_append : ∀ (s t : list T), length (s ++ t) = length s + length
 
 theorem eq_nil_of_length_eq_zero : ∀ {l : list T}, length l = 0 → l = []
 | []     H := rfl
-| (a::s) H := nat.no_confusion H
+| (a::s) H := by contradiction
 
 -- add_rewrite length_nil length_cons
 

library/data/option.lean

@@ -23,7 +23,7 @@ namespace option
   by contradiction
 
   theorem some.inj {A : Type} {a₁ a₂ : A} (H : some a₁ = some a₂) : a₁ = a₂ :=
-  option.no_confusion H (λe, e)
+  by injection H; assumption
 
   protected definition is_inhabited [instance] (A : Type) : inhabited (option A) :=
   inhabited.mk none

library/data/sum.lean

@@ -28,10 +28,10 @@ namespace sum
   by contradiction
 
   definition inl_inj {a₁ a₂ : A} : intro_left B a₁ = intro_left B a₂ → a₁ = a₂ :=
-  assume H, sum.no_confusion H (λe, e)
+  assume H, by injection H; assumption
 
   definition inr_inj {b₁ b₂ : B} : intro_right A b₁ = intro_right A b₂ → b₁ = b₂ :=
-  assume H, sum.no_confusion H (λe, e)
+  assume H, by injection H; assumption
 
   protected definition is_inhabited_left [instance] [h : inhabited A] : inhabited (A + B) :=
   inhabited.mk (inl (default A))

library/init/nat.lean

@@ -34,9 +34,10 @@ namespace nat
   | has_decidable_eq (succ x) zero     := inr (by contradiction)
   | has_decidable_eq zero     (succ y) := inr (by contradiction)
   | has_decidable_eq (succ x) (succ y) :=
-      if H : x = y
-      then inl (eq.rec_on H rfl)
-      else inr (λ h : succ x = succ y, nat.no_confusion h (λ heq : x = y, absurd heq H))
+      match has_decidable_eq x y with
+      | inl xeqy := inl (by rewrite xeqy)
+      | inr xney := inr (λ h : succ x = succ y, by injection h with xeqy; exact absurd xeqy xney)
+      end
 
   -- less-than is well-founded
   definition lt.wf [instance] : well_founded lt :=
@@ -51,12 +52,10 @@ namespace nat
       acc.intro (succ n) (λ (m : nat) (hlt : m < succ n),
         have aux : ∀ {n₁} (hlt : m < n₁), succ n = n₁ → acc lt m, from
           λ n₁ hlt, nat.lt.cases_on hlt
-            (λ (heq : succ n = succ m),
-              nat.no_confusion heq (λ (e : n = m),
-                eq.rec_on e ih))
-            (λ b (hlt : m < b) (heq : succ n = succ b),
-              nat.no_confusion heq (λ (e : n = b),
-                acc.inv (eq.rec_on e ih) hlt)),
+            (λ (sn_eq_sm : succ n = succ m),
+               by injection sn_eq_sm with neqm; rewrite neqm at ih; exact ih)
+            (λ b (hlt : m < b) (sn_eq_sb : succ n = succ b),
+               by injection sn_eq_sb with neqb; rewrite neqb at ih; exact acc.inv ih hlt),
         aux hlt rfl)))
 
   definition measure {A : Type} (f : A → nat) : A → A → Prop :=