feat(data/rat/denumerable): computable denumerability of Q (#1104)

* feat(data/rat/denumerable): computable denumerability of Q

* blah

* fix build

* remove unnecessary decidable_eq

* add header

* delete rat.lean and update imports

* fix build

* prove exists_not_mem_finset

* massively speed up encode

* minor change

src/algebra/archimedean.lean

@@ -6,7 +6,7 @@ Authors: Mario Carneiro
 Archimedean groups and fields.
 -/
 import algebra.group_power algebra.field_power
-import data.rat tactic.linarith tactic.abel
+import data.rat.basic tactic.linarith tactic.abel
 
 local infix ` • ` := add_monoid.smul
 

src/data/equiv/denumerable.lean

@@ -7,7 +7,7 @@ Denumerable (countably infinite) types, as a typeclass extending
 encodable. This is used to provide explicit encode/decode functions
 from nat, where the functions are known inverses of each other.
 -/
-import data.equiv.encodable data.sigma
+import data.equiv.encodable data.sigma data.fintype data.list.min_max
 open nat
 
 /-- A denumerable type is one which is (constructively) bijective with ℕ.
@@ -110,3 +110,130 @@ def pair : (α × α) ≃ α := equiv₂ _ _
 
 end
 end denumerable
+
+namespace nat.subtype
+open function encodable lattice
+
+variables {s : set ℕ} [decidable_pred s] [infinite s]
+
+lemma exists_succ (x : s) : ∃ n, x.1 + n + 1 ∈ s :=
+classical.by_contradiction $ λ h,
+have ∀ (a : ℕ) (ha : a ∈ s), a < x.val.succ,
+  from λ a ha, lt_of_not_ge (λ hax, h ⟨a - (x.1 + 1),
+    by rwa [add_right_comm, nat.add_sub_cancel' hax]⟩),
+infinite.not_fintype
+  ⟨(((multiset.range x.1.succ).filter (∈ s)).pmap
+      (λ (y : ℕ) (hy : y ∈ s), subtype.mk y hy)
+      (by simp [-multiset.range_succ])).to_finset,
+    by simpa [subtype.ext, multiset.mem_filter, -multiset.range_succ]⟩
+
+def succ (x : s) : s :=
+have h : ∃ m, x.1 + m + 1 ∈ s, from exists_succ x,
+⟨x.1 + nat.find h + 1, nat.find_spec h⟩
+
+lemma succ_le_of_lt {x y : s} (h : y < x) : succ y ≤ x :=
+have hx : ∃ m, y.1 + m + 1 ∈ s, from exists_succ _,
+let ⟨k, hk⟩ := nat.exists_eq_add_of_lt h in
+have nat.find hx ≤ k, from nat.find_min' _ (hk ▸ x.2),
+show y.1 + nat.find hx + 1 ≤ x.1,
+by rw hk; exact add_le_add_right (add_le_add_left this _) _
+
+lemma le_succ_of_forall_lt_le {x y : s} (h : ∀ z < x, z ≤ y) : x ≤ succ y :=
+have hx : ∃ m, y.1 + m + 1 ∈ s, from exists_succ _,
+show x.1 ≤ y.1 + nat.find hx + 1,
+from le_of_not_gt $ λ hxy,
+have y.1 + nat.find hx + 1 ≤ y.1 := h ⟨_, nat.find_spec hx⟩ hxy,
+not_lt_of_le this $
+  calc y.1 ≤ y.1 + nat.find hx : le_add_of_nonneg_right (nat.zero_le _)
+  ... < y.1 + nat.find hx + 1 : nat.lt_succ_self _
+
+lemma lt_succ_self (x : s) : x < succ x :=
+calc x.1 ≤ x.1 + _ : le_add_right (le_refl _)
+... < succ x : nat.lt_succ_self (x.1 + _)
+
+lemma lt_succ_iff_le {x y : s} : x < succ y ↔ x ≤ y :=
+⟨λ h, le_of_not_gt (λ h', not_le_of_gt h (succ_le_of_lt h')),
+  λ h, lt_of_le_of_lt h (lt_succ_self _)⟩
+
+def of_nat (s : set ℕ) [decidable_pred s] [infinite s] : ℕ → s
+| 0     := ⊥
+| (n+1) := succ (of_nat n)
+
+lemma of_nat_surjective_aux : ∀ {x : ℕ} (hx : x ∈ s), ∃ n, of_nat s n = ⟨x, hx⟩
+| x := λ hx, let t : list s := ((list.range x).filter (λ y, y ∈ s)).pmap
+  (λ (y : ℕ) (hy : y ∈ s), ⟨y, hy⟩) (by simp) in
+have hmt : ∀ {y : s}, y ∈ t ↔ y < ⟨x, hx⟩,
+  by simp [list.mem_filter, subtype.ext, t]; intros; refl,
+if ht : t = [] then ⟨0, le_antisymm (@bot_le s _ _)
+  (le_of_not_gt (λ h, list.not_mem_nil ⊥ $
+    by rw [← ht, hmt]; exact h))⟩
+else by letI : inhabited s := ⟨⊥⟩;
+  exact have wf : (list.maximum t).1 < x, by simpa [hmt] using list.mem_maximum ht,
+  let ⟨a, ha⟩ := of_nat_surjective_aux (list.maximum t).2 in
+  ⟨a + 1, le_antisymm
+    (by rw of_nat; exact succ_le_of_lt (by rw ha; exact wf)) $
+    by rw of_nat; exact le_succ_of_forall_lt_le
+      (λ z hz, by rw ha; exact list.le_maximum_of_mem (hmt.2 hz))⟩
+
+lemma of_nat_surjective : surjective (of_nat s) :=
+λ ⟨x, hx⟩, of_nat_surjective_aux hx
+
+private def to_fun_aux (x : s) : ℕ :=
+(list.range x).countp s
+
+private lemma to_fun_aux_eq (x : s) :
+  to_fun_aux x = ((finset.range x).filter s).card :=
+by rw [to_fun_aux, list.countp_eq_length_filter]; refl
+
+open finset
+
+private lemma right_inverse_aux : ∀ n, to_fun_aux (of_nat s n) = n
+| 0 := begin
+  rw [to_fun_aux_eq, card_eq_zero, eq_empty_iff_forall_not_mem],
+  assume n,
+  rw [mem_filter, of_nat, mem_range],
+  assume h,
+  exact not_lt_of_le bot_le (show (⟨n, h.2⟩ : s) < ⊥, from h.1)
+end
+| (n+1) := have ih : to_fun_aux (of_nat s n) = n, from right_inverse_aux n,
+have h₁ : (of_nat s n : ℕ) ∉ (range (of_nat s n)).filter s, by simp,
+have h₂ : (range (succ (of_nat s n))).filter s =
+    insert (of_nat s n) ((range (of_nat s n)).filter s),
+  begin
+    simp only [finset.ext, mem_insert, mem_range, mem_filter],
+    assume m,
+    exact ⟨λ h, by simp only [h.2, and_true]; exact or.symm
+        (lt_or_eq_of_le ((@lt_succ_iff_le _ _ _ ⟨m, h.2⟩ _).1 h.1)),
+      λ h, h.elim (λ h, h.symm ▸ ⟨lt_succ_self _, subtype.property _⟩)
+        (λ h, ⟨lt_of_le_of_lt (le_of_lt h.1) (lt_succ_self _), h.2⟩)⟩
+  end,
+begin
+  clear_aux_decl,
+  simp only [to_fun_aux_eq, of_nat, range_succ] at *,
+  conv {to_rhs, rw [← ih, ← card_insert_of_not_mem h₁, ← h₂] },
+end
+
+def denumerable (s : set ℕ) [decidable_pred s] [infinite s] : denumerable s :=
+denumerable.of_equiv ℕ
+{ to_fun := to_fun_aux,
+  inv_fun := of_nat s,
+  left_inv := left_inverse_of_surjective_of_right_inverse
+    of_nat_surjective right_inverse_aux,
+  right_inv := right_inverse_aux }
+
+end nat.subtype
+
+namespace denumerable
+open encodable
+
+def of_encodable_of_infinite (α : Type*) [encodable α] [infinite α] : denumerable α :=
+begin
+  letI := @decidable_range_encode α _;
+  letI : infinite (set.range (@encode α _)) :=
+    infinite.of_injective _ (equiv.set.range _ encode_injective).injective,
+  letI := nat.subtype.denumerable (set.range (@encode α _)),
+  exact denumerable.of_equiv (set.range (@encode α _))
+    (equiv_range_encode α)
+end
+
+end denumerable

src/data/equiv/encodable.lean

@@ -100,6 +100,24 @@ encode_injective $ (mem_decode2.1 h₁).trans (mem_decode2.1 h₂).symm
 theorem encodek2 [encodable α] (a : α) : decode2 α (encode a) = some a :=
 mem_decode2.2 rfl
 
+def decidable_range_encode (α : Type*) [encodable α] : decidable_pred (set.range (@encode α _)) :=
+λ x, decidable_of_iff (option.is_some (decode2 α x))
+  ⟨λ h, ⟨option.get h, by rw [← decode2_is_partial_inv (option.get h), option.some_get]⟩,
+  λ ⟨n, hn⟩, by rw [← hn, encodek2]; exact rfl⟩
+
+def equiv_range_encode (α : Type*) [encodable α] : α ≃ set.range (@encode α _) :=
+{ to_fun := λ a : α, ⟨encode a, set.mem_range_self _⟩,
+  inv_fun := λ n, option.get (show is_some (decode2 α n.1),
+    by cases n.2 with x hx; rw [← hx, encodek2]; exact rfl),
+  left_inv := λ a, by dsimp;
+    rw [← option.some_inj, option.some_get, encodek2],
+  right_inv := λ ⟨n, x, hx⟩, begin
+    apply subtype.eq,
+    dsimp,
+    conv {to_rhs, rw ← hx},
+    rw [encode_injective.eq_iff, ← option.some_inj, option.some_get, ← hx, encodek2],
+  end }
+
 section sum
 variables [encodable α] [encodable β]
 

src/data/fintype.lean

@@ -682,3 +682,29 @@ lemma bijective_bij_inv (f_bij : bijective f) : bijective (bij_inv f_bij) :=
 end bijection_inverse
 
 end fintype
+
+class infinite (α : Type*) : Prop :=
+(not_fintype : fintype α → false)
+
+namespace infinite
+
+lemma exists_not_mem_finset [infinite α] (s : finset α) : ∃ x, x ∉ s :=
+classical.not_forall.1 $ λ h, not_fintype ⟨s, h⟩
+
+instance nonempty (α : Type*) [infinite α] : nonempty α :=
+nonempty_of_exists (exists_not_mem_finset (∅ : finset α))
+
+lemma of_injective [infinite β] (f : β → α) (hf : injective f) : infinite α :=
+⟨λ I, by exactI not_fintype (fintype.of_injective f hf)⟩
+
+lemma of_surjective [infinite β] (f : α → β) (hf : surjective f) : infinite α :=
+⟨λ I, by classical; exactI not_fintype (fintype.of_surjective f hf)⟩
+
+end infinite
+
+instance nat.infinite : infinite ℕ :=
+⟨λ ⟨s, hs⟩, not_le_of_gt (nat.lt_succ_self (s.sum id)) $
+  @finset.single_le_sum _ _ _ id _ _ (λ _ _, nat.zero_le _) _ (hs _)⟩
+
+instance int.infinite : infinite ℤ :=
+infinite.of_injective int.of_nat (λ _ _, int.of_nat_inj)

src/data/fp/basic.lean

@@ -6,7 +6,7 @@ Authors: Mario Carneiro
 Implementation of floating-point numbers (experimental).
 -/
 
-import data.rat data.semiquot
+import data.rat.basic data.semiquot
 
 def int.shift2 (a b : ℕ) : ℤ → ℕ × ℕ
 | (int.of_nat e) := (a.shiftl e, b)
@@ -201,4 +201,4 @@ meta def div (mode : rmode) : float → float → float
 
 end float
 
-end fp
+end fp

src/data/option/basic.lean

@@ -14,6 +14,11 @@ variables {α : Type*} {β : Type*}
 theorem get_of_mem {a : α} : ∀ {o : option α} (h : is_some o), a ∈ o → option.get h = a
 | _ _ rfl := rfl
 
+@[simp] lemma some_get : ∀ {x : option α} (h : is_some x), some (option.get h) = x
+| (some x) hx := rfl
+
+@[simp] lemma get_some (x : α) (h : is_some (some x)) : option.get h = x := rfl
+
 theorem mem_unique {o : option α} {a b : α} (ha : a ∈ o) (hb : b ∈ o) : a = b :=
 option.some.inj $ ha.symm.trans hb
 

src/data/padics/padic_norm.lean

@@ -6,7 +6,7 @@ Authors: Robert Y. Lewis
 Define the p-adic valuation on ℤ and ℚ, and the p-adic norm on ℚ
 -/
 
-import data.rat algebra.gcd_domain algebra.field_power
+import data.rat.basic algebra.gcd_domain algebra.field_power
 import ring_theory.multiplicity tactic.ring
 import data.real.cau_seq
 import tactic.norm_cast

src/data/rat/denumerable.lean

@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2019 Chris Hughes. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Chris Hughes
+-/
+
+import data.rat.basic data.equiv.denumerable
+
+namespace rat
+open denumerable
+
+instance : infinite ℚ :=
+infinite.of_injective (coe : ℕ → ℚ) nat.cast_injective
+
+private def denumerable_aux : ℚ ≃ { x : ℤ × ℕ // 0 < x.2 ∧ x.1.nat_abs.coprime x.2 } :=
+{ to_fun := λ x, ⟨⟨x.1, x.2⟩, x.3, x.4⟩,
+  inv_fun := λ x, ⟨x.1.1, x.1.2, x.2.1, x.2.2⟩,
+  left_inv := λ ⟨_, _, _, _⟩, rfl,
+  right_inv := λ ⟨⟨_, _⟩, _, _⟩, rfl }
+
+instance : denumerable ℚ :=
+begin
+  let T := { x : ℤ × ℕ // 0 < x.2 ∧ x.1.nat_abs.coprime x.2 },
+  letI : infinite T := infinite.of_injective _ denumerable_aux.injective,
+  letI : encodable T := encodable.subtype,
+  letI : denumerable T := of_encodable_of_infinite T,
+  exact denumerable.of_equiv T denumerable_aux
+end
+
+end rat

src/measure_theory/outer_measure.lean

@@ -55,7 +55,7 @@ begin
   { intros n h,
     transitivity, swap,
     rw [show decode2 β n = _, from option.get_mem (H n h)],
-    congr, simp [ext_iff] }
+    congr, simp [ext_iff, -option.some_get] }
 end
 
 protected theorem Union (m : outer_measure α)

src/order/bounded_lattice.lean

@@ -168,6 +168,17 @@ end semilattice_sup_bot
 instance nat.semilattice_sup_bot : semilattice_sup_bot ℕ :=
 { bot := 0, bot_le := nat.zero_le, .. nat.distrib_lattice }
 
+private def bot_aux (s : set ℕ) [decidable_pred s] [h : nonempty s] : s :=
+have ∃ x, x ∈ s, from nonempty.elim h (λ x, ⟨x.1, x.2⟩),
+⟨nat.find this, nat.find_spec this⟩
+
+instance nat.subtype.semilattice_sup_bot (s : set ℕ) [decidable_pred s] [h : nonempty s] :
+  semilattice_sup_bot s :=
+{ bot := bot_aux s,
+  bot_le := λ x, nat.find_min' _ x.2,
+  ..subtype.linear_order s,
+  ..lattice.lattice_of_decidable_linear_order }
+
 /-- A `semilattice_inf_top` is a semilattice with top and meet. -/
 class semilattice_inf_top (α : Type u) extends order_top α, semilattice_inf α
 
@@ -726,4 +737,3 @@ instance [bounded_distrib_lattice α] [bounded_distrib_lattice β] :
 { .. prod.lattice.bounded_lattice α β, .. prod.lattice.distrib_lattice α β }
 
 end prod
-

src/tactic/norm_num.lean

@@ -6,7 +6,7 @@ Authors: Simon Hudon, Mario Carneiro
 Evaluating arithmetic expressions including *, +, -, ^, ≤
 -/
 
-import algebra.group_power data.rat data.nat.prime
+import algebra.group_power data.rat.basic data.nat.prime
 import tactic.interactive tactic.converter.interactive
 
 universes u v w