From a4a8253f50c36bab359589c3f2bf0c6f6c7fb9e4 Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Mon, 15 Jun 2015 21:10:03 +1000
Subject: [PATCH] refactor(library,hott,tests): rename succ_inj to succ.inj,
 add abbreviation eq_of_succ_eq_succ

---
 hott/types/nat/basic.hlean         | 6 +++---
 library/data/fintype/function.lean | 2 +-
 library/data/list/basic.lean       | 2 +-
 library/data/nat/basic.lean        | 8 +++++---
 library/data/vec.lean              | 4 ++--
 tests/lean/K_bug.lean              | 2 +-
 tests/lean/slow/nat_bug2.lean      | 8 ++++----
 tests/lean/slow/nat_wo_hints.lean  | 8 ++++----
 8 files changed, 21 insertions(+), 19 deletions(-)

diff --git a/hott/types/nat/basic.hlean b/hott/types/nat/basic.hlean
index 32dc4f010..ac14b7084 100644
--- a/hott/types/nat/basic.hlean
+++ b/hott/types/nat/basic.hlean
@@ -65,7 +65,7 @@ nat.rec_on n
 definition exists_eq_succ_of_ne_zero {n : ℕ} (H : n ≠ 0) : Σk : ℕ, n = succ k :=
 sigma.mk _ (sum_resolve_right !eq_zero_or_eq_succ_pred H)
 
-definition succ_inj {n m : ℕ} (H : succ n = succ m) : n = m :=
+definition succ.inj {n m : ℕ} (H : succ n = succ m) : n = m :=
 lift.down (nat.no_confusion H (λe, e))
 
 definition succ_ne_self {n : ℕ} : succ n ≠ n :=
@@ -73,7 +73,7 @@ nat.rec_on n
   (take H : 1 = 0,
     have ne : 1 ≠ 0, from !succ_ne_zero,
     absurd H ne)
-  (take k IH H, IH (succ_inj H))
+  (take k IH H, IH (succ.inj H))
 
 definition discriminate {B : Type} {n : ℕ} (H1: n = 0 → B) (H2 : ∀m, n = succ m → B) : B :=
 have H : n = n → B, from nat.cases_on n H1 H2,
@@ -161,7 +161,7 @@ nat.rec_on n
       succ (n + m) = succ n + m   : succ_add
                ... = succ n + k   : H
                ... = succ (n + k) : succ_add,
-    have H3 : n + m = n + k, from succ_inj H2,
+    have H3 : n + m = n + k, from succ.inj H2,
     IH H3)
 
 definition add.cancel_right {n m k : ℕ} (H : n + m = k + m) : n = k :=
diff --git a/library/data/fintype/function.lean b/library/data/fintype/function.lean
index 0c375f8ac..7b2ae4551 100644
--- a/library/data/fintype/function.lean
+++ b/library/data/fintype/function.lean
@@ -61,7 +61,7 @@ lemma mem_all_lists : ∀ {n : nat} {l : list A}, length l = n → l ∈ all_lis
 | (succ n) (a::l)   := assume Peq, begin
                     apply mem_map, apply mem_product,
                       exact fintype.complete a,
-                      exact mem_all_lists (succ_inj Peq)
+                      exact mem_all_lists (succ.inj Peq)
                     end
 
 lemma mem_all_nodups [deceqA : decidable_eq A] (n : nat) (l : list A) :
diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index 14032bfae..aa029aa40 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -441,7 +441,7 @@ lemma not_mem_of_find_eq_length : ∀ {a} {l : list T}, find a l = length l →
                   begin
                     rewrite [find_cons_of_ne l Pne, length_cons, mem_cons_iff],
                     intro Plen, apply (not_or Pne),
-                    exact not_mem_of_find_eq_length (succ_inj Plen)
+                    exact not_mem_of_find_eq_length (succ.inj Plen)
                   end)
 
 lemma find_lt_length {a} {l : list T} (Pin : a ∈ l) : find a l < length l :=
diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean
index 79959b6dd..8d63ae93f 100644
--- a/library/data/nat/basic.lean
+++ b/library/data/nat/basic.lean
@@ -64,15 +64,17 @@ nat.induction_on n
 theorem exists_eq_succ_of_ne_zero {n : ℕ} (H : n ≠ 0) : ∃k : ℕ, n = succ k :=
 exists.intro _ (or_resolve_right !eq_zero_or_eq_succ_pred H)
 
-theorem succ_inj {n m : ℕ} (H : succ n = succ m) : n = m :=
+theorem succ.inj {n m : ℕ} (H : succ n = succ m) : n = m :=
 nat.no_confusion H (λe, e)
 
+abbreviation eq_of_succ_eq_succ := @succ.inj
+
 theorem succ_ne_self {n : ℕ} : succ n ≠ n :=
 nat.induction_on n
   (take H : 1 = 0,
     have ne : 1 ≠ 0, from !succ_ne_zero,
     absurd H ne)
-  (take k IH H, IH (succ_inj H))
+  (take k IH H, IH (succ.inj H))
 
 theorem discriminate {B : Prop} {n : ℕ} (H1: n = 0 → B) (H2 : ∀m, n = succ m → B) : B :=
 have H : n = n → B, from nat.cases_on n H1 H2,
@@ -160,7 +162,7 @@ nat.induction_on n
       succ (n + m) = succ n + m   : succ_add
                ... = succ n + k   : H
                ... = succ (n + k) : succ_add,
-    have H3 : n + m = n + k, from succ_inj H2,
+    have H3 : n + m = n + k, from succ.inj H2,
     IH H3)
 
 theorem add.cancel_right {n m k : ℕ} (H : n + m = k + m) : n = k :=
diff --git a/library/data/vec.lean b/library/data/vec.lean
index 6328135b9..8b047eed3 100644
--- a/library/data/vec.lean
+++ b/library/data/vec.lean
@@ -38,7 +38,7 @@ namespace vec
 
   definition tail {n : nat} : vec A (succ n) → vec A n
   | (tag []     h) := by contradiction
-  | (tag (a::v) h) := tag v (succ_inj h)
+  | (tag (a::v) h) := tag v (succ.inj h)
 
   theorem head_cons {n : nat} (a : A) (v : vec A n) : head (a :: v) = a :=
   by induction v; reflexivity
@@ -49,7 +49,7 @@ namespace vec
   theorem head_lcons {n : nat} (a : A) (l : list A) (h : length (a::l) = succ n) : head (tag (a::l) h) = a :=
   rfl
 
-  theorem tail_lcons {n : nat} (a : A) (l : list A) (h : length (a::l) = succ n) : tail (tag (a::l) h) = tag l (succ_inj h) :=
+  theorem tail_lcons {n : nat} (a : A) (l : list A) (h : length (a::l) = succ n) : tail (tag (a::l) h) = tag l (succ.inj h) :=
   rfl
 
   theorem eta : ∀ {n : nat} (v : vec A (succ n)), head v :: tail v = v
diff --git a/tests/lean/K_bug.lean b/tests/lean/K_bug.lean
index 0e56a3bb7..b1299db12 100644
--- a/tests/lean/K_bug.lean
+++ b/tests/lean/K_bug.lean
@@ -9,7 +9,7 @@ namespace Nat
 definition pred (n : Nat) := Nat.rec zero (fun m x, m) n
 theorem pred_succ (n : Nat) : pred (succ n) = n := rfl
 
-theorem succ_inj {n m : Nat} (H : succ n = succ m) : n = m
+theorem succ.inj {n m : Nat} (H : succ n = succ m) : n = m
 := calc
     n = pred (succ n) : pred_succ n⁻¹
   ... = pred (succ m) : {H}
diff --git a/tests/lean/slow/nat_bug2.lean b/tests/lean/slow/nat_bug2.lean
index 2aa0534a5..9eaf20e44 100644
--- a/tests/lean/slow/nat_bug2.lean
+++ b/tests/lean/slow/nat_bug2.lean
@@ -70,7 +70,7 @@ theorem discriminate {B : Prop} {n : ℕ} (H1: n = 0 → B) (H2 : ∀m, n = succ
     (take H3 : n = 0, H1 H3)
     (take H3 : n = succ (pred n), H2 (pred n) H3)
 
-theorem succ_inj {n m : ℕ} (H : succ n = succ m) : n = m
+theorem succ.inj {n m : ℕ} (H : succ n = succ m) : n = m
 := calc
     n = pred (succ n) : (pred_succ n)⁻¹
   ... = pred (succ m) : {H}
@@ -81,7 +81,7 @@ theorem succ_ne_self (n : ℕ) : succ n ≠ n
     (take H : 1 = 0,
       have ne : 1 ≠ 0, from succ_ne_zero 0,
       absurd H ne)
-    (take k IH H, IH (succ_inj H))
+    (take k IH H, IH (succ.inj H))
 
 theorem decidable_eq [instance] (n m : ℕ) : decidable (n = m)
 := have general : ∀n, decidable (n = m), from
@@ -99,7 +99,7 @@ theorem decidable_eq [instance] (n m : ℕ) : decidable (n = m)
                (assume Heq : n' = m', inl (congr_arg succ Heq))
                (assume Hne : n' ≠ m',
                  have H1 : succ n' ≠ succ m', from
-                   assume Heq, absurd (succ_inj Heq) Hne,
+                   assume Heq, absurd (succ.inj Heq) Hne,
                  inr H1))),
   general n
 
@@ -209,7 +209,7 @@ theorem add_cancel_left {n m k : ℕ} : n + m = n + k → m = k
         succ (n + m) = succ n + m : symm (succ_add n m)
           ... = succ n + k : H
           ... = succ (n + k) : succ_add n k,
-      have H3 : n + m = n + k, from succ_inj H2,
+      have H3 : n + m = n + k, from succ.inj H2,
       IH H3)
 
 --rename to and_cancel_right
diff --git a/tests/lean/slow/nat_wo_hints.lean b/tests/lean/slow/nat_wo_hints.lean
index af66f4c9c..801ac3fec 100644
--- a/tests/lean/slow/nat_wo_hints.lean
+++ b/tests/lean/slow/nat_wo_hints.lean
@@ -64,7 +64,7 @@ theorem discriminate {B : Prop} {n : ℕ} (H1: n = 0 → B) (H2 : ∀m, n = succ
     (take H3 : n = 0, H1 H3)
     (take H3 : n = succ (pred n), H2 (pred n) H3)
 
-theorem succ_inj {n m : ℕ} (H : succ n = succ m) : n = m
+theorem succ.inj {n m : ℕ} (H : succ n = succ m) : n = m
 := calc
     n = pred (succ n) : (pred_succ n)⁻¹
   ... = pred (succ m) : {H}
@@ -75,7 +75,7 @@ theorem succ_ne_self (n : ℕ) : succ n ≠ n
     (take H : 1 = 0,
       have ne : 1 ≠ 0, from succ_ne_zero 0,
       absurd H ne)
-    (take k IH H, IH (succ_inj H))
+    (take k IH H, IH (succ.inj H))
 
 theorem decidable_eq [instance] (n m : ℕ) : decidable (n = m)
 := have general : ∀n, decidable (n = m), from
@@ -93,7 +93,7 @@ theorem decidable_eq [instance] (n m : ℕ) : decidable (n = m)
                (assume Heq : n' = m', inl (congr_arg succ Heq))
                (assume Hne : n' ≠ m',
                  have H1 : succ n' ≠ succ m', from
-                   assume Heq, absurd (succ_inj Heq) Hne,
+                   assume Heq, absurd (succ.inj Heq) Hne,
                  inr H1))),
   general n
 
@@ -203,7 +203,7 @@ theorem add_cancel_left {n m k : ℕ} : n + m = n + k → m = k
         succ (n + m) = succ n + m : symm (succ_add n m)
           ... = succ n + k : H
           ... = succ (n + k) : succ_add n k,
-      have H3 : n + m = n + k, from succ_inj H2,
+      have H3 : n + m = n + k, from succ.inj H2,
       IH H3)
 
 --rename to and_cancel_right