feat: enable cancel_denoms preprocessor in linarith (#3801)

Enable the `cancelDenoms` preprocessor in `linarith`. Closes #2714.

- [x] depends on: #3797


[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/from-referrer/)


Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Patrick Massot <patrickmassot@free.fr>
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib/Algebra/Order/Floor.lean

@@ -1437,26 +1437,18 @@ theorem round_eq (x : α) : round x = ⌊x + 1 / 2⌋ := by
     rw [if_pos hx, self_eq_add_right, floor_eq_iff, cast_zero, zero_add]
     constructor
     . linarith [fract_nonneg x]
-    · -- Porting note: `add_halves` can be removed after linarith learns about fractions
-      linarith [add_halves (1:α)]
+    · linarith
   · have : ⌊fract x + 1 / 2⌋ = 1 := by
       rw [floor_eq_iff]
       constructor
-      . -- norm_num at *
-        -- linarith
-        -- Porting note: linarith broke here after the move to ℚ in norm_num.
-        have := add_le_add_right hx (1/2)
-        norm_num at *
-        assumption
-      · -- Porting note: `norm_num at *` can lose the *, after linarith learns about fractions
-        norm_num at *
+      . norm_num
+        linarith
+      · norm_num
         linarith [fract_lt_one x]
     rw [if_neg (not_lt.mpr hx), ← fract_add_floor x, add_assoc, add_left_comm, floor_int_add,
       ceil_add_int, add_comm _ ⌊x⌋, add_right_inj, ceil_eq_iff, this, cast_one, sub_self]
     constructor
-    . -- Porting note: can be just `norm_num ; linarith` after linarith learns about fractions
-      have : (0:α) < 1/2 := half_pos <| by norm_num
-      linarith
+    . linarith
     · linarith [fract_lt_one x]
 #align round_eq round_eq
 
@@ -1473,18 +1465,14 @@ theorem round_neg_two_inv : round (-2⁻¹ : α) = 0 := by
 @[simp]
 theorem round_eq_zero_iff {x : α} : round x = 0 ↔ x ∈ Ico (-(1 / 2)) ((1 : α) / 2) := by
   rw [round_eq, floor_eq_zero_iff, add_mem_Ico_iff_left]
-  rw [← add_halves (1:α)] -- porting note: line can be removed after norm_num learns about fractions
   norm_num
 #align round_eq_zero_iff round_eq_zero_iff
 
 theorem abs_sub_round (x : α) : |x - round x| ≤ 1 / 2 := by
   rw [round_eq, abs_sub_le_iff]
   have := floor_le (x + 1 / 2)
   have := lt_floor_add_one (x + 1 / 2)
-  constructor
-  . -- Porting note: `add_halves` can be removed after linarith learns about fractions
-    linarith [add_halves (1:α)]
-  . linarith
+  constructor <;> linarith
 #align abs_sub_round abs_sub_round
 
 theorem abs_sub_round_div_natCast_eq {m n : ℕ} :

Mathlib/Analysis/Normed/Order/UpperLower.lean

@@ -133,16 +133,7 @@ theorem IsUpperSet.exists_subset_ball (hs : IsUpperSet s) (hx : x ∈ closure s)
   replace hz := (norm_le_pi_norm _ i).trans hz
   dsimp at hxy hz
   rw [abs_sub_le_iff] at hxy hz
-  -- Porting note: rest of proof was just `linarith`. Probably mathlib4#2714
-  have hxz : x i - z i ≤ -2 / 4 * δ := by
-    have h3 : -2 / 4 * δ - δ / 4 = -(3 / 4 * δ) := by ring
-    linarith
-  have hyz : y i - z i ≤ -δ / 4 := by
-    have t := add_le_add hxy.2 hxz
-    have h1 : δ / 4 + -2 / 4 * δ = -δ / 4 := by ring
-    linarith
-  have hδ4 : -δ / 4 < 0 := div_neg_of_neg_of_pos (Left.neg_neg_iff.mpr hδ) zero_lt_four
-  exact sub_neg.mp (lt_of_le_of_lt hyz hδ4)
+  linarith
 #align is_upper_set.exists_subset_ball IsUpperSet.exists_subset_ball
 
 theorem IsLowerSet.exists_subset_ball (hs : IsLowerSet s) (hx : x ∈ closure s) (hδ : 0 < δ) :
@@ -160,16 +151,7 @@ theorem IsLowerSet.exists_subset_ball (hs : IsLowerSet s) (hx : x ∈ closure s)
   replace hz := (norm_le_pi_norm _ i).trans hz
   dsimp at hxy hz
   rw [abs_sub_le_iff] at hxy hz
-  -- Porting note: rest of proof was just `linarith`. Probably mathlib4#2714
-  have hzx : z i - x i ≤ -2 / 4 * δ := by
-    have h3 : -2 / 4 * δ - δ / 4 = -(3 / 4 * δ) := by ring
-    linarith
-  have hzy : z i - y i ≤ -δ / 4 := by
-    have t := add_le_add hzx hxy.1
-    have h1 : -2 / 4 * δ + δ / 4 = -δ / 4 := by ring
-    linarith
-  have hδ4 : -δ / 4 < 0 := div_neg_of_neg_of_pos (Left.neg_neg_iff.mpr hδ) zero_lt_four
-  exact sub_neg.mp (lt_of_le_of_lt hzy hδ4)
+  linarith
 #align is_lower_set.exists_subset_ball IsLowerSet.exists_subset_ball
 
 end Fintype

Mathlib/Data/Complex/Exponential.lean

@@ -1696,27 +1696,13 @@ theorem exp_bound' {x : ℂ} {n : ℕ} (hx : abs x / n.succ ≤ 1 / 2) :
     · simp_rw [← div_pow]
       rw [geom_sum_eq, div_le_iff_of_neg]
       · trans (-1 : ℝ)
-        · -- Porting note: was linarith
-          simp [Nat.succ_eq_add_one] at hx
-          rw [mul_comm, ← le_div_iff]
-          simp [hx]
-          . norm_num [this, hx]
-            simp [hx]
-          . exact zero_lt_two
+        · linarith
         · simp only [neg_le_sub_iff_le_add, div_pow, Nat.cast_succ, le_add_iff_nonneg_left]
           exact
             div_nonneg (pow_nonneg (abs.nonneg x) k)
               (pow_nonneg (add_nonneg n.cast_nonneg zero_le_one) k)
-      · -- Porting note: was linarith
-        simp [Nat.succ_eq_add_one] at hx
-        simp
-        apply lt_of_le_of_lt hx
-        norm_num
-      · -- Porting note: was linarith
-        intro h
-        simp at h
-        simp [h] at hx
-        norm_num at hx
+      · linarith
+      · linarith
     · exact div_nonneg (pow_nonneg (abs.nonneg x) n) (Nat.cast_nonneg n.factorial)
 #align complex.exp_bound' Complex.exp_bound'
 
@@ -1941,9 +1927,7 @@ theorem sin_pos_of_pos_of_le_one {x : ℝ} (hx0 : 0 < x) (hx : x ≤ 1) : 0 < si
                     x ^ 3 ≤ x ^ 1 := pow_le_pow_of_le_one (le_of_lt hx0) hx (by decide)
                     _ = x := pow_one _
                     ))
-            --Porting note : was `_ < x := by linarith`
-            _ = x * (7 / 32) := by ring
-            _ < x := (mul_lt_iff_lt_one_right hx0).2 (by norm_num))
+            _ < x := by linarith)
     _ ≤ sin x :=
       sub_le_comm.1 (abs_sub_le_iff.1 (sin_bound (by rwa [_root_.abs_of_nonneg (le_of_lt hx0)]))).2
 #align real.sin_pos_of_pos_of_le_one Real.sin_pos_of_pos_of_le_one

Mathlib/Data/Nat/Digits.lean

@@ -633,10 +633,8 @@ namespace NormDigits
 theorem digits_succ (b n m r l) (e : r + b * m = n) (hr : r < b)
     (h : Nat.digits b m = l ∧ 1 < b ∧ 0 < m) : (Nat.digits b n = r :: l) ∧ 1 < b ∧ 0 < n := by
   rcases h with ⟨h, b2, m0⟩
-  -- Porting note: Below line was proved by `by linarith`
-  have b0 : 0 < b := by simp_arith [lt_iff_le_and_ne.mp b2]
-  -- Porting note: Below line was proved by `by linarith [mul_pos b0 m0]`
-  have n0 : 0 < n := le_trans (lt_iff_add_one_le.mp (mul_pos b0 m0)) (e.subst (le_add_left _ r))
+  have b0 : 0 < b := by linarith
+  have n0 : 0 < n := by linarith [mul_pos b0 m0]
   refine' ⟨_, b2, n0⟩
   obtain ⟨rfl, rfl⟩ := (Nat.div_mod_unique b0).2 ⟨e, hr⟩
   subst h; exact Nat.digits_def' b2 n0

Mathlib/GroupTheory/Perm/Cycle/Type.lean

@@ -583,8 +583,7 @@ theorem _root_.card_support_eq_three_iff : σ.support.card = 3 ↔ σ.IsThreeCyc
   obtain ⟨m, hm⟩ := exists_mem_of_ne_zero h1
   rw [← sum_cycleType, ← cons_erase hn, ← cons_erase hm, Multiset.sum_cons, Multiset.sum_cons] at h
   -- TODO: linarith [...] should solve this directly
-  have : ∀ {k}, 2 ≤ m → 2 ≤ n → n + (m + k) = 3 → False :=
-    by
+  have : ∀ {k}, 2 ≤ m → 2 ≤ n → n + (m + k) = 3 → False := by
     intros
     linarith
   cases this (two_le_of_mem_cycleType (mem_of_mem_erase hm)) (two_le_of_mem_cycleType hn) h

Mathlib/Lean/Expr/Basic.lean

@@ -340,6 +340,30 @@ def mkProjection (e : Expr) (fieldName : Name) : MetaM Expr := do
     e := mkAppN (.const projName us) (type.getAppArgs.push e)
   mkDirectProjection e fieldName
 
+/-- Returns true if `e` contains a name `n` where `p n` is true. -/
+def containsConst (e : Expr) (p : Name → Bool) : Bool :=
+  Option.isSome <| e.find? fun | .const n _ => p n | _ => false
+
+/--
+Rewrites `e` via some `eq`, producing a proof `e = e'` for some `e'`.
+
+Rewrites with a fresh metavariable as the ambient goal.
+Fails if the rewrite produces any subgoals.
+-/
+def rewrite (e eq : Expr) : MetaM Expr := do
+  let ⟨_, eq', []⟩ ← (← mkFreshExprMVar none).mvarId!.rewrite e eq
+    | throwError "Expr.rewrite may not produce subgoals."
+  return eq'
+
+/--
+Rewrites the type of `e` via some `eq`, then moves `e` into the new type via `Eq.mp`.
+
+Rewrites with a fresh metavariable as the ambient goal.
+Fails if the rewrite produces any subgoals.
+-/
+def rewriteType (e eq : Expr) : MetaM Expr := do
+  mkEqMP (← (← inferType e).rewrite eq) e
+
 end Expr
 
 /-- Get the projections that are projections to parent structures. Similar to `getParentStructures`,

Mathlib/Tactic/Linarith/Datatypes.lean

@@ -266,16 +266,16 @@ structure GlobalBranchingPreprocessor : Type where
 /--
 A `Preprocessor` lifts to a `GlobalPreprocessor` by folding it over the input list.
 -/
-def Preprocessor.globalize (pp : Preprocessor) : GlobalPreprocessor :=
-{ name := pp.name,
-  transform := List.foldrM (fun e ret => do return (← pp.transform e) ++ ret) [] }
+def Preprocessor.globalize (pp : Preprocessor) : GlobalPreprocessor where
+  name := pp.name
+  transform := List.foldrM (fun e ret => do return (← pp.transform e) ++ ret) []
 
 /--
 A `GlobalPreprocessor` lifts to a `GlobalBranchingPreprocessor` by producing only one branch.
 -/
-def GlobalPreprocessor.branching (pp : GlobalPreprocessor) : GlobalBranchingPreprocessor :=
-{ name := pp.name,
-  transform := fun g l => do return [⟨g, ← pp.transform l⟩] }
+def GlobalPreprocessor.branching (pp : GlobalPreprocessor) : GlobalBranchingPreprocessor where
+  name := pp.name
+  transform := fun g l => do return [⟨g, ← pp.transform l⟩]
 
 /--
 `process pp l` runs `pp.transform` on `l` and returns the result,

Mathlib/Tactic/Linarith/Preprocessing.lean

@@ -6,6 +6,7 @@ Ported by: Scott Morrison
 -/
 import Mathlib.Tactic.Linarith.Datatypes
 import Mathlib.Tactic.Zify
+import Mathlib.Tactic.CancelDenoms
 import Mathlib.Lean.Exception
 import Std.Data.RBMap.Basic
 import Mathlib.Data.HashMap
@@ -276,31 +277,39 @@ def compWithZero : Preprocessor where
 
 end compWithZero
 
--- FIXME the `cancelDenoms : Preprocessor` from mathlib3 will need to wait
--- for a port of the `cancel_denoms` tactic.
 section cancelDenoms
--- /--
--- `normalize_denominators_in_lhs h lhs` assumes that `h` is a proof of `lhs R 0`.
--- It creates a proof of `lhs' R 0`, where all numeric division in `lhs` has been cancelled.
--- -/
--- meta def normalize_denominators_in_lhs (h lhs : expr) : tactic expr :=
--- do (v, lhs') ← cancel_factors.derive lhs,
---    if v = 1 then return h else do
---    (ih, h'') ← mk_single_comp_zero_pf v h,
---    (_, nep, _) ← infer_type h'' >>= rewrite_core lhs',
---    mk_eq_mp nep h''
 
--- /--
--- `cancel_denoms pf` assumes `pf` is a proof of `t R 0`. If `t` contains the division symbol `/`,
--- it tries to scale `t` to cancel out division by numerals.
--- -/
--- meta def cancel_denoms : preprocessor :=
--- { name := "cancel denominators",
---   transform := λ pf,
--- (do some (_, lhs) ← parse_into_comp_and_expr <$> infer_type pf,
---    guardb $ lhs.contains_constant (= `has_div.div),
---    singleton <$> normalize_denominators_in_lhs pf lhs)
--- <|> return [pf] }
+theorem without_one_mul [MulOneClass M] {a b : M} (h : 1 * a = b) : a = b := by rwa [one_mul] at h
+
+/--
+`normalizeDenominatorsLHS h lhs` assumes that `h` is a proof of `lhs R 0`.
+It creates a proof of `lhs' R 0`, where all numeric division in `lhs` has been cancelled.
+-/
+def normalizeDenominatorsLHS (h lhs : Expr) : MetaM Expr := do
+  let mut (v, lhs') ← CancelDenoms.derive lhs
+  if v = 1 then
+    -- `lhs'` has a `1 *` out front, but `mkSingleCompZeroOf` has a special case
+    -- where it does not produce `1 *`. We strip it off here:
+    lhs' ← mkAppM ``without_one_mul #[lhs']
+  let (_, h'') ← mkSingleCompZeroOf v h
+  try
+    h''.rewriteType lhs'
+  catch e =>
+    dbg_trace
+      s!"Error in Linarith.normalizeDenominatorsLHS: {← e.toMessageData.toString}"
+    throw e
+
+/--
+`cancelDenoms pf` assumes `pf` is a proof of `t R 0`. If `t` contains the division symbol `/`,
+it tries to scale `t` to cancel out division by numerals.
+-/
+def cancelDenoms : Preprocessor where
+  name := "cancel denominators"
+  transform := fun pf => (do
+      let (_, lhs) ← parseCompAndExpr (← inferType pf)
+      guard $ lhs.containsConst (fun n => n = ``HDiv.hDiv || n = ``Div.div)
+      pure [← normalizeDenominatorsLHS pf lhs])
+    <|> return [pf]
 end cancelDenoms
 
 section nlinarith
@@ -405,7 +414,7 @@ The default list of preprocessors, in the order they should typically run.
 -/
 def defaultPreprocessors : List GlobalBranchingPreprocessor :=
   [filterComparisons, removeNegations, natToInt, strengthenStrictInt,
-    compWithZero/-, cancelDenoms-/]
+    compWithZero, cancelDenoms]
 
 /--
 `preprocess pps l` takes a list `l` of proofs of propositions.

Mathlib/Topology/Homotopy/Basic.lean

@@ -270,9 +270,7 @@ theorem symm_trans {f₀ f₁ f₂ : C(X, Y)} (F : Homotopy f₀ f₁) (G : Homo
   rw [trans_apply, symm_apply, trans_apply]
   simp only [coe_symm_eq, symm_apply]
   split_ifs with h₁ h₂ h₂
-  . have ht : (t : ℝ) = 1 / 2 :=
-      -- porting note: this was proved by linarith in mathlib
-      le_antisymm h₂ (by convert sub_le_comm.mp h₁ using 1; norm_num)
+  . have ht : (t : ℝ) = 1 / 2 := by linarith
     simp only [ht]
     norm_num
   . congr 2
@@ -284,11 +282,7 @@ theorem symm_trans {f₀ f₁ f₂ : C(X, Y)} (F : Homotopy f₀ f₁) (G : Homo
     simp only [coe_symm_eq]
     linarith
   . exfalso
-    -- porting note: this was proved by linarith in mathlib
-    apply h₂
-    rw [sub_le_comm, not_le] at h₁
-    convert le_of_lt h₁ using 1
-    norm_num
+    linarith
 #align continuous_map.homotopy.symm_trans ContinuousMap.Homotopy.symm_trans
 
 /-- Casting a `Homotopy f₀ f₁` to a `Homotopy g₀ g₁` where `f₀ = g₀` and `f₁ = g₁`.

Mathlib/Topology/MetricSpace/Basic.lean

@@ -449,8 +449,7 @@ contains it.
 See also `exists_lt_subset_ball`. -/
 theorem exists_lt_mem_ball_of_mem_ball (h : x ∈ ball y ε) : ∃ ε' < ε, x ∈ ball y ε' := by
   simp only [mem_ball] at h ⊢
-  -- porting note: todo: Mathlib 3 used `by linarith` here
-  exact ⟨(dist x y + ε) / 2, add_div_two_lt_right.2 h, left_lt_add_div_two.2 h⟩
+  exact ⟨(dist x y + ε) / 2, by linarith, by linarith⟩
 #align metric.exists_lt_mem_ball_of_mem_ball Metric.exists_lt_mem_ball_of_mem_ball
 
 theorem ball_eq_ball (ε : ℝ) (x : α) :

Mathlib/Topology/MetricSpace/CantorScheme.lean

@@ -134,19 +134,16 @@ theorem VanishingDiam.dist_lt (hA : VanishingDiam A) (ε : ℝ) (ε_pos : 0 < ε
     ∃ n : ℕ, ∀ (y) (_ : y ∈ A (res x n)) (z) (_ : z ∈ A (res x n)), dist y z < ε := by
   specialize hA x
   rw [ENNReal.tendsto_atTop_zero] at hA
-  cases'
-    hA (ENNReal.ofReal (ε / 2))
-      (by
-        simp only [gt_iff_lt, ENNReal.ofReal_pos]
-        exact half_pos ε_pos) with -- Porting note: was `linarith`
-    n hn
+  cases' hA (ENNReal.ofReal (ε / 2)) (by
+    simp only [gt_iff_lt, ENNReal.ofReal_pos]
+    linarith) with n hn
   use n
   intro y hy z hz
   rw [← ENNReal.ofReal_lt_ofReal_iff ε_pos, ← edist_dist]
   apply lt_of_le_of_lt (EMetric.edist_le_diam_of_mem hy hz)
   apply lt_of_le_of_lt (hn _ (le_refl _))
   rw [ENNReal.ofReal_lt_ofReal_iff ε_pos]
-  exact half_lt_self ε_pos -- Porting note: was `linarith`
+  linarith
 #align cantor_scheme.vanishing_diam.dist_lt CantorScheme.VanishingDiam.dist_lt
 
 /-- A scheme with vanishing diameter along each branch induces a continuous map. -/