Merge pull request #39 from leanprover/Upgrade-4.10.0-rc2

Upgrade to lean4.10.0-rc2

SampCert/DifferentialPrivacy/Pure/Const.lean

@@ -28,7 +28,6 @@ theorem privConst_DP_Bound {u : U} : DP (privConst u : Mechanism T U) 0 := by
   rw [DP_singleton]
   intros
   simp [privConst]
-  split <;> simp
 
 /--
 ``privComposeAdaptive`` satisfies zCDP

SampCert/DifferentialPrivacy/Queries/Histogram/Code.lean

@@ -44,7 +44,7 @@ A histogram with a fixed binning method and ``i+1`` bins
 Counts in the histogram are permitted to be negative.
 -/
 structure Histogram (T : Type) (num_bins : ℕ+) (B : Bins T num_bins) where
-  count : Vector ℤ num_bins
+  count : Mathlib.Vector ℤ num_bins
 
 variable {T : Type}
 variable (B : Bins T numBins)
@@ -53,7 +53,7 @@ variable (B : Bins T numBins)
 Construct an empty histagram
 -/
 def emptyHistogram : Histogram T numBins B :=
-  Histogram.mk (Vector.replicate numBins 0)
+  Histogram.mk (Mathlib.Vector.replicate numBins 0)
 
 -- Is there any way to get the discrete measure space for free?
 instance : MeasurableSpace (Histogram T numBins B) where
@@ -65,7 +65,7 @@ instance : MeasurableSpace (Histogram T numBins B) where
 -- There's probably an easier way to do this?
 instance : Countable (Histogram T numBins B) where
   exists_injective_nat' := by
-    have Y : ∃ f : Vector ℤ numBins -> ℕ, Function.Injective f := by exact Countable.exists_injective_nat'
+    have Y : ∃ f : Mathlib.Vector ℤ numBins -> ℕ, Function.Injective f := by exact Countable.exists_injective_nat'
     rcases Y with ⟨ f, Hf ⟩
     exists (fun h => f h.count)
     intro h₁ h₂

SampCert/DifferentialPrivacy/Queries/HistogramMean/Code.lean

@@ -22,7 +22,7 @@ Implementation for
 
 noncomputable section
 
-variable (dps : DPSystem ℕ)
+variable (dps : SLang.DPSystem ℕ)
 variable (numBins : ℕ+)
 variable (B : Bins ℕ numBins)
 

lake-manifest.json

@@ -1,10 +1,11 @@
-{"version": "1.0.0",
+{"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "54bb04c3119f24fde14b9068c4b2e69db52a1450",
+   "scope": "leanprover-community",
+   "rev": "c0efc1fd2a0bec51bd55c5b17348af13d7419239",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -13,6 +14,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
+   "scope": "leanprover-community",
    "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
@@ -22,7 +24,8 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "06cca4bd36b2af743d4858c5cc31604aa9da26bc",
+   "scope": "leanprover-community",
+   "rev": "deb5bd446a108da8aa8c1a1b62dd50722b961b73",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,25 +34,28 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "87c1e7a427d8e21b6eaf8401f12897f52e2c3be9",
+   "scope": "leanprover-community",
+   "rev": "d1b33202c3a29a079f292de65ea438648123b635",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.38",
+   "inputRev": "v0.0.39",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
+   "scope": "",
    "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover-community/import-graph.git",
+  {"url": "https://github.com/leanprover-community/import-graph",
    "type": "git",
    "subDir": null,
-   "rev": "c29c3cdce415240e9dcec5c583ad5d36f83f9c71",
+   "scope": "leanprover-community",
+   "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -58,37 +64,11 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "f0957a7575317490107578ebaee9efaf8e62a4ab",
+   "scope": "",
+   "rev": "984c68d7773ac133c74543b99b82c33e53baea6b",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.9.0",
-   "inherited": false,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/acmepjz/md4lean",
-   "type": "git",
-   "subDir": null,
-   "rev": "9148a0a7506099963925cf239c491fcda5ed0044",
-   "name": "MD4Lean",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/fgdorais/lean4-unicode-basic",
-   "type": "git",
-   "subDir": null,
-   "rev": "c74a052aebee847780e165611099854de050adf7",
-   "name": "UnicodeBasic",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
-   "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/doc-gen4",
-   "type": "git",
-   "subDir": null,
-   "rev": "c369436d21c583a60da62d4513c7b9ea08389074",
-   "name": "«doc-gen4»",
-   "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.10.0-rc2",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "sampcert",

lakefile.lean

@@ -5,7 +5,7 @@ package «sampcert» where
   -- add any package configuration options here
 
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git" @ "v4.9.0"
+  "https://github.com/leanprover-community/mathlib4.git" @ "v4.10.0-rc2"
 
 @[default_target]
 lean_lib «SampCert» where

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.9.0
+leanprover/lean4:v4.10.0-rc2