feat(tactic/positivity): Handle a ≠ 0 assumptions (#16529)

Make `positivity` handle `a ≠ 0` assumptions. This involves
* adding a third constructor to `positivity.strictness`, that I've called `nonzero`. It is meant to hold proofs of `a ≠ 0`, not `0 ≠ a`
* modifying the existing extensions to handle that new case.
* changing `positivity.orelse'` to account for the fact that if we can prove `0 ≤ a` and `a ≠ 0` then we can prove `0 < a`.
* making `compare_hyp` handle `eq` and `ne` hypotheses.

## Other changes

* Introduce `tac1 ≤|≥ tac2` as notation for `positivity.orelse' tac1 tac2`. This has the same precedence as the `<|>` notation for `orelse`.
* Make `positivity` extensions fail with more informative error messages. This is useless when running `positivity` alone but:
  * It clearly marks within the code what each failure means
  * The errors can show up when calling an extension directly. Not sure why you would do that, but you could.
* Add a `has_to_format strictness` instance. This is mostly useful for debugging.

src/algebra/order/floor.lean

@@ -949,6 +949,7 @@ meta def positivity_floor : expr → tactic strictness
       match strictness_a with
       | positive p := nonnegative <$> mk_app ``int_floor_nonneg_of_pos [p]
       | nonnegative p := nonnegative <$> mk_app ``int_floor_nonneg [p]
+      | _ := failed
       end
 | e := pp e >>= fail ∘ format.bracket "The expression `" "` is not of the form `⌊a⌋`"
 
@@ -969,6 +970,7 @@ meta def positivity_ceil : expr → tactic strictness
       match strictness_a with
       | positive p := positive <$> mk_app ``int_ceil_pos [p]
       | nonnegative p := nonnegative <$> mk_app ``int.ceil_nonneg [p]
+      | _ := failed
       end
 | e := pp e >>= fail ∘ format.bracket "The expression `" "` is not of the form `⌈a⌉₊` nor `⌈a⌉`"
 

src/algebra/order/smul.lean

@@ -256,6 +256,7 @@ variables {M}
 end linear_ordered_semifield
 
 namespace tactic
+section ordered_smul
 variables [ordered_semiring R] [ordered_add_comm_monoid M] [smul_with_zero R M] [ordered_smul R M]
   {a : R} {b : M}
 
@@ -265,21 +266,38 @@ smul_nonneg ha.le hb
 private lemma smul_nonneg_of_nonneg_of_pos (ha : 0 ≤ a) (hb : 0 < b) : 0 ≤ a • b :=
 smul_nonneg ha hb.le
 
+end ordered_smul
+
+section no_zero_smul_divisors
+variables [has_zero R] [has_zero M] [has_smul R M] [no_zero_smul_divisors R M] {a : R} {b : M}
+
+private lemma smul_ne_zero_of_pos_of_ne_zero [preorder R] (ha : 0 < a) (hb : b ≠ 0) : a • b ≠ 0 :=
+smul_ne_zero ha.ne' hb
+
+private lemma smul_ne_zero_of_ne_zero_of_pos [preorder M] (ha : a ≠ 0) (hb : 0 < b) : a • b ≠ 0 :=
+smul_ne_zero ha hb.ne'
+
+end no_zero_smul_divisors
+
 open positivity
 
-/-- Extension for the `positivity` tactic: scalar multiplication is nonnegative if both sides are
-nonnegative, and strictly positive if both sides are. -/
+/-- Extension for the `positivity` tactic: scalar multiplication is nonnegative/positive/nonzero if
+both sides are. -/
 @[positivity]
 meta def positivity_smul : expr → tactic strictness
-| `(%%a • %%b) := do
+| e@`(%%a • %%b) := do
   strictness_a ← core a,
   strictness_b ← core b,
   match strictness_a, strictness_b with
   | positive pa, positive pb := positive <$> mk_app ``smul_pos [pa, pb]
   | positive pa, nonnegative pb := nonnegative <$> mk_app ``smul_nonneg_of_pos_of_nonneg [pa, pb]
   | nonnegative pa, positive pb := nonnegative <$> mk_app ``smul_nonneg_of_nonneg_of_pos [pa, pb]
   | nonnegative pa, nonnegative pb := nonnegative <$> mk_app ``smul_nonneg [pa, pb]
+  | positive pa, nonzero pb := nonzero <$> to_expr ``(smul_ne_zero_of_pos_of_ne_zero %%pa %%pb)
+  | nonzero pa, positive pb := nonzero <$> to_expr ``(smul_ne_zero_of_ne_zero_of_pos %%pa %%pb)
+  | nonzero pa, nonzero pb := nonzero <$> to_expr ``(smul_ne_zero %%pa %%pb)
+  | sa@_, sb@ _ := positivity_fail e a b sa sb
   end
-| _ := failed
+| e := pp e >>= fail ∘ format.bracket "The expression `" "` isn't of the form `a • b`"
 
 end tactic

src/analysis/special_functions/pow.lean

@@ -2159,6 +2159,7 @@ do
   match strictness_a with
   | nonnegative p := nonnegative <$> mk_app ``real.rpow_nonneg_of_nonneg [p, b]
   | positive p := positive <$> mk_app ``real.rpow_pos_of_pos [p, b]
+  | _ := failed
   end
 
 private lemma nnrpow_pos {a : ℝ≥0} (ha : 0 < a) (b : ℝ) : 0 < a ^ b := nnreal.rpow_pos ha

src/data/real/ereal.lean

@@ -49,10 +49,11 @@ also do some limits stuff (liminf/limsup etc).
 See https://isabelle.in.tum.de/dist/library/HOL/HOL-Library/Extended_Real.html
 -/
 
+open function
 open_locale ennreal nnreal
 
 /-- ereal : The type `[-∞, ∞]` -/
-@[derive [has_top, comm_monoid_with_zero,
+@[derive [has_top, comm_monoid_with_zero, nontrivial,
   has_Sup, has_Inf, complete_linear_order, linear_ordered_add_comm_monoid_with_top]]
 def ereal := with_top (with_bot ℝ)
 
@@ -69,12 +70,19 @@ instance : has_bot ereal := ⟨some ⊥⟩
 @[simp] lemma bot_ne_top : (⊥ : ereal) ≠ ⊤ := bot_lt_top.ne
 
 instance : has_coe ℝ ereal := ⟨real.to_ereal⟩
+
+lemma coe_strict_mono : strict_mono (coe : ℝ → ereal) :=
+with_top.coe_strict_mono.comp with_bot.coe_strict_mono
+
+lemma coe_injective : injective (coe : ℝ → ereal) := coe_strict_mono.injective
+
 @[simp, norm_cast] protected lemma coe_le_coe_iff {x y : ℝ} : (x : ereal) ≤ (y : ereal) ↔ x ≤ y :=
-by { unfold_coes, simp [real.to_ereal] }
+coe_strict_mono.le_iff_le
 @[simp, norm_cast] protected lemma coe_lt_coe_iff {x y : ℝ} : (x : ereal) < (y : ereal) ↔ x < y :=
-by { unfold_coes, simp [real.to_ereal] }
+coe_strict_mono.lt_iff_lt
 @[simp, norm_cast] protected lemma coe_eq_coe_iff {x y : ℝ} : (x : ereal) = (y : ereal) ↔ x = y :=
-by { unfold_coes, simp [real.to_ereal, option.some_inj] }
+coe_injective.eq_iff
+protected lemma coe_ne_coe_iff {x y : ℝ} : (x : ereal) ≠ (y : ereal) ↔ x ≠ y := coe_injective.ne_iff
 
 /-- The canonical map from nonnegative extended reals to extended reals -/
 def _root_.ennreal.to_ereal : ℝ≥0∞ → ereal
@@ -154,6 +162,11 @@ rfl
 
 @[simp, norm_cast] lemma coe_zero : ((0 : ℝ) : ereal) = 0 := rfl
 
+@[simp, norm_cast] lemma coe_eq_zero {x : ℝ} : (x : ereal) = 0 ↔ x = 0 := ereal.coe_eq_coe_iff
+@[simp, norm_cast] lemma coe_eq_one {x : ℝ} : (x : ereal) = 1 ↔ x = 1 := ereal.coe_eq_coe_iff
+lemma coe_ne_zero {x : ℝ} : (x : ereal) ≠ 0 ↔ x ≠ 0 := ereal.coe_ne_coe_iff
+lemma coe_ne_one {x : ℝ} : (x : ereal) ≠ 1 ↔ x ≠ 1 := ereal.coe_ne_coe_iff
+
 @[simp, norm_cast] protected lemma coe_nonneg {x : ℝ} : (0 : ereal) ≤ x ↔ 0 ≤ x :=
 ereal.coe_le_coe_iff
 
@@ -225,6 +238,7 @@ end
 lemma coe_nnreal_eq_coe_real (x : ℝ≥0) : ((x : ℝ≥0∞) : ereal) = (x : ℝ) := rfl
 
 @[simp, norm_cast] lemma coe_ennreal_zero : ((0 : ℝ≥0∞) : ereal) = 0 := rfl
+@[simp, norm_cast] lemma coe_ennreal_one : ((1 : ℝ≥0∞) : ereal) = 1 := rfl
 @[simp, norm_cast] lemma coe_ennreal_top : ((⊤ : ℝ≥0∞) : ereal) = ⊤ := rfl
 
 @[simp] lemma coe_ennreal_eq_top_iff : ∀ {x : ℝ≥0∞}, (x : ereal) = ⊤ ↔ x = ⊤
@@ -255,6 +269,17 @@ lemma coe_nnreal_ne_top (x : ℝ≥0) : ((x : ℝ≥0∞) : ereal) ≠ ⊤ := de
 | ⊤ (some y) := by simp [(coe_nnreal_lt_top y).ne']
 | (some x) (some y) := by simp [coe_nnreal_eq_coe_real]
 
+@[simp, norm_cast] lemma coe_ennreal_eq_zero {x : ℝ≥0∞} : (x : ereal) = 0 ↔ x = 0 :=
+by rw [←coe_ennreal_eq_coe_ennreal_iff, coe_ennreal_zero]
+
+@[simp, norm_cast] lemma coe_ennreal_eq_one {x : ℝ≥0∞} : (x : ereal) = 1 ↔ x = 1 :=
+by rw [←coe_ennreal_eq_coe_ennreal_iff, coe_ennreal_one]
+
+@[norm_cast] lemma coe_ennreal_ne_zero {x : ℝ≥0∞} : (x : ereal) ≠ 0 ↔ x ≠ 0 :=
+coe_ennreal_eq_zero.not
+
+@[norm_cast] lemma coe_ennreal_ne_one {x : ℝ≥0∞} : (x : ereal) ≠ 1 ↔ x ≠ 1 := coe_ennreal_eq_one.not
+
 lemma coe_ennreal_nonneg (x : ℝ≥0∞) : (0 : ereal) ≤ x :=
 coe_ennreal_le_coe_ennreal_iff.2 (zero_le x)
 
@@ -531,6 +556,7 @@ end ereal
 namespace tactic
 open positivity
 
+private lemma ereal_coe_ne_zero {r : ℝ} : r ≠ 0 → (r : ereal) ≠ 0 := ereal.coe_ne_zero.2
 private lemma ereal_coe_nonneg {r : ℝ} : 0 ≤ r → 0 ≤ (r : ereal) := ereal.coe_nonneg.2
 private lemma ereal_coe_pos {r : ℝ} : 0 < r → 0 < (r : ereal) := ereal.coe_pos.2
 private lemma ereal_coe_ennreal_pos {r : ℝ≥0∞} : 0 < r → 0 < (r : ereal) := ereal.coe_ennreal_pos.2
@@ -544,6 +570,7 @@ meta def positivity_coe_real_ereal : expr → tactic strictness
   match strictness_a with
   | positive p := positive <$> mk_app ``ereal_coe_pos [p]
   | nonnegative p := nonnegative <$> mk_mapp ``ereal_coe_nonneg [a, p]
+  | nonzero p := nonzero <$> mk_mapp ``ereal_coe_ne_zero [a, p]
   end
 | e := pp e >>= fail ∘ format.bracket "The expression "
          " is not of the form `(r : ereal)` for `r : ℝ`"
@@ -556,7 +583,7 @@ meta def positivity_coe_ennreal_ereal : expr → tactic strictness
   strictness_a ← core a,
   match strictness_a with
   | positive p := positive <$> mk_app ``ereal_coe_ennreal_pos [p]
-  | nonnegative _ := nonnegative <$> mk_mapp `ereal.coe_ennreal_nonneg [a]
+  | _ := nonnegative <$> mk_mapp `ereal.coe_ennreal_nonneg [a]
   end
 | e := pp e >>= fail ∘ format.bracket "The expression "
          " is not of the form `(r : ereal)` for `r : ℝ≥0∞`"

src/data/real/hyperreal.lean

@@ -23,12 +23,13 @@ notation `ℝ*` := hyperreal
 
 noncomputable instance : has_coe_t ℝ ℝ* := ⟨λ x, (↑x : germ _ _)⟩
 
-@[simp, norm_cast]
-lemma coe_eq_coe {x y : ℝ} : (x : ℝ*) = y ↔ x = y :=
-germ.const_inj
+@[simp, norm_cast] lemma coe_eq_coe {x y : ℝ} : (x : ℝ*) = y ↔ x = y := germ.const_inj
+lemma coe_ne_coe {x y : ℝ} : (x : ℝ*) ≠ y ↔ x ≠ y := coe_eq_coe.not
 
 @[simp, norm_cast] lemma coe_eq_zero {x : ℝ} : (x : ℝ*) = 0 ↔ x = 0 := coe_eq_coe
 @[simp, norm_cast] lemma coe_eq_one {x : ℝ} : (x : ℝ*) = 1 ↔ x = 1 := coe_eq_coe
+@[norm_cast] lemma coe_ne_zero {x : ℝ} : (x : ℝ*) ≠ 0 ↔ x ≠ 0 := coe_ne_coe
+@[norm_cast] lemma coe_ne_one {x : ℝ} : (x : ℝ*) ≠ 1 ↔ x ≠ 1 := coe_ne_coe
 
 @[simp, norm_cast] lemma coe_one : ↑(1 : ℝ) = (1 : ℝ*) := rfl
 @[simp, norm_cast] lemma coe_zero : ↑(0 : ℝ) = (0 : ℝ*) := rfl
@@ -793,6 +794,7 @@ end hyperreal
 namespace tactic
 open positivity
 
+private lemma hyperreal_coe_ne_zero {r : ℝ} : r ≠ 0 → (r : ℝ*) ≠ 0 := hyperreal.coe_ne_zero.2
 private lemma hyperreal_coe_nonneg {r : ℝ} : 0 ≤ r → 0 ≤ (r : ℝ*) := hyperreal.coe_nonneg.2
 private lemma hyperreal_coe_pos {r : ℝ} : 0 < r → 0 < (r : ℝ*) := hyperreal.coe_pos.2
 
@@ -805,6 +807,7 @@ meta def positivity_coe_real_hyperreal : expr → tactic strictness
   match strictness_a with
   | positive p := positive <$> mk_app ``hyperreal_coe_pos [p]
   | nonnegative p := nonnegative <$> mk_app ``hyperreal_coe_nonneg [p]
+  | nonzero p := nonzero <$> mk_app ``hyperreal_coe_ne_zero [p]
   end
 | e := pp e >>= fail ∘ format.bracket "The expression " " is not of the form `(r : ℝ*)` for `r : ℝ`"
 

src/data/real/nnreal.lean

@@ -852,7 +852,7 @@ meta def positivity_coe_nnreal_real : expr → tactic strictness
   strictness_a ← core a,
   match strictness_a with
   | positive p := positive <$> mk_app ``nnreal_coe_pos [p]
-  | nonnegative _ := nonnegative <$> mk_app ``nnreal.coe_nonneg [a]
+  | _ := nonnegative <$> mk_app ``nnreal.coe_nonneg [a]
   end
 | e := pp e >>= fail ∘ format.bracket "The expression "
          " is not of the form `(r : ℝ)` for `r : ℝ≥0`"

src/order/bounded_order.lean

@@ -688,6 +688,8 @@ instance [partial_order α] : partial_order (with_bot α) :=
   end,
   .. with_bot.preorder }
 
+lemma coe_strict_mono [preorder α] : strict_mono (coe : α → with_bot α) := λ a b, some_lt_some.2
+
 lemma map_le_iff [preorder α] [preorder β] (f : α → β) (mono_iff : ∀ {a b}, f a ≤ f b ↔ a ≤ b) :
   ∀ (a b : with_bot α), a.map f ≤ b.map f ↔ a ≤ b
 | ⊥       _       := by simp only [map_bot, bot_le]
@@ -1155,6 +1157,8 @@ instance [partial_order α] : partial_order (with_top α) :=
 { le_antisymm := λ _ _, by { simp_rw [←to_dual_le_to_dual_iff], exact function.swap le_antisymm },
   .. with_top.preorder }
 
+lemma coe_strict_mono [preorder α] : strict_mono (coe : α → with_top α) := λ a b, some_lt_some.2
+
 lemma map_le_iff [preorder α] [preorder β] (f : α → β)
   (a b : with_top α) (mono_iff : ∀ {a b}, f a ≤ f b ↔ a ≤ b) :
   a.map f ≤ b.map f ↔ a ≤ b :=
@@ -1777,11 +1781,9 @@ section nontrivial
 
 variables [partial_order α] [bounded_order α] [nontrivial α]
 
-lemma bot_ne_top : (⊥ : α) ≠ ⊤ :=
-λ H, not_nontrivial_iff_subsingleton.mpr (subsingleton_of_bot_eq_top H) ‹_›
-
-lemma top_ne_bot : (⊤ : α) ≠ ⊥ := bot_ne_top.symm
-lemma bot_lt_top : (⊥ : α) < ⊤ := lt_top_iff_ne_top.2 bot_ne_top
+@[simp] lemma bot_ne_top : (⊥ : α) ≠ ⊤ := λ h, not_subsingleton _ $ subsingleton_of_bot_eq_top h
+@[simp] lemma top_ne_bot : (⊤ : α) ≠ ⊥ := bot_ne_top.symm
+@[simp] lemma bot_lt_top : (⊥ : α) < ⊤ := lt_top_iff_ne_top.2 bot_ne_top
 
 end nontrivial
 

src/ring_theory/dedekind_domain/ideal.lean

@@ -585,10 +585,8 @@ noncomputable instance fractional_ideal.semifield :
   inv_zero := inv_zero' _,
   div := (/),
   div_eq_mul_inv := fractional_ideal.div_eq_mul_inv,
-  exists_pair_ne := ⟨0, 1, (coe_to_fractional_ideal_injective le_rfl).ne
-    (by simpa using @zero_ne_one (ideal A) _ _)⟩,
   mul_inv_cancel := λ I, fractional_ideal.mul_inv_cancel,
-  .. fractional_ideal.comm_semiring }
+  .. fractional_ideal.comm_semiring, ..(coe_to_fractional_ideal_injective le_rfl).nontrivial }
 
 /-- Fractional ideals have cancellative multiplication in a Dedekind domain.