From dce257bccb2e2ef41727bd8a49c22b3d645b69c8 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Thu, 4 Jun 2015 20:23:44 -0400
Subject: [PATCH] fix(init/nat): remove exit

---
 library/init/nat.lean | 258 ------------------------------------------
 1 file changed, 258 deletions(-)

diff --git a/library/init/nat.lean b/library/init/nat.lean
index 89357b937..a3ff98e02 100644
--- a/library/init/nat.lean
+++ b/library/init/nat.lean
@@ -286,262 +286,4 @@ namespace nat
     (le.refl a)
     (λ b₁ ih, le.trans !pred_le ih)
 
-end nat
- exit
-
-
-  definition measure {A : Type} (f : A → nat) : A → A → Prop :=
-  inv_image lt f
-
-  definition measure.wf {A : Type} (f : A → nat) : well_founded (measure f) :=
-  inv_image.wf f lt.wf
-
-  theorem not_lt_zero (a : nat) : ¬ a < zero :=
-  have aux : ∀ {b}, a < b → b = zero → false, from
-    λ b H, lt.cases_on H
-      (by contradiction)
-      (by contradiction),
-  λ H, aux H rfl
-
-  theorem zero_lt_succ (a : nat) : zero < succ a :=
-  nat.rec_on a
-    (lt.base zero)
-    (λ a (hlt : zero < succ a), lt.step hlt)
-
-  theorem lt.trans [trans] {a b c : nat} (H₁ : a < b) (H₂ : b < c) : a < c :=
-  have aux : a < b → a < c, from
-    lt.rec_on H₂
-      (λ h₁, lt.step h₁)
-      (λ b₁ bb₁ ih h₁, lt.step (ih h₁)),
-  aux H₁
-
-  theorem succ_lt_succ {a b : nat} (H : a < b) : succ a < succ b :=
-  lt.rec_on H
-    (lt.base (succ a))
-    (λ b hlt ih, lt.trans ih (lt.base (succ b)))
-
-  theorem lt_of_succ_lt {a b : nat} (H : succ a < b) : a < b :=
-  lt.rec_on H
-    (lt.step (lt.base a))
-    (λ b h ih, lt.step ih)
-
-  theorem lt_of_succ_lt_succ {a b : nat} (H : succ a < succ b) : a < b :=
-  have aux : pred (succ a) < pred (succ b), from
-    lt.rec_on H
-      (lt.base a)
-      (λ (b : nat) (hlt : succ a < b) ih,
-        show pred (succ a) < pred (succ b), from
-        lt_of_succ_lt hlt),
-  aux
-
-  definition decidable_lt [instance] : decidable_rel lt :=
-  λ a b, nat.rec_on b
-    (λ (a : nat), inr (not_lt_zero a))
-    (λ (b₁ : nat) (ih : ∀ a, decidable (a < b₁)) (a : nat), nat.cases_on a
-       (inl !zero_lt_succ)
-       (λ a, decidable.rec_on (ih a)
-         (λ h_pos : a < b₁, inl (succ_lt_succ h_pos))
-         (λ h_neg : ¬ a < b₁,
-           have aux : ¬ succ a < succ b₁, from
-             λ h : succ a < succ b₁, h_neg (lt_of_succ_lt_succ h),
-           inr aux)))
-    a
-
-  theorem le.refl [refl] (a : nat) : a ≤ a :=
-  lt.base a
-
-  theorem le_of_lt {a b : nat} (H : a < b) : a ≤ b :=
-  lt.step H
-
-  theorem eq_or_lt_of_le {a b : nat} (H : a ≤ b) : a = b ∨ a < b :=
-  begin
-    cases H with b hlt,
-      apply or.inl rfl,
-      apply or.inr hlt
-  end
-
-  theorem le_of_eq_or_lt {a b : nat} (H : a = b ∨ a < b) : a ≤ b :=
-  or.rec_on H
-    (λ hl, eq.rec_on hl !le.refl)
-    (λ hr, le_of_lt hr)
-
-  definition decidable_le [instance] : decidable_rel le :=
-  λ a b, decidable_of_decidable_of_iff _ (iff.intro le_of_eq_or_lt eq_or_lt_of_le)
-
-  theorem le.rec_on {a : nat} {P : nat → Prop} {b : nat} (H : a ≤ b) (H₁ : P a) (H₂ : ∀ b, a < b → P b) : P b :=
-  begin
-    cases H with b hlt,
-      apply H₁,
-      apply H₂ b hlt
-  end
-
-  theorem lt.irrefl (a : nat) : ¬ a < a :=
-  nat.rec_on a
-    !not_lt_zero
-    (λ (a : nat) (ih : ¬ a < a) (h : succ a < succ a),
-      ih (lt_of_succ_lt_succ h))
-
-  theorem lt.asymm {a b : nat} (H : a < b) : ¬ b < a :=
-  lt.rec_on H
-    (λ h : succ a < a, !lt.irrefl (lt_of_succ_lt h))
-    (λ b hlt (ih : ¬ b < a) (h : succ b < a), ih (lt_of_succ_lt h))
-
-  theorem lt.trichotomy (a b : nat) : a < b ∨ a = b ∨ b < a :=
-  nat.rec_on b
-    (λa, nat.cases_on a
-       (or.inr (or.inl rfl))
-       (λ a₁, or.inr (or.inr !zero_lt_succ)))
-    (λ b₁ (ih : ∀a, a < b₁ ∨ a = b₁ ∨ b₁ < a) (a : nat), nat.cases_on a
-       (or.inl !zero_lt_succ)
-       (λ a, or.rec_on (ih a)
-           (λ h : a < b₁, or.inl (succ_lt_succ h))
-           (λ h, or.rec_on h
-              (λ h : a = b₁, or.inr (or.inl (eq.rec_on h rfl)))
-              (λ h : b₁ < a, or.inr (or.inr (succ_lt_succ h))))))
-    a
-
-  theorem eq_or_lt_of_not_lt {a b : nat} (hnlt : ¬ a < b) : a = b ∨ b < a :=
-  or.rec_on (lt.trichotomy a b)
-    (λ hlt, absurd hlt hnlt)
-    (λ h, h)
-
-  theorem lt_succ_of_le {a b : nat} (h : a ≤ b) : a < succ b :=
-  h
-
-  theorem lt_of_succ_le {a b : nat} (h : succ a ≤ b) : a < b :=
-  lt_of_succ_lt_succ h
-
-  theorem le_succ_of_le {a b : nat} (h : a ≤ b) : a ≤ succ b :=
-  lt.step h
-
-  theorem succ_le_of_lt {a b : nat} (h : a < b) : succ a ≤ b :=
-  succ_lt_succ h
-
-  theorem le.trans [trans] {a b c : nat} (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c :=
-  begin
-    cases h₁ with b' hlt,
-      apply h₂,
-      apply lt.trans hlt h₂
-  end
-
-  theorem lt_of_le_of_lt [trans] {a b c : nat} (h₁ : a ≤ b) (h₂ : b < c) : a < c :=
-  begin
-    cases h₁ with b' hlt,
-      apply h₂,
-      apply lt.trans hlt h₂
-  end
-
-  theorem lt_of_lt_of_le [trans] {a b c : nat} (h₁ : a < b) (h₂ : b ≤ c) : a < c :=
-  begin
-    cases h₁ with b' hlt,
-      apply lt_of_succ_lt_succ h₂,
-      apply lt.trans hlt (lt_of_succ_lt_succ h₂)
-  end
-
-  definition max (a b : nat) : nat :=
-  if a < b then b else a
-
-  definition min (a b : nat) : nat :=
-  if a < b then a else b
-
-  theorem max_self (a : nat) : max a a = a :=
-  eq.rec_on !if_t_t rfl
-
-  theorem max_eq_right {a b : nat} (H : a < b) : max a b = b :=
-  if_pos H
-
-  theorem max_eq_left {a b : nat} (H : ¬ a < b) : max a b = a :=
-  if_neg H
-
-  theorem eq_max_right {a b : nat} (H : a < b) : b = max a b :=
-  eq.rec_on (max_eq_right H) rfl
-
-  theorem eq_max_left {a b : nat} (H : ¬ a < b) : a = max a b :=
-  eq.rec_on (max_eq_left H) rfl
-
-  theorem le_max_left (a b : nat) : a ≤ max a b :=
-  by_cases
-    (λ h : a < b,   le_of_lt (eq.rec_on (eq_max_right h) h))
-    (λ h : ¬ a < b, eq.rec_on (eq_max_left h) !le.refl)
-
-  theorem le_max_right (a b : nat) : b ≤ max a b :=
-  by_cases
-    (λ h : a < b,   eq.rec_on (eq_max_right h) !le.refl)
-    (λ h : ¬ a < b, or.rec_on (eq_or_lt_of_not_lt h)
-      (λ heq, eq.rec_on heq (eq.rec_on (eq.symm (max_self a)) !le.refl))
-      (λ h : b < a,
-        have aux : a = max a b, from eq_max_left (lt.asymm h),
-        eq.rec_on aux (le_of_lt h)))
-
-  definition gt [reducible] a b := lt b a
-  definition decidable_gt [instance] : decidable_rel gt :=
-  _
-
-  notation a > b := gt a b
-
-  definition ge [reducible] a b := le b a
-  definition decidable_ge [instance] : decidable_rel ge :=
-  _
-
-  notation a >= b := ge a b
-  notation a ≥ b := ge a b
-
-  -- add is defined in init.num
-
-  definition sub (a b : nat) : nat :=
-  nat.rec_on b a (λ b₁ r, pred r)
-
-  notation a - b := sub a b
-
-  definition mul (a b : nat) : nat :=
-  nat.rec_on b zero (λ b₁ r, r + a)
-
-  notation a * b := mul a b
-
-  section
-  local attribute sub [reducible]
-  theorem succ_sub_succ_eq_sub (a b : nat) : succ a - succ b = a - b :=
-  nat.rec_on b
-    rfl
-    (λ b₁ (ih : succ a - succ b₁ = a - b₁),
-      eq.rec_on ih (eq.refl (pred (succ a - succ b₁))))
-  end
-
-  theorem sub_eq_succ_sub_succ (a b : nat) : a - b = succ a - succ b :=
-  eq.rec_on (succ_sub_succ_eq_sub a b) rfl
-
-  theorem zero_sub_eq_zero (a : nat) : zero - a = zero :=
-  nat.rec_on a
-    rfl
-    (λ a₁ (ih : zero - a₁ = zero),
-      eq.rec_on ih (eq.refl (pred (zero - a₁))))
-
-  theorem zero_eq_zero_sub (a : nat) : zero = zero - a :=
-  eq.rec_on (zero_sub_eq_zero a) rfl
-
-  theorem sub_lt {a b : nat} : zero < a → zero < b → a - b < a :=
-  have aux : Π {a}, zero < a → Π {b}, zero < b → a - b < a, from
-    λa h₁, lt.rec_on h₁
-      (λb h₂, lt.cases_on h₂
-        (lt.base zero)
-        (λ b₁ bpos,
-          eq.rec_on (sub_eq_succ_sub_succ zero b₁)
-           (eq.rec_on (zero_eq_zero_sub b₁) (lt.base zero))))
-      (λa₁ apos ih b h₂, lt.cases_on h₂
-        (lt.base a₁)
-        (λ b₁ bpos,
-          eq.rec_on (sub_eq_succ_sub_succ a₁ b₁)
-            (lt.trans (@ih b₁ bpos) (lt.base a₁)))),
-  λ h₁ h₂, aux h₁ h₂
-
-  theorem pred_le (a : nat) : pred a ≤ a :=
-  nat.cases_on a
-    (le.refl zero)
-    (λ a₁, le_of_lt (lt.base a₁))
-
-  theorem sub_le (a b : nat) : a - b ≤ a :=
-  nat.induction_on b
-    (le.refl a)
-    (λ b₁ ih, le.trans !pred_le ih)
-
 end nat