Merge remote-tracking branch 'origin/main' into bump/v4.6.0

.github/workflows/nightly_detect_failure.yml

@@ -39,12 +39,19 @@ jobs:
         ref: nightly-testing # checkout nightly-testing branch
         fetch-depth: 0 # checkout all branches so that we can push from `nightly-testing` to `nightly-testing-YYYY-MM-DD`
         token: ${{ secrets.NIGHTLY_TESTING }}
-    - name: Update the nightly-testing-YYYY-MM-DD branch
+    - name: Update the nightly-testing-YYYY-MM-DD tag
       run: |
         toolchain=$(<lean-toolchain)
         if [[ $toolchain =~ leanprover/lean4:nightly-([a-zA-Z0-9_-]+) ]]; then
           version=${BASH_REMATCH[1]}
-          git push origin refs/heads/nightly-testing:refs/heads/nightly-testing-$version
+          if git ls-remote --tags --exit-code origin "refs/tags/nightly-testing-$version" >/dev/null; then
+              echo "Tag nightly-testing-$version already exists on the remote."
+          else
+              # If the tag does not exist, create and push the tag to remote
+              echo "Creating tag nightly-testing-$version from the current state of the nightly-testing branch."
+              git tag nightly-testing-$version
+              git push origin nightly-testing-$version
+          fi
         else
           echo "Error: The file lean-toolchain does not contain the expected pattern."
           exit 1

Std/Data/Array/Basic.lean

@@ -36,6 +36,18 @@ Sort an array using `compare` to compare elements.
 def qsortOrd [ord : Ord α] (xs : Array α) : Array α :=
   xs.qsort fun x y => compare x y |>.isLT
 
+set_option linter.unusedVariables.funArgs false in
+/--
+Returns the first minimal element among `d` and elements of the array.
+If `start` and `stop` are given, only the subarray `xs[start:stop]` is
+considered (in addition to `d`).
+-/
+@[inline]
+protected def minWith [ord : Ord α]
+    (xs : Array α) (d : α) (start := 0) (stop := xs.size) : α :=
+  xs.foldl (init := d) (start := start) (stop := stop) fun min x =>
+    if compare x min |>.isLT then x else min
+
 set_option linter.unusedVariables.funArgs false in
 /--
 Find the first minimal element of an array. If the array is empty, `d` is
@@ -45,8 +57,10 @@ considered.
 @[inline]
 protected def minD [ord : Ord α]
     (xs : Array α) (d : α) (start := 0) (stop := xs.size) : α :=
-  xs.foldl (init := d) (start := start) (stop := stop) fun min x =>
-    if compare x min |>.isLT then x else min
+  if h: start < xs.size ∧ start < stop then
+    xs.minWith (xs.get ⟨start, h.left⟩) (start + 1) stop
+  else
+    d
 
 set_option linter.unusedVariables.funArgs false in
 /--
@@ -57,8 +71,8 @@ considered.
 @[inline]
 protected def min? [ord : Ord α]
     (xs : Array α) (start := 0) (stop := xs.size) : Option α :=
-  if h : start < xs.size then
-    some $ xs.minD (xs.get ⟨start, h⟩) start stop
+  if h : start < xs.size ∧ start < stop then
+    some $ xs.minD (xs.get ⟨start, h.left⟩) start stop
   else
     none
 
@@ -73,6 +87,17 @@ protected def minI [ord : Ord α] [Inhabited α]
     (xs : Array α) (start := 0) (stop := xs.size) : α :=
   xs.minD default start stop
 
+set_option linter.unusedVariables.funArgs false in
+/--
+Returns the first maximal element among `d` and elements of the array.
+If `start` and `stop` are given, only the subarray `xs[start:stop]` is
+considered (in addition to `d`).
+-/
+@[inline]
+protected def maxWith [ord : Ord α]
+    (xs : Array α) (d : α) (start := 0) (stop := xs.size) : α :=
+  xs.minWith (ord := ord.opposite) d start stop
+
 set_option linter.unusedVariables.funArgs false in
 /--
 Find the first maximal element of an array. If the array is empty, `d` is

Std/Tactic/Basic.lean

@@ -19,7 +19,7 @@ namespace Std.Tactic
 open Lean Parser.Tactic Elab Command Elab.Tactic Meta
 
 /-- `exfalso` converts a goal `⊢ tgt` into `⊢ False` by applying `False.elim`. -/
-macro "exfalso" : tactic => `(tactic| apply False.elim)
+macro "exfalso" : tactic => `(tactic| refine False.elim ?_)
 
 /--
 `_` in tactic position acts like the `done` tactic: it fails and gives the list

test/exfalso.lean

@@ -0,0 +1,13 @@
+import Std.Tactic.Basic
+
+private axiom test_sorry : ∀ {α}, α
+
+example {A} (h : False) : A := by
+  exfalso
+  exact h
+
+example {A} : False → A := by
+  exfalso
+  show False -- exfalso is not supposed to close the goal yet
+  exact test_sorry
+