chore: merge main

Author: fgdorais

Batteries/Data/Fin/Lemmas.lean

@@ -37,7 +37,23 @@ protected theorem le_antisymm {x y : Fin n} (h1 : x ≤ y) (h2 : y ≤ x) : x =
 theorem list_succ (n) : list (n+1) = 0 :: (list n).map Fin.succ := by
   apply List.ext_get; simp; intro i; cases i <;> simp
 
-/-! ### foldlM -/
+theorem list_succ_last (n) : list (n+1) = (list n).map castSucc ++ [last n] := by
+  rw [list_succ]
+  induction n with
+  | zero => rfl
+  | succ n ih =>
+    rw [list_succ, List.map_cons castSucc, ih]
+    simp [Function.comp_def, succ_castSucc]
+
+theorem list_reverse (n) : (list n).reverse = (list n).map rev := by
+  induction n with
+  | zero => rfl
+  | succ n ih =>
+    conv => lhs; rw [list_succ_last]
+    conv => rhs; rw [list_succ]
+    simp [List.reverse_map, ih, Function.comp_def, rev_succ]
+
+/-! ### foldl -/
 
 theorem foldlM_loop_lt [Monad m] (f : α → Fin n → m α) (x) (h : i < n) :
     foldlM.loop n f x i = f x ⟨i, h⟩ >>= (foldlM.loop n f . (i+1)) := by
@@ -75,14 +91,22 @@ theorem foldlM_eq_foldlM_list [Monad m] (f : α → Fin n → m α) (x) :
 
 theorem foldl_eq_foldlM : foldl n f init = foldlM (m:=Id) n f init := rfl
 
-theorem foldl_zero (f : α → Fin 0 → α) (x) : foldl 0 f x = x := rfl
+@[simp] theorem foldl_zero (f : α → Fin 0 → α) (x) : foldl 0 f x = x := rfl
 
 theorem foldl_succ (f : α → Fin (n+1) → α) (x) :
     foldl (n+1) f x = foldl n (fun x j => f x j.succ) (f x 0) := foldlM_succ ..
 
-theorem foldl_eq_foldl_list (f : α → Fin n → α) (x) :
-    foldl n f x = (list n).foldl f x :=
-  by simp only [foldl_eq_foldlM, foldlM_eq_foldlM_list, List.foldl_eq_foldlM]
+theorem foldl_succ_last (f : α → Fin (n+1) → α) (x) :
+    foldl (n+1) f x = f (foldl n (f · ·.castSucc) x) (last n) := by
+  rw [foldl_succ]
+  induction n generalizing x with
+  | zero => rfl
+  | succ n ih => rw [foldl_succ, ih (f · ·.succ), foldl_succ]; simp [succ_castSucc]
+
+theorem foldl_eq_foldl_list (f : α → Fin n → α) (x) : foldl n f x = (list n).foldl f x := by
+  induction n generalizing x with
+  | zero => rfl
+  | succ n ih => rw [foldl_succ, ih, list_succ, List.foldl_cons, List.foldl_map]
 
 /-! ### foldrM -/
 
@@ -104,24 +128,33 @@ theorem foldrM_loop [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) (x
     rw [foldrM_loop_succ, foldrM_loop_succ, bind_assoc]
     congr; funext; exact ih ..
 
-theorem foldrM_zero [Monad m] (f : Fin 0 → α → m α) (x) : foldrM 0 f x = pure x := rfl
+@[simp] theorem foldr_zero (f : Fin 0 → α → α) (x) : foldr 0 f x = x := rfl
 
-theorem foldrM_succ [Monad m] [LawfulMonad m] (f : Fin (n+1) → α → m α) (x) :
-    foldrM (n+1) f x = foldrM n (fun i => f i.succ) x >>= f 0 := foldrM_loop ..
+theorem foldr_succ (f : Fin (n+1) → α → α) (x) :
+    foldr (n+1) f x = f 0 (foldr n (fun i => f i.succ) x) := foldr_loop ..
 
-theorem foldrM_eq_foldrM_list [Monad m] [LawfulMonad m] (f : Fin n → α → m α) (x) :
-    foldrM n f x = (list n).foldrM f x := by
-  induction n with
+theorem foldr_succ_last (f : Fin (n+1) → α → α) (x) :
+    foldr (n+1) f x = foldr n (f ·.castSucc) (f (last n) x) := by
+  rw [foldr_succ]
+  induction n generalizing x with
   | zero => rfl
-  | succ n ih => rw [foldrM_succ, ih, list_succ, List.foldrM_cons, List.foldrM_map]
+  | succ n ih => rw [foldr_succ, ih (f ·.succ), foldr_succ]; simp [succ_castSucc]
 
-theorem foldr_eq_foldrM (f : Fin n → α → α) (init) : foldr n f init = foldrM (m:=Id) n f init := rfl
+theorem foldr_eq_foldr_list (f : Fin n → α → α) (x) : foldr n f x = (list n).foldr f x := by
+  induction n with
+  | zero => rfl
+  | succ n ih => rw [foldr_succ, ih, list_succ, List.foldr_cons, List.foldr_map]
 
-theorem foldr_zero (f : Fin 0 → α → α) (x) : foldr 0 f x = x := rfl
+/-! ### foldl/foldr -/
 
-theorem foldr_succ (f : Fin (n+1) → α → α) (x) :
-    foldr (n+1) f x = f 0 (foldr n (fun i => f i.succ) x) := foldrM_loop ..
+theorem foldl_rev (f : Fin n → α → α) (x) :
+    foldl n (fun x i => f i.rev x) x = foldr n f x := by
+  induction n generalizing x with
+  | zero => rfl
+  | succ n ih => rw [foldl_succ, foldr_succ_last, ← ih]; simp [rev_succ]
 
-theorem foldr_eq_foldr_list (f : Fin n → α → α) (x) :
-    foldr n f x = (list n).foldr f x := by
-  simp only [foldr_eq_foldrM, foldrM_eq_foldrM_list, List.foldr_eq_foldrM]
+theorem foldr_rev (f : α → Fin n → α) (x) :
+     foldr n (fun i x => f x i.rev) x = foldl n f x := by
+  induction n generalizing x with
+  | zero => rfl
+  | succ n ih => rw [foldl_succ_last, foldr_succ, ← ih]; simp [rev_succ]

Batteries/Data/String.lean

@@ -1,2 +1,3 @@
 import Batteries.Data.String.Basic
 import Batteries.Data.String.Lemmas
+import Batteries.Data.String.Matcher

Batteries/Data/String/Basic.lean

@@ -3,7 +3,6 @@ Copyright (c) 2022 Jannis Limperg. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jannis Limperg, James Gallicchio, F. G. Dorais
 -/
-import Batteries.Data.Array.Match
 
 instance : Coe String Substring := ⟨String.toSubstring⟩
 
@@ -12,63 +11,6 @@ namespace String
 protected theorem Pos.ne_zero_of_lt : {a b : Pos} → a < b → b ≠ 0
   | _, _, hlt, rfl => Nat.not_lt_zero _ hlt
 
-/-- Knuth-Morris-Pratt matcher type
-
-This type is used to keep data for running the Knuth-Morris-Pratt (KMP) string matching algorithm.
-KMP is a linear time algorithm to locate all substrings of a string that match a given pattern.
-Generating the algorithm data is also linear in the length of the pattern but the data can be
-re-used to match the same pattern over different strings.
-
-The KMP data for a pattern string can be generated using `Matcher.ofString`. Then `Matcher.find?`
-and `Matcher.findAll` can be used to run the algorithm on an input string.
-```
-def m := Matcher.ofString "abba"
-
-#eval Option.isSome <| m.find? "AbbabbA" -- false
-#eval Option.isSome <| m.find? "aabbaa" -- true
-
-#eval Array.size <| m.findAll "abbabba" -- 2
-#eval Array.size <| m.findAll "abbabbabba" -- 3
-```
--/
-structure Matcher extends Array.Matcher Char where
-  /-- The pattern for the matcher -/
-  pattern : Substring
-
-/-- Make KMP matcher from pattern substring -/
-@[inline] def Matcher.ofSubstring (pattern : Substring) : Matcher where
-  toMatcher := Array.Matcher.ofStream pattern
-  pattern := pattern
-
-/-- Make KMP matcher from pattern string -/
-@[inline] def Matcher.ofString (pattern : String) : Matcher :=
-  Matcher.ofSubstring pattern
-
-/-- The byte size of the string pattern for the matcher -/
-abbrev Matcher.patternSize (m : Matcher) : Nat := m.pattern.bsize
-
-/-- Find all substrings of `s` matching `m.pattern`. -/
-partial def Matcher.findAll (m : Matcher) (s : Substring) : Array Substring :=
-  loop s m.toMatcher #[]
-where
-  /-- Accumulator loop for `String.Matcher.findAll` -/
-  loop (s : Substring) (am : Array.Matcher Char) (occs : Array Substring) : Array Substring :=
-    match am.next? s with
-    | none => occs
-    | some (s, am) =>
-      loop s am <| occs.push { s with
-        startPos := ⟨s.startPos.byteIdx - m.patternSize⟩
-        stopPos := s.startPos }
-
-/-- Find the first substring of `s` matching `m.pattern`, or `none` if no such substring exists. -/
-def Matcher.find? (m : Matcher) (s : Substring) : Option Substring :=
-  match m.next? s with
-  | none => none
-  | some (s, _) =>
-    some { s with
-      startPos := ⟨s.startPos.byteIdx - m.patternSize⟩
-      stopPos := s.startPos }
-
 end String
 
 namespace Substring
@@ -133,41 +75,10 @@ def dropSuffix? (s : Substring) (suff : Substring) : Option Substring :=
   else
     none
 
-/--
-Returns all the substrings of `s` that match `pattern`.
--/
-@[inline] def findAllSubstr (s pattern : Substring) : Array Substring :=
-  (String.Matcher.ofSubstring pattern).findAll s
-
-/--
-Returns the first substring of `s` that matches `pattern`,
-or `none` if there is no such substring.
--/
-@[inline] def findSubstr? (s pattern : Substring) : Option Substring :=
-  (String.Matcher.ofSubstring pattern).find? s
-
-/--
-Returns true iff `pattern` occurs as a substring of `s`.
--/
-@[inline] def containsSubstr (s pattern : Substring) : Bool :=
-  s.findSubstr? pattern |>.isSome
-
 end Substring
 
 namespace String
 
-@[inherit_doc Substring.findAllSubstr]
-abbrev findAllSubstr (s : String) (pattern : Substring) : Array Substring :=
-  (String.Matcher.ofSubstring pattern).findAll s
-
-@[inherit_doc Substring.findSubstr?]
-abbrev findSubstr? (s : String) (pattern : Substring) : Option Substring :=
-  s.toSubstring.findSubstr? pattern
-
-@[inherit_doc Substring.containsSubstr]
-abbrev containsSubstr (s : String) (pattern : Substring) : Bool :=
-  s.toSubstring.containsSubstr pattern
-
 /--
 If `pre` is a prefix of `s`, i.e. `s = pre ++ t`, returns the remainder `t`.
 -/

Batteries/Lean/Name.lean

@@ -16,8 +16,13 @@ Generally, user code should not explicitly use internal names.
 def isInternalDetail : Name → Bool
   | .str p s     =>
     s.startsWith "_"
-      || s.startsWith "match_"
-      || s.startsWith "proof_"
+      || matchPrefix s "eq_"
+      || matchPrefix s "match_"
+      || matchPrefix s "proof_"
       || p.isInternalOrNum
   | .num _ _     => true
   | p            => p.isInternalOrNum
+where
+  /-- Check that a string begins with the given prefix, and then is only digit characters. -/
+  matchPrefix (s : String) (pre : String) :=
+    s.startsWith pre && (s |>.drop pre.length |>.all Char.isDigit)

Batteries/Util/Cache.lean

@@ -132,7 +132,7 @@ the second will store declarations from imports (and will hopefully be "read-onl
 -/
 @[reducible] def DiscrTreeCache (α : Type) : Type := DeclCache (DiscrTree α × DiscrTree α)
 
-/-- Discrimation tree settings for the `DiscrTreeCache`. -/
+/-- Discrimination tree settings for the `DiscrTreeCache`. -/
 def DiscrTreeCache.config : WhnfCoreConfig := {}
 
 /--

Batteries/Util/CheckTactic.lean

@@ -9,7 +9,7 @@ import Lean.Elab.Term
 /-
 This file is the home for commands to tactics behave as expected.
 
-It currently includes two tactixs:
+It currently includes two tactics:
 
 #check_tactic t ~> res
 

Batteries/Util/ExtendedBinder.lean

@@ -52,22 +52,3 @@ macro_rules -- TODO: merging the two macro_rules breaks expansion
   | `(∀ᵉ _ : $ty:term, $b) => `(∀ _ : $ty:term, $b)
   | `(∀ᵉ $x:ident : $ty:term, $b) => `(∀ $x:ident : $ty:term, $b)
   | `(∀ᵉ $x:binderIdent $p:binderPred, $b) => `(∀ $x:binderIdent $p:binderPred, $b)
-
-open Parser.Command in
-/--
-Declares a binder predicate.  For example:
-```
-binder_predicate x " > " y:term => `($x > $y)
-```
--/
-syntax (name := binderPredicate) (docComment)? (Parser.Term.attributes)? (attrKind)?
-  "binder_predicate" optNamedName optNamedPrio ppSpace ident (ppSpace macroArg)* " => "
-    term : command
-
-open Linter.MissingDocs Parser Term in
-/-- Missing docs handler for `binder_predicate` -/
-@[missing_docs_handler binderPredicate]
-def checkBinderPredicate : SimpleHandler := fun stx => do
-  if stx[0].isNone && stx[2][0][0].getKind != ``«local» then
-    if stx[4].isNone then lint stx[3] "binder predicate"
-    else lintNamed stx[4][0][3] "binder predicate"

Batteries/WF.lean

@@ -91,7 +91,7 @@ end Acc
 namespace WellFounded
 
 /-- Attaches to `x` the proof that `x` is accessible in the given well-founded relation.
-This can be used in recursive function definitions to explicitly use a differerent relation
+This can be used in recursive function definitions to explicitly use a different relation
 than the one inferred by default:
 
 ```

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.8.0-rc2
+leanprover/lean4:v4.8.0

scripts/test.lean

@@ -36,16 +36,20 @@ def main (args : List String) : IO Unit := do
           args := #["env", "lean", t.toString],
           env := #[("LEAN_ABORT_ON_PANIC", "1")] }
       let mut exitCode := out.exitCode
+      let stdout := out.stdout
+      let stderr := "\n".intercalate <|
+        -- We don't count manifest out of date warnings as noise.
+        out.stderr.splitOn "\n" |>.filter (!·.startsWith "warning: manifest out of date: ")
       if exitCode = 0 then
-        if out.stdout.isEmpty && out.stderr.isEmpty then
+        if stdout.isEmpty && stderr.isEmpty then
           IO.println s!"Test succeeded: {t}"
         else
           IO.println s!"Test succeeded with noisy output: {t}"
           unless allowNoisy do exitCode := 1
       else
         IO.eprintln s!"Test failed: `lake env lean {t}` produced:"
-      unless out.stdout.isEmpty do IO.eprintln out.stdout
-      unless out.stderr.isEmpty do IO.eprintln out.stderr
+      unless stdout.isEmpty do IO.eprintln stdout
+      unless out.stderr.isEmpty do IO.eprintln out.stderr -- We still print the manifest warning.
       pure exitCode
   -- Wait on all the jobs and exit with 1 if any failed.
   let mut exitCode : UInt8 := 0

test/kmp_matcher.lean

@@ -1,4 +1,4 @@
-import Batteries.Data.String.Basic
+import Batteries.Data.String.Matcher
 
 /-! Tests for Knuth-Morris-Pratt matching algorithm -/