feat: patch for std4#196 (more min/max lemmas for Nat) (#8074)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib/Data/List/Basic.lean

@@ -1888,13 +1888,13 @@ theorem take_take : ∀ (n m) (l : List α), take n (take m l) = take (min n m)
   | 0, m, l => by rw [zero_min, take_zero, take_zero]
   | succ n, succ m, nil => by simp only [take_nil]
   | succ n, succ m, a :: l => by
-    simp only [take, min_succ_succ, take_take n m l]
+    simp only [take, succ_min_succ, take_take n m l]
 #align list.take_take List.take_take
 
 theorem take_replicate (a : α) : ∀ n m : ℕ, take n (replicate m a) = replicate (min n m) a
   | n, 0 => by simp
   | 0, m => by simp
-  | succ n, succ m => by simp [min_succ_succ, take_replicate]
+  | succ n, succ m => by simp [succ_min_succ, take_replicate]
 #align list.take_replicate List.take_replicate
 
 theorem map_take {α β : Type*} (f : α → β) :
@@ -1986,7 +1986,7 @@ theorem take_eq_take :
   | _ :: xs, 0, 0 => by simp
   | x :: xs, m + 1, 0 => by simp
   | x :: xs, 0, n + 1 => by simp [@eq_comm ℕ 0]
-  | x :: xs, m + 1, n + 1 => by simp [Nat.min_succ_succ, take_eq_take]
+  | x :: xs, m + 1, n + 1 => by simp [Nat.succ_min_succ, take_eq_take]
 #align list.take_eq_take List.take_eq_take
 
 theorem take_add (l : List α) (m n : ℕ) : l.take (m + n) = l.take m ++ (l.drop m).take n := by

Mathlib/Data/List/Func.lean

@@ -109,7 +109,7 @@ theorem length_set : ∀ {m : ℕ} {as : List α}, as {m ↦ a}.length = max as.
     have := @length_set m []
     simp [set, length, @length_set m, Nat.zero_max]
   | m + 1, _ :: as => by
-    simp [set, length, @length_set m, Nat.max_succ_succ]
+    simp [set, length, @length_set m, Nat.succ_max_succ]
 #align list.func.length_set List.Func.length_set
 
 -- porting note : @[simp] has been removed since `#lint` says this is
@@ -306,7 +306,7 @@ theorem length_pointwise {f : α → β → γ} :
   | _ :: as, [] => by
     simp only [pointwise, length, length_map, max_eq_left (Nat.zero_le (length as + 1))]
   | _ :: as, _ :: bs => by
-    simp only [pointwise, length, Nat.max_succ_succ, @length_pointwise _ as bs]
+    simp only [pointwise, length, Nat.succ_max_succ, @length_pointwise _ as bs]
 #align list.func.length_pointwise List.Func.length_pointwise
 
 end Func

Mathlib/Data/Nat/Basic.lean

@@ -192,13 +192,7 @@ theorem one_lt_succ_succ (n : ℕ) : 1 < n.succ.succ :=
 
 -- Porting note: Nat.succ_le_succ_iff is in Std
 
-theorem max_succ_succ {m n : ℕ} : max (succ m) (succ n) = succ (max m n) := by
-  by_cases h1 : m ≤ n
-  rw [max_eq_right h1, max_eq_right (succ_le_succ h1)]
-  · rw [not_le] at h1
-    have h2 := le_of_lt h1
-    rw [max_eq_left h2, max_eq_left (succ_le_succ h2)]
-#align nat.max_succ_succ Nat.max_succ_succ
+#align nat.max_succ_succ Nat.succ_max_succ
 
 theorem not_succ_lt_self {n : ℕ} : ¬succ n < n :=
   not_lt_of_ge (Nat.le_succ _)

Mathlib/Data/Nat/Order/Basic.lean

@@ -112,8 +112,6 @@ theorem eq_zero_of_mul_le (hb : 2 ≤ n) (h : n * m ≤ m) : m = 0 :=
   eq_zero_of_double_le <| le_trans (Nat.mul_le_mul_right _ hb) h
 #align nat.eq_zero_of_mul_le Nat.eq_zero_of_mul_le
 
-theorem zero_max : max 0 n = n :=
-  max_eq_right (zero_le _)
 #align nat.zero_max Nat.zero_max
 
 @[simp]

Mathlib/Data/Stream/Init.lean

@@ -591,7 +591,7 @@ theorem length_take (n : ℕ) (s : Stream' α) : (take n s).length = n := by
 theorem take_take {s : Stream' α} : ∀ {m n}, (s.take n).take m = s.take (min n m)
   | 0, n => by rw [min_zero, List.take_zero, take_zero]
   | m, 0 => by rw [zero_min, take_zero, List.take_nil]
-  | m+1, n+1 => by rw [take_succ, List.take_cons, Nat.min_succ_succ, take_succ, take_take]
+  | m+1, n+1 => by rw [take_succ, List.take_cons, Nat.succ_min_succ, take_succ, take_take]
 
 @[simp] theorem concat_take_get {s : Stream' α} : s.take n ++ [s.get n] = s.take (n+1) :=
   (take_succ' n).symm

Mathlib/Init/Data/List/Lemmas.lean

@@ -176,7 +176,7 @@ theorem length_mapAccumr₂ :
     calc
       succ (length (mapAccumr₂ f x y c).2) = succ (min (length x) (length y)) :=
         congr_arg succ (length_mapAccumr₂ f x y c)
-      _ = min (succ (length x)) (succ (length y)) := Eq.symm (min_succ_succ (length x) (length y))
+      _ = min (succ (length x)) (succ (length y)) := Eq.symm (succ_min_succ (length x) (length y))
   | _, _ :: _, [], _ => rfl
   | _, [], _ :: _, _ => rfl
   | _, [], [], _ => rfl

Mathlib/Init/Data/Nat/Lemmas.lean

@@ -470,7 +470,7 @@ Many lemmas are proven more generally in mathlib `algebra/order/sub` -/
 
 #align nat.min_zero Nat.min_zero
 
-#align nat.min_succ_succ Nat.min_succ_succ
+#align nat.succ_min_succ Nat.succ_min_succ
 
 #align nat.sub_eq_sub_min Nat.sub_eq_sub_min
 

Mathlib/Tactic/Backtrack.lean

@@ -43,19 +43,6 @@ def List.tryAllM [Monad m] [Alternative m] (L : List α) (f : α → m β) : m (
   return (R.filterMap (fun s => match s with | .inl a => a | _ => none),
     R.filterMap (fun s => match s with | .inr b => b | _ => none))
 
-namespace Lean.MVarId
-
-/--
-Given any tactic that takes a goal, and returns a sequence of alternative outcomes
-(each outcome consisting of a list of new subgoals),
-we can perform backtracking search by repeatedly applying the tactic.
--/
-def firstContinuation (results : MVarId → Nondet MetaM (List MVarId))
-    (cont : List MVarId → MetaM α) (g : MVarId) : MetaM α := do
-  (results g).firstM fun r => observing? do cont r
-
-end Lean.MVarId
-
 namespace Mathlib.Tactic
 
 /--
@@ -70,38 +57,39 @@ structure BacktrackConfig where
   /-- Maximum recursion depth. -/
   maxDepth : Nat := 6
   /-- An arbitrary procedure which can be used to modify the list of goals
-  before each attempt to apply a lemma.
+  before each attempt to generate alternatives.
   Called as `proc goals curr`, where `goals` are the original goals for `backtracking`,
   and `curr` are the current goals.
   Returning `some l` will replace the current goals with `l` and recurse
   (consuming one step of maximum depth).
-  Returning `none` will proceed to applying lemmas without changing goals.
+  Returning `none` will proceed to generating alternative without changing goals.
   Failure will cause backtracking.
   (defaults to `none`) -/
   proc : List MVarId → List MVarId → MetaM (Option (List MVarId)) := fun _ _ => pure none
-  /-- If `suspend g`, then we do not attempt to apply any further lemmas,
+  /-- If `suspend g`, then we do not consider alternatives for `g`,
   but return `g` as a new subgoal. (defaults to `false`) -/
   suspend : MVarId → MetaM Bool := fun _ => pure false
-  /-- `discharge g` is called on goals for which no lemmas apply.
+  /-- `discharge g` is called on goals for which there were no alternatives.
   If `none` we return `g` as a new subgoal.
   If `some l`, we replace `g` by `l` in the list of active goals, and recurse.
   If failure, we backtrack. (defaults to failure) -/
   discharge : MVarId → MetaM (Option (List MVarId)) := fun _ => failure
-  /-- If we solve any "independent" goals, don't fail. -/
+  /--
+  If we solve any "independent" goals, don't fail.
+  See `Lean.MVarId.independent?` for the definition of independence.
+  -/
   commitIndependentGoals : Bool := false
 
-def ppMVarIds (gs : List MVarId) : MetaM (List Format) := do
-  gs.mapM fun g => do ppExpr (← g.getType)
-
 /--
 Attempts to solve the `goals`, by recursively calling `alternatives g` on each subgoal that appears.
-`alternatives` returns a nondeterministic list of goals
-(this is essentially a lazy list of `List MVarId`,
-with the extra state required to backtrack in `MetaM`).
+`alternatives` returns a nondeterministic list of new subgoals generated from a goal.
 
 `backtrack` performs a backtracking search, attempting to close all subgoals.
 
 Further flow control options are available via the `Config` argument.
+
+Returns a list of subgoals which were "suspended" via the `suspend` or `discharge` hooks
+in `Config`. In the default configuration, `backtrack` will either return an empty list or fail.
 -/
 partial def backtrack (cfg : BacktrackConfig := {}) (trace : Name := .anonymous)
     (alternatives : MVarId → Nondet MetaM (List MVarId))
@@ -152,9 +140,9 @@ where
           run (n+1) gs (g :: acc)
         else
           try
-            -- We attempt to find an expression which can be applied,
-            -- and for which all resulting sub-goals can be discharged using `run n`.
-            g.firstContinuation alternatives (fun res => run n (res ++ gs) acc)
+            -- We attempt to find an alternative,
+            -- for which all resulting sub-goals can be discharged using `run n`.
+            (alternatives g).firstM fun r => observing? do run n (r ++ gs) acc
           catch _ =>
             -- No lemmas could be applied:
             match (← cfg.discharge g) with
@@ -164,8 +152,10 @@ where
             | some l => (withTraceNode trace
                 (fun _ => return m!"⏬ discharger generated new subgoals") do
               run n (l ++ gs) acc)
-  -- A wrapper around `run`, which works on "independent" goals separately first,
-  -- to reduce backtracking.
+  /--
+  A wrapper around `run`, which works on "independent" goals separately first,
+  to reduce backtracking.
+  -/
   processIndependentGoals (goals remaining : List MVarId) : MetaM (List MVarId) := do
     -- Partition the remaining goals into "independent" goals
     -- (which should be solvable without affecting the solvability of other goals)
@@ -193,11 +183,16 @@ where
         return newSubgoals ++ failed ++ (← (processIndependentGoals goals' ogs <|> pure ogs))
       else if !failed.isEmpty then
         -- If `commitIndependentGoals` is `false`, and we failed on any of the independent goals,
-        -- the overall failure is inevitable so we can stop here.
+        -- then overall failure is inevitable so we can stop here.
         failure
       else
         -- Finally, having solved this batch of independent goals,
         -- recurse (potentially now finding new independent goals).
         return newSubgoals ++ (← processIndependentGoals goals' ogs)
+  /--
+  Pretty print a list of goals.
+  -/
+  ppMVarIds (gs : List MVarId) : MetaM (List Format) := do
+    gs.mapM fun g => do ppExpr (← g.getType)
 
 end Mathlib.Tactic

lake-manifest.json

@@ -4,7 +4,7 @@
  [{"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "123e2f1e31355f79b95396b2d83de61bd9b485e7",
+    "rev": "b541ac2085f0970ef3d3a2d44daba50e34488aab",
     "opts": {},
     "name": "std",
     "inputRev?": "main",