feat(set_theory/ordinal_notation): ordinal notations for ordinals < e0

This allows us to compute with small countable ordinals using trees of nats.

algebra/order.lean

@@ -34,11 +34,18 @@ lemma le_or_lt [linear_order α] : ∀ a b : α, a ≤ b ∨ a > b := le_or_gt
 lemma not_lt_iff_eq_or_lt [linear_order α] {a b : α} : ¬ a < b ↔ a = b ∨ b < a :=
 not_lt.trans $ le_iff_eq_or_lt.trans $ or_congr eq_comm iff.rfl
 
-lemma lt_iff_lt_of_strict_mono {β} [linear_order α] [linear_order β]
+lemma lt_iff_lt_of_strict_mono {β} [linear_order α] [preorder β]
   (f : α → β) (H : ∀ a b, a < b → f a < f b) {a b} :
   f a < f b ↔ a < b :=
-⟨by rw [← not_le, ← not_le, le_iff_lt_or_eq, le_iff_lt_or_eq];
-    exact mt (or.imp (H _ _) (congr_arg _)), H _ _⟩
+⟨λ h, ((lt_trichotomy b a)
+  .resolve_left $ λ h', lt_asymm h $ H _ _ h')
+  .resolve_left $ λ e, ne_of_gt h $ congr_arg _ e, H _ _⟩
+
+lemma injective_of_strict_mono {β} [linear_order α] [preorder β]
+  (f : α → β) (H : ∀ a b, a < b → f a < f b) : function.injective f
+| a b e := ((lt_trichotomy a b)
+  .resolve_left $ λ h, ne_of_lt (H _ _ h) e)
+  .resolve_right $ λ h, ne_of_gt (H _ _ h) e
 
 lemma le_imp_le_iff_lt_imp_lt {β} [linear_order α] [linear_order β] {a b : α} {c d : β} :
   (a ≤ b → c ≤ d) ↔ (d < c → b < a) :=
@@ -65,3 +72,42 @@ le_of_not_lt $ λ h, lt_irrefl _ (H _ h)
 lemma eq_of_forall_ge_iff [partial_order α] {a b : α}
   (H : ∀ c, a ≤ c ↔ b ≤ c) : a = b :=
 le_antisymm ((H _).2 (le_refl _)) ((H _).1 (le_refl _))
+
+namespace ordering
+
+@[simp] def compares [has_lt α] : ordering → α → α → Prop
+| lt a b := a < b
+| eq a b := a = b
+| gt a b := a > b
+
+theorem compares.eq_lt [preorder α] :
+  ∀ {o} {a b : α}, compares o a b → (o = lt ↔ a < b)
+| lt a b h := ⟨λ _, h, λ _, rfl⟩
+| eq a b h := ⟨λ h, by injection h, λ h', (ne_of_lt h' h).elim⟩
+| gt a b h := ⟨λ h, by injection h, λ h', (lt_asymm h h').elim⟩
+
+theorem compares.eq_eq [preorder α] :
+  ∀ {o} {a b : α}, compares o a b → (o = eq ↔ a = b)
+| lt a b h := ⟨λ h, by injection h, λ h', (ne_of_lt h h').elim⟩
+| eq a b h := ⟨λ _, h, λ _, rfl⟩
+| gt a b h := ⟨λ h, by injection h, λ h', (ne_of_gt h h').elim⟩
+
+theorem compares.eq_gt [preorder α] :
+  ∀ {o} {a b : α}, compares o a b → (o = gt ↔ a > b)
+| lt a b h := ⟨λ h, by injection h, λ h', (lt_asymm h h').elim⟩
+| eq a b h := ⟨λ h, by injection h, λ h', (ne_of_gt h' h).elim⟩
+| gt a b h := ⟨λ _, h, λ _, rfl⟩
+
+theorem compares.inj [preorder α] {o₁} :
+  ∀ {o₂} {a b : α}, compares o₁ a b → compares o₂ a b → o₁ = o₂
+| lt a b h₁ h₂ := h₁.eq_lt.2 h₂
+| eq a b h₁ h₂ := h₁.eq_eq.2 h₂
+| gt a b h₁ h₂ := h₁.eq_gt.2 h₂
+
+theorem compares_of_strict_mono {β} [linear_order α] [preorder β]
+  (f : α → β) (H : ∀ a b, a < b → f a < f b) {a b} : ∀ {o}, compares o (f a) (f b) ↔ compares o a b
+| lt := lt_iff_lt_of_strict_mono f H
+| eq := ⟨λ h, injective_of_strict_mono _ H h, congr_arg _⟩
+| gt := lt_iff_lt_of_strict_mono f H
+
+end ordering

data/nat/cast.lean

@@ -21,7 +21,7 @@ protected def cast : ℕ → α
 
 @[simp] theorem cast_zero : ((0 : ℕ) : α) = 0 := rfl
 
-@[simp] theorem cast_add_one (n : ℕ) : ((n + 1 : ℕ) : α) = n + 1 := rfl
+theorem cast_add_one (n : ℕ) : ((n + 1 : ℕ) : α) = n + 1 := rfl
 @[simp] theorem cast_succ (n : ℕ) : ((succ n : ℕ) : α) = n + 1 := rfl
 end
 

data/pnat.lean

@@ -13,32 +13,30 @@ meta def exact_dec_trivial : tactic unit := `[exact dec_trivial]
 
 namespace nat
 
-  def to_pnat (n : ℕ) (h : n > 0 . exact_dec_trivial) : ℕ+ := ⟨n, h⟩
+def to_pnat (n : ℕ) (h : n > 0 . exact_dec_trivial) : ℕ+ := ⟨n, h⟩
 
-  def succ_pnat (n : ℕ) : ℕ+ := ⟨succ n, succ_pos n⟩
+def succ_pnat (n : ℕ) : ℕ+ := ⟨succ n, succ_pos n⟩
+
+def to_pnat' (n : ℕ) : ℕ+ := succ_pnat (pred n)
 
-  def to_pnat' (n : ℕ) : ℕ+ := succ_pnat (pred n)
 end nat
 
 instance coe_nat_pnat : has_coe ℕ ℕ+ := ⟨nat.to_pnat'⟩
 
 namespace pnat
-  open nat
 
-  instance : has_one ℕ+ := ⟨succ_pnat 0⟩
+open nat
 
-  protected def add : ℕ+ → ℕ+ → ℕ+
-  | ⟨m, m0⟩ ⟨n, n0⟩ := ⟨m + n, add_pos m0 n0⟩
+instance : has_one ℕ+ := ⟨succ_pnat 0⟩
 
-  instance : has_add ℕ+ := ⟨pnat.add⟩
+instance : has_add ℕ+ := ⟨λ m n, ⟨m.1 + n.1, add_pos m.2 n.2⟩⟩
 
-  protected def mul : ℕ+ → ℕ+ → ℕ+
-  | ⟨m, m0⟩ ⟨n, n0⟩ := ⟨m * n, mul_pos m0 n0⟩
+instance : has_mul ℕ+ := ⟨λ m n, ⟨m.1 * n.1, mul_pos m.2 n.2⟩⟩
 
-  instance : has_mul ℕ+ := ⟨pnat.mul⟩
+@[simp] theorem ne_zero (n : ℕ+) : n.1 ≠ 0 := ne_of_gt n.2
 
-  @[simp] theorem to_pnat'_val {n : ℕ} : n > 0 → n.to_pnat'.val = n := succ_pred_eq_of_pos
-  @[simp] theorem nat_coe_val  {n : ℕ} : n > 0 → (n : ℕ+).val = n := succ_pred_eq_of_pos
-  @[simp] theorem to_pnat'_coe {n : ℕ} : n > 0 → (n.to_pnat' : ℕ) = n := succ_pred_eq_of_pos
+@[simp] theorem to_pnat'_val {n : ℕ} : n > 0 → n.to_pnat'.val = n := succ_pred_eq_of_pos
+@[simp] theorem nat_coe_val  {n : ℕ} : n > 0 → (n : ℕ+).val = n := succ_pred_eq_of_pos
+@[simp] theorem to_pnat'_coe {n : ℕ} : n > 0 → (n.to_pnat' : ℕ) = n := succ_pred_eq_of_pos
 
 end pnat

logic/basic.lean

@@ -207,6 +207,12 @@ if ha : a then or.inr (h ha) else or.inl ha
 theorem imp_iff_not_or [decidable a] : (a → b) ↔ (¬ a ∨ b) :=
 ⟨not_or_of_imp, or.neg_resolve_left⟩
 
+theorem imp_or_distrib [decidable a] : (a → b ∨ c) ↔ (a → b) ∨ (a → c) :=
+by simp [imp_iff_not_or, or.comm, or.left_comm]
+
+theorem imp_or_distrib' [decidable b] : (a → b ∨ c) ↔ (a → b) ∨ (a → c) :=
+by by_cases b; simp [h, or_iff_right_of_imp ((∘) false.elim)]
+
 theorem not_imp_of_and_not (h : a ∧ ¬ b) : ¬ (a → b) :=
 assume h₁, and.right h (h₁ (and.left h))
 

theories/number_theory/dioph.lean → number_theory/dioph.lean

@@ -3,7 +3,7 @@ Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import theories.number_theory.pell data.set data.pfun
+import number_theory.pell data.set data.pfun
 
 universe u
 

data/ordinal.lean → set_theory/ordinal.lean

@@ -7,7 +7,7 @@ Ordinal arithmetic.
 
 Ordinals are defined as equivalences of well-ordered sets by order isomorphism.
 -/
-import order.order_iso data.cardinal data.sum
+import order.order_iso set_theory.cardinal data.sum
 noncomputable theory
 
 open function cardinal
@@ -1725,6 +1725,12 @@ match o, o.out, o.out_eq, f :
   ⟨λ H i h, by simpa using H (enum r i h), λ H b, H _ _⟩
 end
 
+theorem bsup_type (r : α → α → Prop) [is_well_order α r] (f) :
+  bsup (type r) f = sup (λ a, f (typein r a) (typein_lt_type _ _)) :=
+eq_of_forall_ge_iff $ λ o,
+by rw [bsup_le, sup_le]; exact
+  ⟨λ H b, H _ _, λ H i h, by simpa using H (enum r i h)⟩
+
 theorem le_bsup {o} (f : Π a < o, ordinal) (i h) : f i h ≤ bsup o f :=
 bsup_le.1 (le_refl _) _ _
 
@@ -1999,6 +2005,9 @@ by simp [le_antisymm_iff]
 @[simp] theorem nat_cast_ne_zero {n : ℕ} : (n : ordinal) ≠ 0 ↔ n ≠ 0 :=
 not_congr nat_cast_eq_zero
 
+@[simp] theorem nat_cast_pos {n : ℕ} : (0 : ordinal) < n ↔ 0 < n :=
+by simpa using @nat_cast_lt 0 n
+
 @[simp] theorem nat_cast_sub {m n : ℕ} : ((m - n : ℕ) : ordinal) = m - n :=
 (_root_.le_total m n).elim
   (λ h, by rw [nat.sub_eq_zero_iff_le.2 h, sub_eq_zero_iff_le.2 (nat_cast_le.2 h)]; refl)
@@ -2156,6 +2165,36 @@ theorem add_absorp_iff {o : ordinal} (o0 : o > 0) : (∀ a < o, a + o = o) ↔ 
 end⟩,
 λ ⟨b, e⟩, e.symm ▸ λ a, add_omega_power⟩
 
+theorem add_mul_limit_aux {a b c : ordinal} (ba : b + a = a)
+  (l : is_limit c)
+  (IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b) :
+  (a + b) * c = a * c :=
+le_antisymm
+  ((mul_le_of_limit l).2 $ λ c' h, begin
+    apply le_trans (mul_le_mul_left _ (le_of_lt $ lt_succ_self _)),
+    rw IH _ h,
+    apply le_trans (add_le_add_left _ _),
+    { rw ← mul_succ, exact mul_le_mul_left _ (succ_le.2 $ l.2 _ h) },
+    { rw ← ba, exact le_add_right _ _ }
+  end)
+  (mul_le_mul_right _ (le_add_right _ _))
+
+theorem add_mul_succ {a b : ordinal} (c) (ba : b + a = a) :
+  (a + b) * succ c = a * succ c + b :=
+begin
+  apply limit_rec_on c,
+  { simp },
+  { intros c IH,
+    rw [mul_succ, IH, ← add_assoc, add_assoc _ b, ba, ← mul_succ] },
+  { intros c l IH,
+    have := add_mul_limit_aux ba l IH,
+    rw [mul_succ, add_mul_limit_aux ba l IH, mul_succ, add_assoc] }
+end
+
+theorem add_mul_limit {a b c : ordinal} (ba : b + a = a)
+  (l : is_limit c) : (a + b) * c = a * c :=
+add_mul_limit_aux ba l (λ c' _, add_mul_succ c' ba)
+
 theorem mul_omega {a : ordinal} (a0 : 0 < a) (ha : a < omega) : a * omega = omega :=
 le_antisymm
   ((mul_le_of_limit omega_is_limit).2 $ λ b hb, le_of_lt (mul_lt_omega ha hb))
@@ -2685,9 +2724,15 @@ theorem cof_sup_le {ι} (f : ι → ordinal) (H : ∀ i, f i < sup.{u u} f) :
   cof (sup.{u u} f) ≤ mk ι :=
 by simpa [cardinal.lift_id.{u u}] using cof_sup_le_lift.{u u} f H
 
-/-
-theorem cof_bsup_le_lift {o : ordinal} (f : Π a < o, ordinal) (H : ∀ i h, f i h < bsup o f) :
+theorem cof_bsup_le_lift {o : ordinal} : ∀ (f : Π a < o, ordinal), (∀ i h, f i h < bsup o f) →
   cof (bsup o f) ≤ o.card.lift :=
-_-/
+induction_on o $ λ α r _ f H,
+by rw bsup_type; refine cof_sup_le_lift _ _;
+   rw ← bsup_type; intro a; apply H
+
+theorem cof_bsup_le {o : ordinal} : ∀ (f : Π a < o, ordinal), (∀ i h, f i h < bsup.{u u} o f) →
+  cof (bsup.{u u} o f) ≤ o.card :=
+induction_on o $ λ α r _ f H,
+by simpa [cardinal.lift_id.{u u}] using cof_bsup_le_lift.{u u} f H
 
 end ordinal