Merge branch 'master' into jiedong_jiang_neg_split

Archive/Imo/Imo2019Q4.lean

@@ -5,7 +5,7 @@ Authors: Floris van Doorn
 -/
 import Mathlib.Data.Nat.Factorial.BigOperators
 import Mathlib.Data.Nat.Multiplicity
-import Mathlib.Data.Nat.Prime.Basic
+import Mathlib.Data.Nat.Prime.Int
 import Mathlib.Tactic.IntervalCases
 import Mathlib.Tactic.GCongr
 

Archive/Wiedijk100Theorems/BuffonsNeedle.lean

@@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Enrico Z. Borba
 -/
 
-import Mathlib.Probability.Density
-import Mathlib.Probability.Notation
-import Mathlib.MeasureTheory.Constructions.Prod.Integral
 import Mathlib.Analysis.SpecialFunctions.Integrals
+import Mathlib.MeasureTheory.Integral.Prod
+import Mathlib.Probability.Density
 import Mathlib.Probability.Distributions.Uniform
+import Mathlib.Probability.Notation
 
 /-!
 

Archive/Wiedijk100Theorems/InverseTriangleSum.lean

@@ -27,8 +27,8 @@ open Finset
 /-- **Sum of the Reciprocals of the Triangular Numbers** -/
 theorem Theorems100.inverse_triangle_sum :
     ∀ n, ∑ k ∈ range n, (2 : ℚ) / (k * (k + 1)) = if n = 0 then 0 else 2 - (2 : ℚ) / n := by
-  refine sum_range_induction _ _ (if_pos rfl) ?_
-  rintro (_ | n)
-  · rw [if_neg, if_pos] <;> norm_num
+  refine sum_range_induction _ _ rfl ?_
+  rintro (_ | _)
+  · norm_num
   field_simp
   ring

Counterexamples/CharPZeroNeCharZero.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Damiano Testa. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Damiano Testa, Eric Wieser
 -/
-import Mathlib.Algebra.CharP.Basic
+import Mathlib.Algebra.CharP.Lemmas
 import Mathlib.Algebra.PUnitInstances.Algebra
 
 /-! # `CharP R 0` and `CharZero R` need not coincide for semirings

Counterexamples/ZeroDivisorsInAddMonoidAlgebras.lean

@@ -28,8 +28,8 @@ nontrivial ring `R` and the additive group `G` with a torsion element can be any
 Besides this example, we also address a comment in `Data.Finsupp.Lex` to the effect that the proof
 that addition is monotone on `α →₀ N` uses that it is *strictly* monotone on `N`.
 
-The specific statement is about `Finsupp.Lex.covariantClass_lt_left` and its analogue
-`Finsupp.Lex.covariantClass_le_right`.  We do not need two separate counterexamples, since the
+The specific statement is about `Finsupp.Lex.addLeftStrictMono` and its analogue
+`Finsupp.Lex.addRightStrictMono`.  We do not need two separate counterexamples, since the
 operation is commutative.
 
 The example is very simple.  Let `F = {0, 1}` with order determined by `0 < 1` and absorbing
@@ -142,9 +142,9 @@ elab "guard_decl" na:ident mod:ident : command => do
   let .some mdni := env.getModuleIdx? mdn | throwError "the module {mod} is not imported!"
   unless dcli = mdni do throwError "instance {na} is no longer in {mod}."
 
-guard_decl Finsupp.Lex.covariantClass_le_left Mathlib.Data.Finsupp.Lex
+guard_decl Finsupp.Lex.addLeftMono Mathlib.Data.Finsupp.Lex
 
-guard_decl Finsupp.Lex.covariantClass_le_right Mathlib.Data.Finsupp.Lex
+guard_decl Finsupp.Lex.addRightMono Mathlib.Data.Finsupp.Lex
 
 namespace F
 
@@ -182,20 +182,20 @@ instance : AddCommMonoid F where
   add_comm := by boom
   nsmul := nsmulRec
 
-/-- The `CovariantClass`es asserting monotonicity of addition hold for `F`. -/
-instance covariantClass_add_le : CovariantClass F F (· + ·) (· ≤ ·) :=
+/-- The `AddLeftMono`es asserting monotonicity of addition hold for `F`. -/
+instance addLeftMono : AddLeftMono F :=
   ⟨by boom⟩
 
-example : CovariantClass F F (Function.swap (· + ·)) (· ≤ ·) := by infer_instance
+example : AddRightMono F := by infer_instance
 
 /-- The following examples show that `F` has all the typeclasses used by
-`Finsupp.Lex.covariantClass_le_left`... -/
+`Finsupp.Lex.addLeftStrictMono`... -/
 example : LinearOrder F := by infer_instance
 
 example : AddMonoid F := by infer_instance
 
 /-- ... except for the strict monotonicity of addition, the crux of the matter. -/
-example : ¬CovariantClass F F (· + ·) (· < ·) := fun h =>
+example : ¬AddLeftStrictMono F := fun h =>
   lt_irrefl 1 <| (h.elim : Covariant F F (· + ·) (· < ·)) 1 z01
 
 /-- A few `simp`-lemmas to take care of trivialities in the proof of the example below. -/
@@ -220,8 +220,8 @@ theorem f110 : ofLex (Finsupp.single (1 : F) (1 : F)) 0 = 0 :=
 
 /-- Here we see that (not-necessarily strict) monotonicity of addition on `Lex (F →₀ F)` is not
 a consequence of monotonicity of addition on `F`.  Strict monotonicity of addition on `F` is
-enough and is the content of `Finsupp.Lex.covariantClass_le_left`. -/
-example : ¬CovariantClass (Lex (F →₀ F)) (Lex (F →₀ F)) (· + ·) (· ≤ ·) := by
+enough and is the content of `Finsupp.Lex.addLeftStrictMono`. -/
+example : ¬AddLeftMono (Lex (F →₀ F)) := by
   rintro ⟨h⟩
   refine (not_lt (α := Lex (F →₀ F))).mpr (@h (Finsupp.single (0 : F) (1 : F))
     (Finsupp.single 1 1) (Finsupp.single 0 1) ?_) ⟨1, ?_⟩

LongestPole/Main.lean

@@ -54,7 +54,7 @@ def RunResponse.instructions (response : RunResponse) :
   for m in response.run.result.measurements do
     let n := m.dimension.benchmark
     if n.startsWith "~" then
-      r := r.insert (n.drop 1).toName m.value
+      r := r.insert (n.drop 1).toName (m.value/10^6)
   return r
 
 def instructions (run : String) : IO (NameMap Float) :=
@@ -116,6 +116,19 @@ def Float.toStringDecimals (r : Float) (digits : Nat) : String :=
   | [a, b] => a ++ "." ++ b.take digits
   | _ => r.toString
 
+open System in
+-- Lines of code is obviously a `Nat` not a `Float`,
+-- but we're using it here as a very rough proxy for instruction count.
+def countLOC (modules : List Name) : IO (NameMap Float) := do
+  let mut r := {}
+  for m in modules do
+    let fp := FilePath.mk ((← findOLean m).toString.replace ".lake/build/lib/" "")
+      |>.withExtension "lean"
+    if ← fp.pathExists then
+      let src ← IO.FS.readFile fp
+      r := r.insert m (src.toList.count '\n').toFloat
+  return r
+
 /-- Implementation of the longest pole command line program. -/
 def longestPoleCLI (args : Cli.Parsed) : IO UInt32 := do
   let to ← match args.flag? "to" with
@@ -126,7 +139,10 @@ def longestPoleCLI (args : Cli.Parsed) : IO UInt32 := do
     let graph := env.importGraph
     let sha ← headSha
     IO.eprintln s!"Analyzing {to} at {sha}"
-    let instructions ← SpeedCenterAPI.instructions (sha)
+    let instructions ← if args.hasFlag "loc" then
+      countLOC (graph.toList.map (·.1))
+    else
+      SpeedCenterAPI.instructions sha
     let cumulative := cumulativeInstructions instructions graph
     let total := totalInstructions instructions graph
     let slowest := slowestParents cumulative graph
@@ -138,10 +154,12 @@ def longestPoleCLI (args : Cli.Parsed) : IO UInt32 := do
       let c := cumulative.find! n'
       let t := total.find! n'
       let r := (t / c).toStringDecimals 2
-      table := table.push #[n.get!.toString, toString (i/10^6 |>.toUInt64), toString (c/10^6 |>.toUInt64), r]
+      table := table.push
+        #[n.get!.toString, toString (i |>.toUInt64), toString (c |>.toUInt64), r]
       n := slowest.find? n'
+    let instructionsHeader := if args.hasFlag "loc" then "LoC" else "instructions"
     IO.println (formatTable
-                  #["file", "instructions", "cumulative", "parallelism"]
+                  #["file", instructionsHeader, "cumulative", "parallelism"]
                   table
                   #[Alignment.left, Alignment.right, Alignment.right, Alignment.center])
   return 0
@@ -157,6 +175,7 @@ def pole : Cmd := `[Cli|
 
   FLAGS:
     to : ModuleName;      "Calculate the longest pole to the specified module."
+    loc;                  "Use lines of code instead of speedcenter instruction counts."
 ]
 
 /-- `lake exe pole` -/