feat(*): replace fact(0 < t) with ne_zero (#16145)

This has almost fully made things easier, whilst also being easier on the typeclass system (`fact` can cause many slowdowns). It also allows us to make many things that were not instances before into instances.



Co-authored-by: Eric Rodriguez <[email protected]>

counterexamples/homogeneous_prime_not_prime.lean

@@ -118,14 +118,18 @@ instance : graded_algebra (grading R) :=
 /-- The counterexample is the ideal `I = span {(2, 2)}`. -/
 def I : ideal (R × R) := ideal.span {((2, 2) : (R × R))}.
 
+set_option class.instance_max_depth 33
+
 lemma I_not_prime : ¬ I.is_prime :=
 begin
   rintro ⟨rid1, rid2⟩,
   apply rid1, clear rid1, revert rid2,
   simp only [I, ideal.mem_span_singleton, ideal.eq_top_iff_one],
-  dec_trivial,
+  dec_trivial, -- this is what we change the max instance depth for, it's only 1 above the default
 end
 
+set_option class.instance_max_depth 32
+
 lemma I_is_homogeneous : I.is_homogeneous (grading R) :=
 begin
   rw ideal.is_homogeneous.iff_exists,

src/algebra/algebra/basic.lean

@@ -4,9 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Yury Kudryashov
 -/
 import algebra.module.basic
+import algebra.module.ulift
+import algebra.ne_zero
 import algebra.ring.aut
 import algebra.ring.ulift
-import algebra.module.ulift
 import linear_algebra.span
 import tactic.abel
 
@@ -1450,6 +1451,10 @@ suffices function.injective (λ (c : R), c • (1 : A)),
 by { convert this, ext, rw [algebra.smul_def, mul_one] },
 smul_left_injective R one_ne_zero
 
+lemma _root_.ne_zero.of_no_zero_smul_divisors (n : ℕ) [comm_ring R] [ne_zero (n : R)] [ring A]
+  [nontrivial A] [algebra R A] [no_zero_smul_divisors R A] : ne_zero (n : A) :=
+ne_zero.nat_of_injective $ no_zero_smul_divisors.algebra_map_injective R A
+
 variables {R A}
 lemma iff_algebra_map_injective [comm_ring R] [ring A] [is_domain A] [algebra R A] :
   no_zero_smul_divisors R A ↔ function.injective (algebra_map R A) :=

src/algebra/char_p/basic.lean

@@ -427,8 +427,8 @@ match p, hc with
 | (m+2), hc := or.inl (@char_is_prime_of_two_le R _ _ (m+2) hc (nat.le_add_left 2 m))
 end
 
-lemma char_is_prime_of_pos (p : ℕ) [h : fact (0 < p)] [char_p R p] : fact p.prime :=
-⟨(char_p.char_is_prime_or_zero R _).resolve_right (pos_iff_ne_zero.1 h.1)⟩
+lemma char_is_prime_of_pos (p : ℕ) [ne_zero p] [char_p R p] : fact p.prime :=
+⟨(char_p.char_is_prime_or_zero R _).resolve_right $ ne_zero.ne p⟩
 
 end nontrivial
 
@@ -591,3 +591,15 @@ begin
 end
 
 end
+
+namespace ne_zero
+
+variables (R) [add_monoid_with_one R] {r : R} {n p : ℕ} {a : ℕ+}
+
+lemma of_not_dvd [char_p R p] (h : ¬ p ∣ n) : ne_zero (n : R) :=
+⟨(char_p.cast_eq_zero_iff R p n).not.mpr h⟩
+
+lemma not_char_dvd  (p : ℕ) [char_p R p] (k : ℕ) [h : ne_zero (k : R)] : ¬ p ∣ k :=
+by rwa [←char_p.cast_eq_zero_iff R p k, ←ne.def, ←ne_zero_iff]
+
+end ne_zero

src/algebra/char_p/invertible.lean

@@ -40,9 +40,10 @@ def invertible_of_char_p_not_dvd {p : ℕ} [char_p K p]
   {t : ℕ} (not_dvd : ¬(p ∣ t)) : invertible (t : K) :=
 invertible_of_nonzero (λ h, not_dvd ((char_p.cast_eq_zero_iff K p t).mp h))
 
-instance invertible_of_pos [char_zero K] (n : ℕ) [h : fact (0 < n)] :
-  invertible (n : K) :=
-invertible_of_nonzero $ by simpa [pos_iff_ne_zero] using h.out
+-- warning: this could potentially loop with `ne_zero.invertible` - if there is weird type-class
+-- loops, watch out for that.
+instance invertible_of_pos [char_zero K] (n : ℕ) [ne_zero n] : invertible (n : K) :=
+invertible_of_nonzero $ ne_zero.out
 
 end field
 

src/algebra/invertible.lean

@@ -5,6 +5,7 @@ Authors: Anne Baanen
 -/
 
 import algebra.group.units
+import algebra.ne_zero
 import algebra.ring.basic
 
 /-!
@@ -212,6 +213,9 @@ lemma nonzero_of_invertible [mul_zero_one_class α] (a : α) [nontrivial α] [in
 λ ha, zero_ne_one $ calc   0 = ⅟a * a : by simp [ha]
                          ... = 1 : inv_of_mul_self a
 
+@[priority 100] instance invertible.ne_zero [mul_zero_one_class α] [nontrivial α] (a : α)
+  [invertible a] : ne_zero a := ⟨nonzero_of_invertible a⟩
+
 section monoid_with_zero
 variable [monoid_with_zero α]
 

src/algebra/ne_zero.lean

@@ -3,7 +3,10 @@ Copyright (c) 2021 Eric Rodriguez. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Rodriguez
 -/
-import data.zmod.basic
+
+import data.nat.cast
+import data.pnat.basic
+import algebra.group_power.ring
 
 /-!
 # `ne_zero` typeclass
@@ -30,21 +33,46 @@ lemma ne_zero_iff {R : Type*} [has_zero R] {n : R} : ne_zero n ↔ n ≠ 0 :=
 lemma not_ne_zero {R : Type*} [has_zero R] {n : R} : ¬ ne_zero n ↔ n = 0 :=
 by simp [ne_zero_iff]
 
+lemma eq_zero_or_ne_zero {α} [has_zero α] (a : α) : a = 0 ∨ ne_zero a :=
+(eq_or_ne a 0).imp_right ne_zero.mk
+
 namespace ne_zero
 
 variables {R S M F : Type*} {r : R} {x y : M} {n p : ℕ} {a : ℕ+}
 
 instance pnat : ne_zero (a : ℕ) := ⟨a.ne_zero⟩
 instance succ : ne_zero (n + 1) := ⟨n.succ_ne_zero⟩
 
+instance one (R) [mul_zero_one_class R] [nontrivial R] : ne_zero (1 : R) := ⟨one_ne_zero⟩
+
+lemma pos (r : R) [canonically_ordered_add_monoid R] [ne_zero r] : 0 < r :=
+(zero_le r).lt_of_ne $ ne_zero.out.symm
+
 lemma of_pos [preorder M] [has_zero M] (h : 0 < x) : ne_zero x := ⟨h.ne'⟩
 lemma of_gt  [canonically_ordered_add_monoid M] (h : x < y) : ne_zero y := of_pos $ pos_of_gt h
 
-instance char_zero [ne_zero n] [add_monoid_with_one M] [char_zero M] : ne_zero (n : M) :=
-⟨nat.cast_ne_zero.mpr $ ne_zero.ne n⟩
+-- 1 < p is still an often-used `fact`, due to `nat.prime` implying it, and it implying `nontrivial`
+-- on `zmod`'s ring structure. We cannot just set this to be any `x < y`, else that becomes a
+-- metavariable and it will hugely slow down typeclass inference.
+@[priority 10]
+instance of_gt' [canonically_ordered_add_monoid M] [has_one M] [fact (1 < y)] : ne_zero y :=
+of_gt $ fact.out $ 1 < y
+
+instance bit0 [canonically_ordered_add_monoid M] [ne_zero x] : ne_zero (bit0 x) :=
+of_pos $ bit0_pos $ ne_zero.pos x
+
+instance bit1 [canonically_ordered_comm_semiring M] [nontrivial M] : ne_zero (bit1 x) :=
+⟨mt (λ h, le_iff_exists_add'.2 ⟨_, h.symm⟩) canonically_ordered_comm_semiring.zero_lt_one.not_le⟩
+
+instance pow [monoid_with_zero M] [no_zero_divisors M] [ne_zero x] : ne_zero (x ^ n) :=
+⟨pow_ne_zero n out⟩
+
+instance mul [has_zero M] [has_mul M] [no_zero_divisors M] [ne_zero x] [ne_zero y] :
+  ne_zero (x * y) :=
+⟨mul_ne_zero out out⟩
 
-@[priority 100] instance invertible [mul_zero_one_class M] [nontrivial M] [invertible x] :
-  ne_zero x := ⟨nonzero_of_invertible x⟩
+instance char_zero [ne_zero n] [add_monoid_with_one M] [char_zero M] : ne_zero (n : M) :=
+⟨nat.cast_ne_zero.mpr out⟩
 
 instance coe_trans [has_zero M] [has_coe R S] [has_coe_t S M] [h : ne_zero (r : M)] :
   ne_zero ((r : S) : M) := ⟨h.out⟩
@@ -70,36 +98,12 @@ lemma nat_of_injective [non_assoc_semiring M] [non_assoc_semiring R] [h : ne_zer
   [ring_hom_class F R M] {f : F} (hf : function.injective f) : ne_zero (n : M) :=
  ⟨λ h, (ne_zero.ne' n R) $ hf $ by simpa⟩
 
-lemma pos (r : R) [canonically_ordered_add_monoid R] [ne_zero r] : 0 < r :=
-(zero_le r).lt_of_ne $ ne_zero.out.symm
-
 variables (R M)
 
-lemma of_not_dvd [add_monoid_with_one M] [char_p M p] (h : ¬ p ∣ n) : ne_zero (n : M) :=
-⟨(not_iff_not.mpr $ char_p.cast_eq_zero_iff M p n).mpr h⟩
-
-lemma of_no_zero_smul_divisors (n : ℕ) [comm_ring R] [ne_zero (n : R)] [ring M] [nontrivial M]
-  [algebra R M] [no_zero_smul_divisors R M] : ne_zero (n : M) :=
-nat_of_injective $ no_zero_smul_divisors.algebra_map_injective R M
-
 lemma of_ne_zero_coe [add_monoid_with_one R] [h : ne_zero (n : R)] : ne_zero n :=
 ⟨by {casesI h, rintro rfl, by simpa using h}⟩
 
-lemma not_char_dvd [add_monoid_with_one R] (p : ℕ) [char_p R p] (k : ℕ) [h : ne_zero (k : R)] :
-  ¬ p ∣ k :=
-by rwa [←not_iff_not.mpr $ char_p.cast_eq_zero_iff R p k, ←ne.def, ←ne_zero_iff]
-
 lemma pos_of_ne_zero_coe [add_monoid_with_one R] [ne_zero (n : R)] : 0 < n :=
 (ne_zero.of_ne_zero_coe R).out.bot_lt
 
 end ne_zero
-
-lemma eq_zero_or_ne_zero {α} [has_zero α] (a : α) : a = 0 ∨ ne_zero a :=
-(eq_or_ne a 0).imp_right ne_zero.mk
-
-namespace zmod
-
-instance fintype' (n : ℕ) [ne_zero n] : fintype (zmod n) :=
-@zmod.fintype n ⟨ne_zero.pos n⟩
-
-end zmod

src/control/random.lean

@@ -5,11 +5,11 @@ Authors: Simon Hudon
 -/
 
 import control.monad.basic
+import control.uliftable
+import data.bitvec.basic
 import data.int.basic
 import data.stream.defs
-import control.uliftable
 import tactic.norm_num
-import data.bitvec.basic
 
 
 /-!
@@ -224,7 +224,7 @@ variables {g : Type} [random_gen g]
 open nat
 
 namespace fin
-variables {n : ℕ} [fact (0 < n)]
+variables {n : ℕ} [ne_zero n]
 
 /-- generate a `fin` randomly -/
 protected def random : rand_g g (fin n) :=
@@ -252,7 +252,7 @@ instance int_bounded_random : bounded_random ℤ :=
          (int.coe_nat_le_coe_nat_of_le h₁)
          (le_of_eq $ int.of_nat_nat_abs_eq_of_nonneg (int.sub_nonneg_of_le hxy)) ⟩ }
 
-instance fin_random (n : ℕ) [fact (0 < n)] : random (fin n) :=
+instance fin_random (n : ℕ) [ne_zero n] : random (fin n) :=
 { random := λ g inst, @fin.random g inst _ _ }
 
 instance fin_bounded_random (n : ℕ) : bounded_random (fin n) :=
@@ -284,8 +284,6 @@ instance : bounded_random bool :=
   subtype.map bool.of_nat (bool_of_nat_mem_Icc_of_mem_Icc_to_nat x y) <$>
     @bounded_random.random_r ℕ _ _ g _inst x.to_nat y.to_nat (bool.to_nat_le_to_nat p) }
 
-open_locale fin_fact
-
 /-- generate a random bit vector of length `n` -/
 def bitvec.random (n : ℕ) : rand_g g (bitvec n) :=
 bitvec.of_fin <$> rand.random (fin $ 2^n)

src/data/bitvec/basic.lean

@@ -22,7 +22,7 @@ by rw [of_fin,to_nat_of_nat,nat.mod_eq_of_lt]; apply i.is_lt
 
 /-- convert `bitvec` to `fin` -/
 def to_fin {n : ℕ} (i : bitvec n) : fin $ 2^n :=
-@fin.of_nat' _ ⟨pow_pos (by norm_num) _⟩ i.to_nat
+fin.of_nat' i.to_nat
 
 lemma add_lsb_eq_twice_add_one {x b} :
   add_lsb x b = 2 * x + cond b 1 0 :=

src/data/fin/basic.lean

@@ -3,9 +3,10 @@ Copyright (c) 2017 Robert Y. Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Y. Lewis, Keeley Hoek
 -/
-import tactic.apply_fun
+import algebra.ne_zero
 import data.nat.cast
 import order.rel_iso
+import tactic.apply_fun
 import tactic.localized
 
 /-!
@@ -54,7 +55,7 @@ This file expands on the development in the core library.
 
 ### Other casts
 
-* `fin.of_nat'`: given a positive number `n` (deduced from `[fact (0 < n)]`), `fin.of_nat' i` is
+* `fin.of_nat'`: given a positive number `n` (deduced from `[ne_zero n]`), `fin.of_nat' i` is
   `i % n` interpreted as an element of `fin n`;
 * `fin.cast_lt i h` : embed `i` into a `fin` where `h` proves it belongs into;
 * `fin.pred_above (p : fin n) i` : embed `i : fin (n+1)` into `fin n` by subtracting one if `p < i`;
@@ -77,22 +78,6 @@ open fin nat function
 /-- Elimination principle for the empty set `fin 0`, dependent version. -/
 def fin_zero_elim {α : fin 0 → Sort u} (x : fin 0) : α x := x.elim0
 
-lemma fact.succ.pos {n} : fact (0 < succ n) := ⟨zero_lt_succ _⟩
-
-lemma fact.bit0.pos {n} [h : fact (0 < n)] : fact (0 < bit0 n) :=
-⟨nat.zero_lt_bit0 $ ne_of_gt h.1⟩
-
-lemma fact.bit1.pos {n} : fact (0 < bit1 n) :=
-⟨nat.zero_lt_bit1 _⟩
-
-lemma fact.pow.pos {p n : ℕ} [h : fact $ 0 < p] : fact (0 < p ^ n) :=
-⟨pow_pos h.1 _⟩
-
-localized "attribute [instance] fact.succ.pos" in fin_fact
-localized "attribute [instance] fact.bit0.pos" in fin_fact
-localized "attribute [instance] fact.bit1.pos" in fin_fact
-localized "attribute [instance] fact.pow.pos" in fin_fact
-
 namespace fin
 
 /-- A non-dependent variant of `elim0`. -/
@@ -323,7 +308,7 @@ section add
 -/
 
 /-- Given a positive `n`, `fin.of_nat' i` is `i % n` as an element of `fin n`. -/
-def of_nat' [h : fact (0 < n)] (i : ℕ) : fin n := ⟨i%n, mod_lt _ h.1⟩
+def of_nat' [ne_zero n] (i : ℕ) : fin n := ⟨i%n, mod_lt _ $ ne_zero.pos n⟩
 
 lemma one_val {n : ℕ} : (1 : fin (n+1)).val = 1 % (n+1) := rfl
 lemma coe_one' {n : ℕ} : ((1 : fin (n+1)) : ℕ) = 1 % (n+1) := rfl
@@ -1668,7 +1653,7 @@ lemma coe_of_nat_eq_mod (m n : ℕ) :
   ((n : fin (succ m)) : ℕ) = n % succ m :=
 by rw [← of_nat_eq_coe]; refl
 
-@[simp] lemma coe_of_nat_eq_mod' (m n : ℕ) [I : fact (0 < m)] :
+@[simp] lemma coe_of_nat_eq_mod' (m n : ℕ) [I : ne_zero m] :
   (@fin.of_nat' _ I n : ℕ) = n % m :=
 rfl
 

src/data/nat/basic.lean

@@ -138,19 +138,6 @@ attribute [simp] nat.not_lt_zero nat.succ_ne_zero nat.succ_ne_self
   nat.bit0_ne_one nat.one_ne_bit0
   nat.bit0_ne_bit1 nat.bit1_ne_bit0
 
-/-!
-Inject some simple facts into the type class system.
-This `fact` should not be confused with the factorial function `nat.fact`!
--/
-section facts
-
-instance succ_pos'' (n : ℕ) : fact (0 < n.succ) := ⟨n.succ_pos⟩
-
-instance pos_of_one_lt (n : ℕ) [h : fact (1 < n)] : fact (0 < n) :=
-⟨lt_trans zero_lt_one h.1⟩
-
-end facts
-
 variables {m n k : ℕ}
 namespace nat
 

src/data/nat/totient.lean

@@ -89,13 +89,13 @@ open zmod
 
 /-- Note this takes an explicit `fintype ((zmod n)ˣ)` argument to avoid trouble with instance
 diamonds. -/
-@[simp] lemma _root_.zmod.card_units_eq_totient (n : ℕ) [h : fact (0 < n)] [fintype ((zmod n)ˣ)] :
+@[simp] lemma _root_.zmod.card_units_eq_totient (n : ℕ) [ne_zero n] [fintype ((zmod n)ˣ)] :
   fintype.card ((zmod n)ˣ) = φ n :=
 calc fintype.card ((zmod n)ˣ) = fintype.card {x : zmod n // x.val.coprime n} :
   fintype.card_congr zmod.units_equiv_coprime
 ... = φ n :
 begin
-  unfreezingI { obtain ⟨m, rfl⟩ : ∃ m, n = m + 1 := exists_eq_succ_of_ne_zero h.out.ne' },
+  unfreezingI { obtain ⟨m, rfl⟩ : ∃ m, n = m + 1 := exists_eq_succ_of_ne_zero ne_zero.out },
   simp only [totient, finset.card_eq_sum_ones, fintype.card_subtype, finset.sum_filter,
     ← fin.sum_univ_eq_sum_range, @nat.coprime_comm (m + 1)],
   refl
@@ -104,6 +104,7 @@ end
 lemma totient_even {n : ℕ} (hn : 2 < n) : even n.totient :=
 begin
   haveI : fact (1 < n) := ⟨one_lt_two.trans hn⟩,
+  haveI : ne_zero n := ne_zero.of_gt hn,
   suffices : 2 = order_of (-1 : (zmod n)ˣ),
   { rw [← zmod.card_units_eq_totient, even_iff_two_dvd, this], exact order_of_dvd_card_univ },
   rw [←order_of_units, units.coe_neg_one, order_of_neg_one, ring_char.eq (zmod n) n, if_neg hn.ne'],
@@ -115,9 +116,9 @@ if hmn0 : m * n = 0
     simp only [totient_zero, mul_zero, zero_mul, h]
   else
   begin
-    haveI : fact (0 < (m * n)) := ⟨nat.pos_of_ne_zero hmn0⟩,
-    haveI : fact (0 < m) := ⟨nat.pos_of_ne_zero $ left_ne_zero_of_mul hmn0⟩,
-    haveI : fact (0 < n) := ⟨nat.pos_of_ne_zero $ right_ne_zero_of_mul hmn0⟩,
+    haveI : ne_zero (m * n) := ⟨hmn0⟩,
+    haveI : ne_zero m := ⟨left_ne_zero_of_mul hmn0⟩,
+    haveI : ne_zero n := ⟨right_ne_zero_of_mul hmn0⟩,
     simp only [← zmod.card_units_eq_totient],
     rw [fintype.card_congr (units.map_equiv (zmod.chinese_remainder h).to_mul_equiv).to_equiv,
       fintype.card_congr (@mul_equiv.prod_units (zmod m) (zmod n) _ _).to_equiv,
@@ -226,22 +227,21 @@ end
 lemma card_units_zmod_lt_sub_one {p : ℕ} (hp : 1 < p) [fintype ((zmod p)ˣ)] :
   fintype.card ((zmod p)ˣ) ≤ p - 1 :=
 begin
-  haveI : fact (0 < p) := ⟨zero_lt_one.trans hp⟩,
+  haveI : ne_zero p := ⟨(pos_of_gt hp).ne'⟩,
   rw zmod.card_units_eq_totient p,
   exact nat.le_pred_of_lt (nat.totient_lt p hp),
 end
 
 lemma prime_iff_card_units (p : ℕ) [fintype ((zmod p)ˣ)] :
   p.prime ↔ fintype.card ((zmod p)ˣ) = p - 1 :=
 begin
-  by_cases hp : p = 0,
+  casesI eq_zero_or_ne_zero p with hp hp,
   { substI hp,
     simp only [zmod, not_prime_zero, false_iff, zero_tsub],
     -- the substI created an non-defeq but subsingleton instance diamond; resolve it
     suffices : fintype.card ℤˣ ≠ 0, { convert this },
     simp },
-  haveI : fact (0 < p) := ⟨nat.pos_of_ne_zero hp⟩,
-  rw [zmod.card_units_eq_totient, nat.totient_eq_iff_prime (fact.out (0 < p))],
+  rw [zmod.card_units_eq_totient, nat.totient_eq_iff_prime $ ne_zero.pos p],
 end
 
 @[simp] lemma totient_two : φ 2 = 1 :=