Merge branch 'main' into bitneg

.gitignore

@@ -5,8 +5,3 @@
 /lakefile.olean
 # After v4.3.0-rc2 lake stores its files here:
 /.lake/
-# Note: because std has no dependencies, the lake-manifest contains no information
-# that is not regenerated automatically by lake, so this avoids conflicts when
-# lake decides to upgrade its manifest version.
-# We may revisit this if lake decides to store more useful information in the manifest.
-lake-manifest.json

GNUmakefile

@@ -10,10 +10,13 @@ all: build test
 build:
 	lake build
 
-test: $(addsuffix .run, $(TESTS))
+# Find all .lean files in test and subdirectories, replace .lean with .run
+TESTS := $(shell find test -type f -name '*.lean' | sed 's/\.lean$$/.run/')
 
-test/%.run: build
-	lake env lean test/$*
+test: $(TESTS)
+
+%.run: build
+	lake env lean $(@:.run=.lean)
 
 lint: build
 	./.lake/build/bin/runLinter

README.md

@@ -68,3 +68,7 @@ One of the easiest ways to contribute is to find a missing proof and complete it
 [`proof_wanted`](https://github.com/search?q=repo%3Aleanprover%2Fstd4+proof_wanted+language%3ALean&type=code&l=Lean)
 declaration documents statements that have been identified as being useful, but that have not yet
 been proven.
+
+In contrast to mathlib, `std` uses pull requests from forks of this repository. Hence, no special permissions on this repository are required for new contributors.
+
+You can change the labels on PRs by commenting one of `awaiting-review`, `awaiting-author`, or `WIP`. This is helpful for triage.

Std.lean

@@ -75,6 +75,7 @@ import Std.Lean.PersistentHashMap
 import Std.Lean.PersistentHashSet
 import Std.Lean.Position
 import Std.Lean.SMap
+import Std.Lean.Syntax
 import Std.Lean.System.IO
 import Std.Lean.Tactic
 import Std.Lean.TagAttribute
@@ -89,6 +90,7 @@ import Std.Tactic.Basic
 import Std.Tactic.ByCases
 import Std.Tactic.Case
 import Std.Tactic.Change
+import Std.Tactic.Classical
 import Std.Tactic.CoeExt
 import Std.Tactic.Congr
 import Std.Tactic.Exact
@@ -98,6 +100,7 @@ import Std.Tactic.FalseOrByContra
 import Std.Tactic.GuardExpr
 import Std.Tactic.GuardMsgs
 import Std.Tactic.HaveI
+import Std.Tactic.Init
 import Std.Tactic.Instances
 import Std.Tactic.LabelAttr
 import Std.Tactic.LeftRight
@@ -145,6 +148,7 @@ import Std.Tactic.Unreachable
 import Std.Tactic.Where
 import Std.Test.Internal.DummyLabelAttr
 import Std.Util.Cache
+import Std.Util.CheckTactic
 import Std.Util.ExtendedBinder
 import Std.Util.LibraryNote
 import Std.Util.Pickle

Std/CodeAction/Basic.lean

@@ -147,7 +147,7 @@ partial def findInfoTree? (kind : SyntaxNodeKind) (tgtRange : String.Range)
   (f : ContextInfo → Info → Bool) (canonicalOnly := false) :
     Option (ContextInfo × InfoTree) :=
   match t with
-  | .context ctx t => findInfoTree? kind tgtRange ctx t f canonicalOnly
+  | .context ctx t => findInfoTree? kind tgtRange (ctx.mergeIntoOuter? ctx?) t f canonicalOnly
   | node@(.node i ts) => do
     if let some ctx := ctx? then
       if let some range := i.stx.getRange? canonicalOnly then

Std/CodeAction/Misc.lean

@@ -38,32 +38,42 @@ In the following:
 instance : Monad Id := _
 ```
 
-invoking the hole code action "Generate a skeleton for the structure under construction." produces:
+invoking the hole code action "Generate a (minimal) skeleton for the structure under construction."
+produces:
 ```lean
-instance : Monad Id := {
+instance : Monad Id where
+  pure := _
+  bind := _
+```
+
+and invoking "Generate a (maximal) skeleton for the structure under construction." produces:
+```lean
+instance : Monad Id where
   map := _
   mapConst := _
   pure := _
   seq := _
   seqLeft := _
   seqRight := _
   bind := _
-}
 ```
 -/
-@[hole_code_action] partial def instanceStub : HoleCodeAction := fun params snap ctx info => do
+@[hole_code_action] partial def instanceStub : HoleCodeAction := fun _ snap ctx info => do
   let some ty := info.expectedType? | return #[]
   let .const name _ := (← info.runMetaM ctx (whnf ty)).getAppFn | return #[]
   unless isStructure snap.env name do return #[]
-  let eager := {
-    title := "Generate a skeleton for the structure under construction."
-    kind? := "quickfix"
-    isPreferred? := true
-  }
   let doc ← readDoc
-  pure #[{
-    eager
-    lazy? := some do
+  let fields := collectFields snap.env name #[] []
+  let only := !fields.any fun (_, auto) => auto
+  let mkAutofix minimal :=
+    let eager := {
+      title := s!"\
+        Generate a {if only then "" else if minimal then "(minimal) " else "(maximal) "}\
+        skeleton for the structure under construction."
+      kind? := "quickfix"
+      isPreferred? := minimal
+    }
+    let lazy? := some do
       let useWhere := do
         let _ :: (stx, _) :: _ ← findStack? snap.stx info.stx | none
         guard (stx.getKind == ``Parser.Command.declValSimple)
@@ -73,7 +83,8 @@ instance : Monad Id := {
       let indent := "\n".pushn ' ' indent
       let mut str := if useWhere.isSome then "where" else "{"
       let mut first := useWhere.isNone && isStart
-      for field in collectFields snap.env name #[] do
+      for (field, auto) in fields do
+        if minimal && auto then continue
         if first then
           str := str ++ " "
           first := false
@@ -92,14 +103,25 @@ instance : Monad Id := {
           newText := str
         }
       }
-  }]
+    { eager, lazy? }
+  pure <| if only then #[mkAutofix true] else #[mkAutofix true, mkAutofix false]
 where
+  /-- Returns true if this field is an autoParam or optParam, or if it is given an optional value
+  in a child struct. -/
+  isAutofillable (env : Environment) (fieldInfo : StructureFieldInfo) (stack : List Name) : Bool :=
+    fieldInfo.autoParam?.isSome || env.contains (mkDefaultFnOfProjFn fieldInfo.projFn)
+      || stack.any fun struct => env.contains (mkDefaultFnOfProjFn (struct ++ fieldInfo.fieldName))
+
   /-- Returns the fields of a structure, unfolding parent structures. -/
-  collectFields (env : Environment) (structName : Name) (fields : Array Name) : Array Name :=
+  collectFields (env : Environment) (structName : Name)
+      (fields : Array (Name × Bool)) (stack : List Name) : Array (Name × Bool) :=
     (getStructureFields env structName).foldl (init := fields) fun fields field =>
-      match isSubobjectField? env structName field with
-      | some substructName => collectFields env substructName fields
-      | none => fields.push field
+      if let some fieldInfo := getFieldInfo? env structName field then
+        if let some substructName := fieldInfo.subobject? then
+          collectFields env substructName fields (structName :: stack)
+        else
+          fields.push (field, isAutofillable env fieldInfo stack)
+      else fields
 
 /-- Returns the explicit arguments given a type. -/
 def getExplicitArgs : Expr → Array Name → Array Name

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/Data/Array/Init/Basic.lean

@@ -29,7 +29,7 @@ def ofFn {n} (f : Fin n → α) : Array α := go 0 (mkEmpty n) where
   /-- Auxiliary for `ofFn`. `ofFn.go f i acc = acc ++ #[f i, ..., f(n - 1)]` -/
   go (i : Nat) (acc : Array α) : Array α :=
     if h : i < n then go (i+1) (acc.push (f ⟨i, h⟩)) else acc
-termination_by _ => n - i
+termination_by n - i
 
 /-- The array `#[0, 1, ..., n - 1]`. -/
 def range (n : Nat) : Array Nat :=

Std/Data/Array/Init/Lemmas.lean

@@ -5,6 +5,7 @@ Authors: Mario Carneiro
 -/
 import Std.Tactic.NoMatch
 import Std.Tactic.HaveI
+import Std.Tactic.ByCases
 import Std.Classes.LawfulMonad
 import Std.Data.Fin.Init.Lemmas
 import Std.Data.Nat.Init.Lemmas
@@ -152,7 +153,7 @@ where
     · rw [← List.get_drop_eq_drop _ i ‹_›]
       simp [aux (i+1), map_eq_pure_bind]; rfl
     · rw [List.drop_length_le (Nat.ge_of_not_lt ‹_›)]; rfl
-termination_by aux => arr.size - i
+  termination_by arr.size - i
 
 theorem SatisfiesM_mapM [Monad m] [LawfulMonad m] (as : Array α) (f : α → m β)
     (motive : Nat → Prop) (h0 : motive 0)
@@ -262,9 +263,9 @@ theorem SatisfiesM_anyM [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Arra
         | true, h => .pure h
         | false, h => go hj hstop h hp
     · next hj => exact .pure <| Nat.le_antisymm hj' (Nat.ge_of_not_lt hj) ▸ h0
+    termination_by stop - j
   simp only [Array.anyM_eq_anyM_loop]
   exact go hstart _ h0 fun i hi => hp i <| Nat.lt_of_lt_of_le hi <| Nat.min_le_left ..
-termination_by go => stop - j
 
 theorem SatisfiesM_anyM_iff_exists [Monad m] [LawfulMonad m]
     (p : α → m Bool) (as : Array α) (start stop) (q : Fin as.size → Prop)

Std/Data/Array/Lemmas.lean

@@ -7,6 +7,7 @@ Authors: Mario Carneiro, Gabriel Ebner
 import Std.Data.Nat.Lemmas
 import Std.Data.List.Lemmas
 import Std.Data.Array.Basic
+import Std.Tactic.SeqFocus
 import Std.Tactic.HaveI
 import Std.Tactic.Simpa
 import Std.Util.ProofWanted
@@ -41,10 +42,26 @@ attribute [simp] isEmpty uget
 
 @[simp] theorem data_length {l : Array α} : l.data.length = l.size := rfl
 
+/-- # mem -/
+
 theorem mem_data {a : α} {l : Array α} : a ∈ l.data ↔ a ∈ l := (mem_def _ _).symm
 
 theorem not_mem_nil (a : α) : ¬ a ∈ #[] := fun.
 
+/-- # set -/
+
+@[simp] theorem set!_is_setD : @set! = @setD := rfl
+
+@[simp] theorem size_setD (a : Array α) (index : Nat) (val : α) :
+  (Array.setD a index val).size = a.size := by
+  if h : index < a.size  then
+    simp [setD, h]
+  else
+    simp [setD, h]
+
+
+/-- # get lemmas -/
+
 theorem getElem?_mem {l : Array α} {i : Fin l.size} : l[i] ∈ l := by
   erw [Array.mem_def, getElem_eq_data_get]
   apply List.get_mem
@@ -131,6 +148,22 @@ theorem get_set (a : Array α) (i : Fin a.size) (j : Nat) (hj : j < a.size) (v :
     (a.set i v)[j]'(by simp [*]) = if i = j then v else a[j] := by
   if h : i.1 = j then subst j; simp [*] else simp [*]
 
+@[simp] theorem getElem_setD (a : Array α) (i : Nat) (v : α) (h : i < (setD a i v).size) :
+  (setD a i v)[i]'h = v := by
+  simp at h
+  simp only [setD, h, dite_true, get_set, ite_true]
+
+/--
+This lemma simplifies a normal form from `get!`
+-/
+@[simp] theorem getD_get?_setD (a : Array α) (i : Nat) (v d : α) :
+  Option.getD (setD a i v)[i]? d = if i < a.size then v else d := by
+  if h : i < a.size then
+    simp [setD, h, getElem?, get_set]
+  else
+    have p : i ≥ a.size := Nat.le_of_not_gt h
+    simp [setD, h, get?_len_le, p]
+
 theorem set_set (a : Array α) (i : Fin a.size) (v v' : α) :
     (a.set i v).set ⟨i, by simp [i.2]⟩ v' = a.set i v' := by simp [set, List.set_set]
 
@@ -266,8 +299,8 @@ theorem mapIdx_induction' (as : Array α) (f : Fin as.size → α → β)
 
 theorem size_eq_length_data (as : Array α) : as.size = as.data.length := rfl
 
-@[simp] theorem size_swap! (a : Array α) (i j) (hi : i < a.size) (hj : j < a.size) :
-    (a.swap! i j).size = a.size := by simp [swap!, hi, hj]
+@[simp] theorem size_swap! (a : Array α) (i j) :
+    (a.swap! i j).size = a.size := by unfold swap!; split <;> (try split) <;> simp [size_swap]
 
 @[simp] theorem size_reverse (a : Array α) : a.reverse.size = a.size := by
   let rec go (as : Array α) (i j) : (reverse.loop as i j).size = as.size := by
@@ -276,8 +309,8 @@ theorem size_eq_length_data (as : Array α) : as.size = as.data.length := rfl
       have := reverse.termination h
       simp [(go · (i+1) ⟨j-1, ·⟩), h]
     else simp [h]
+    termination_by j - i
   simp only [reverse]; split <;> simp [go]
-termination_by _ => j - i
 
 @[simp] theorem size_range {n : Nat} : (range n).size = n := by
   unfold range
@@ -323,14 +356,14 @@ theorem size_modifyM [Monad m] [LawfulMonad m] (a : Array α) (i : Nat) (f : α
         cases Nat.le_antisymm h₂.1 h₂.2
         exact (List.get?_reverse' _ _ h).symm
       · rfl
+    termination_by j - i
   simp only [reverse]; split
   · match a with | ⟨[]⟩ | ⟨[_]⟩ => rfl
   · have := Nat.sub_add_cancel (Nat.le_of_not_le ‹_›)
     refine List.ext <| go _ _ _ _ (by simp [this]) rfl fun k => ?_
     split; {rfl}; rename_i h
     simp [← show k < _ + 1 ↔ _ from Nat.lt_succ (n := a.size - 1), this] at h
     rw [List.get?_eq_none.2 ‹_›, List.get?_eq_none.2 (a.data.length_reverse ▸ ‹_›)]
-termination_by _ => j - i
 
 @[simp] theorem size_ofFn_go {n} (f : Fin n → α) (i acc) :
     (ofFn.go f i acc).size = acc.size + (n - i) := by
@@ -343,7 +376,7 @@ termination_by _ => j - i
     have : n - i = 0 := Nat.sub_eq_zero_of_le (Nat.le_of_not_lt hin)
     unfold ofFn.go
     simp [hin, this]
-termination_by _ => n - i
+termination_by n - i
 
 @[simp] theorem size_ofFn (f : Fin n → α) : (ofFn f).size = n := by simp [ofFn]
 
@@ -363,7 +396,7 @@ theorem getElem_ofFn_go (f : Fin n → α) (i) {acc k}
     | inr hj => simp [get_push, *]
   else
     simp [hin, hacc k (Nat.lt_of_lt_of_le hki (Nat.le_of_not_lt (hi ▸ hin)))]
-termination_by _ => n - i
+termination_by n - i
 
 @[simp] theorem getElem_ofFn (f : Fin n → α) (i : Nat) (h) :
     (ofFn f)[i] = f ⟨i, size_ofFn f ▸ h⟩ :=
@@ -427,8 +460,8 @@ theorem zipWith_eq_zipWith_data (f : α → β → γ) (as : Array α) (bs : Arr
         ((List.get bs.data i_bs) :: List.drop (i_bs + 1) bs.data) =
         List.zipWith f (List.drop i as.data) (List.drop i bs.data)
       simp only [List.get_cons_drop]
+    termination_by as.size - i
   simp [zipWith, loop 0 #[] (by simp) (by simp)]
-termination_by loop i _ _ _ => as.size - i
 
 theorem size_zipWith (as : Array α) (bs : Array β) (f : α → β → γ) :
     (as.zipWith bs f).size = min as.size bs.size := by