chore: bump version to 4.29

SampCert/DifferentialPrivacy/Approximate/DP.lean

@@ -39,7 +39,9 @@ theorem ApproximateDP_gt1 (m : Mechanism T U) (ε : ℝ) {δ : NNReal} (Hδ : 1
     rw [<- PMF.tsum_coe (m l₁)]
     apply ENNReal.tsum_le_tsum
     intro u
-    split <;> simp
+    split
+    · exact le_refl _
+    · exact zero_le _
   apply le_trans H1
   conv =>
     left

SampCert/DifferentialPrivacy/Generic.lean

@@ -146,7 +146,6 @@ lemma compose_sum_rw_adaptive (nq1 : List T → SPMF U) (nq2 : U -> List T → S
   rw [tsum_ite_eq]
   exact MulOneClass.mul_one (nq2 u l v)
 
-
 /--
 Chain rule relating the adaptive composition definitions
 
@@ -157,9 +156,7 @@ lemma privComposeChainRule (nq1 : Mechanism T U) (nq2 : U -> Mechanism T V) (l :
   intros u v
   rw [<- compose_sum_rw_adaptive]
   simp [privComposeAdaptive]
-  simp [SPMF.instFunLike]
-
-
+  simp [DFunLike.coe]
 
 -- @[simp]
 -- lemma bind_bind_indep (p : Mechanism T U) (q : Mechanism T V) (h : U → V → PMF A) :

SampCert/DifferentialPrivacy/Pure/AdaptiveComposition.lean

@@ -15,6 +15,8 @@ open Classical Set
 
 namespace SLang
 
+set_option pp.coercions false
+
 -- Better proof for Pure DP adaptive composition
 theorem PureDP_ComposeAdaptive' (nq1 : List T → PMF U) (nq2 : U -> List T → PMF V) (ε₁ ε₂ ε : NNReal) (h1 : PureDP nq1 ε₁)  (h2 : ∀ u : U, PureDP (nq2 u) ε₂) (Hε : ε₁ + ε₂ = ε ) :
   PureDP (privComposeAdaptive nq1 nq2) ε := by
@@ -30,31 +32,35 @@ theorem PureDP_ComposeAdaptive' (nq1 : List T → PMF U) (nq2 : U -> List T →
   rw [ENNReal.ofReal_mul ?s1]
   case s1 => apply Real.exp_nonneg
   rw [ENNReal.div_eq_inv_mul]
-
+  simp [DFunLike.coe]
   cases Classical.em ((nq1 l₂) u * (nq2 u l₂) v = 0)
   · rename_i Hz
+    simp only [DFunLike.coe] at Hz
     rw [Hz]
     simp
     simp at Hz
     cases Hz
     · cases (Classical.em (nq1 l₁ u = 0))
-      · simp_all
+      · simp_all [DFunLike.coe]
       · rename_i HA HB
+        simp_all only [DFunLike.coe]
         exfalso
         have hcont := h1 l₁ l₂ Hl₁l₂ u
         simp [HA, division_def] at hcont
         rw [ENNReal.mul_top HB] at hcont
         simp_all
     · cases (Classical.em (nq2 u l₁ v = 0))
-      · simp_all
+      · simp_all [DFunLike.coe]
       · rename_i HA HB
         exfalso
         have hcont := h2 u
         rw [event_eq_singleton] at hcont
         simp [DP_singleton] at hcont
         have hcont := hcont l₁ l₂ Hl₁l₂ v
+        simp [DFunLike.coe] at hcont
         simp [HA, division_def] at hcont
-        rw [ENNReal.mul_top HB] at hcont
+        rw [ENNReal.mul_top ?G] at hcont
+        case G => exact (Ne.intro (HB ·.symm)).symm
         simp_all
   · rw [ENNReal.mul_inv]
     · rw [<- mul_assoc]
@@ -73,8 +79,8 @@ theorem PureDP_ComposeAdaptive' (nq1 : List T → PMF U) (nq2 : U -> List T →
     · left
       rename_i hnz
       intro HK
-      simp_all
+      simp_all [DFunLike.coe]
     · right
       intro HK
-      simp_all
+      simp_all [DFunLike.coe]
 end SLang

SampCert/DifferentialPrivacy/Pure/DP.lean

@@ -99,9 +99,10 @@ theorem ApproximateDP_of_DP (m : Mechanism T U) (ε : ℝ) (h : DP m ε) :
       apply ENNReal.tsum_le_tsum
       intro u
       split <;> simp
-    rw [PMF.tsum_coe] at H1
     intro HK
     simp_all
+    have HK'' : ∑' (x : U), (m l₂) x = 1 := HasSum.tsum_eq (m l₂ |>.property)
+    simp [HK''] at H1
   apply le_trans h
   simp
 

SampCert/DifferentialPrivacy/Pure/Postprocessing.lean

@@ -29,7 +29,7 @@ lemma privPostProcess_DP_bound {nq : Mechanism T U} {ε : NNReal} (h : PureDP nq
   replace h := h l₁ l₂ neighbours
   simp [privPostProcess]
   apply ENNReal.div_le_of_le_mul
-  simp [SPMF.instFunLike]
+  simp [DFunLike.coe]
   rw [← ENNReal.tsum_mul_left]
   apply ENNReal.tsum_le_tsum
   intro i

SampCert/DifferentialPrivacy/Queries/AboveThresh/Privacy.lean

@@ -45,7 +45,7 @@ lemma tsum_shift (Δ : ℤ) (f : ℤ → ENNReal) : (∑'(x : ℤ), f x = ∑'(x
 lemma laplace_inequality' (τ τ' : ℤ) (Δ : ℕ+) :
       ((ENNReal.ofReal (Real.exp (-abs τ' / (Δ * ε₂ / ε₁)))) * ((DiscreteLaplaceGenSamplePMF (Δ * ε₂) ε₁ 0 τ))) ≤
       (DiscreteLaplaceGenSamplePMF (Δ * ε₂) ε₁ 0) (τ + τ') := by
-  simp [DiscreteLaplaceGenSamplePMF, PMF.instFunLike]
+  simp [DiscreteLaplaceGenSamplePMF, DFunLike.coe]
   generalize HA : (Real.exp (↑↑ε₁ / (↑↑Δ * ↑↑ε₂)) - 1) = A
   generalize HB : (Real.exp (↑↑ε₁ / (↑↑Δ * ↑↑ε₂)) + 1) = B
   generalize HC : ((Δ : Real) * ε₂ / ε₁) = C

SampCert/DifferentialPrivacy/Queries/AboveThresh/Properties.lean

@@ -63,22 +63,11 @@ lemma probBind_congr_strong (p : SLang T) (f : T -> SLang U) (g : T -> SLang U)
   unfold probBind
   apply SLang.ext
   intro u
-  apply Equiv.tsum_eq_tsum_of_support ?G1
-  case G1 =>
-    apply Set.BijOn.equiv (fun x => x)
-    simp [Function.support]
-    have Heq : {x | ¬p x = 0 ∧ ¬f x u = 0} =  {x | ¬p x = 0 ∧ ¬g x u = 0} := by
-      apply Set.sep_ext_iff.mpr
-      intro t Ht
-      rw [Hcong]
-      apply Ht
-    rw [Heq]
-    apply Set.bijOn_id
-  simp [Function.support]
-  intro t Hp _
-  simp [Set.BijOn.equiv]
-  rw [Hcong]
-  exact Hp
+  apply tsum_congr
+  intro t
+  by_cases hp : p t = 0
+  · simp [hp]
+  · rw [Hcong t hp]
 
 
 
@@ -1680,6 +1669,8 @@ def sv6_sv7_eq (qs :  sv_query sv_T) (T : ℤ) (ε₁ ε₂ : ℕ+) (l : List sv
         intro K
         simp [K] at HL
     · simp
+      intros
+      rfl
 
 /-
 ## Program v8
@@ -1733,6 +1724,7 @@ lemma sv7_sv8_cond_eq (qs :  sv_query sv_T) (T : ℤ) (τ : ℤ) (l : List sv_T)
   · intro v0 init
     simp [sv6_cond_rec, sv4_aboveThreshC, sv1_aboveThreshC, sv1_threshold, sv1_noise, List.length]
     simp [sv8_G, sv8_sum]
+    rfl
   · intro vi init
     rename_i vi_1 rest IH
     have IH' := IH vi_1 (init ++ [vi])
@@ -1763,7 +1755,8 @@ def sv7_sv8_eq (qs :  sv_query sv_T) (T : ℤ) (ε₁ ε₂ : ℕ+) (l : List sv
   rename_i point'
   simp only []
   repeat (apply tsum_congr; intro _; congr 1)
-  simp only [sv7_sv8_cond_eq, sv6_cond]
+  simp [sv7_sv8_cond_eq, sv6_cond]
+  rfl
 
 
 /-

SampCert/DifferentialPrivacy/Queries/Histogram/Code.lean

@@ -80,7 +80,7 @@ instance : Inhabited (Histogram T numBins B) where
   default := emptyHistogram numBins B
 
 instance : DiscreteMeasurableSpace (Histogram T numBins B) where
-  forall_measurableSet := by simp
+  forall_measurableSet _ :=  MeasurableSet.congr trivial rfl
 
 namespace SLang
 

SampCert/DifferentialPrivacy/Queries/HistogramMean/Properties.lean

@@ -27,34 +27,17 @@ variable (numBins : ℕ+)
 variable (B : Bins ℕ numBins)
 variable (unbin : Fin numBins -> ℕ+)
 
--- FIXME: Can I get away without these?
-
-instance : MeasurableSpace (Option (Fin ↑numBins) × Option ℚ) where
-  MeasurableSet' _ := True
-  measurableSet_empty := by simp only
-  measurableSet_compl := by simp only [implies_true]
-  measurableSet_iUnion := by simp only [implies_true]
-
+instance : MeasurableSpace (Option (Fin ↑numBins) × Option ℚ) := ⊤
 instance : DiscreteMeasurableSpace (Option (Fin ↑numBins) × Option ℚ) where
-  forall_measurableSet := by simp only [MeasurableSpace.measurableSet_top, implies_true]
-
-instance : MeasurableSpace (Option ℚ) where
-  MeasurableSet' _ := True
-  measurableSet_empty := by simp only
-  measurableSet_compl := by simp only [implies_true]
-  measurableSet_iUnion := by simp only [implies_true]
+  forall_measurableSet _ := .congr trivial rfl
 
+instance : MeasurableSpace (Option ℚ) := ⊤
 instance : DiscreteMeasurableSpace (Option ℚ) where
-  forall_measurableSet := by simp only [MeasurableSpace.measurableSet_top, implies_true]
-
-instance : MeasurableSpace (Option (Fin ↑numBins)) where
-  MeasurableSet' _ := True
-  measurableSet_empty := by simp only
-  measurableSet_compl := by simp only [implies_true]
-  measurableSet_iUnion := by simp only [implies_true]
+  forall_measurableSet _ := .congr trivial rfl
 
+instance : MeasurableSpace (Option (Fin ↑numBins)) := ⊤
 instance : DiscreteMeasurableSpace (Option (Fin ↑numBins)) where
-  forall_measurableSet := by simp only [MeasurableSpace.measurableSet_top, implies_true]
+  forall_measurableSet _ := .congr trivial rfl
 
 
 /--

SampCert/DifferentialPrivacy/Queries/Sparse/Privacy.lean

@@ -25,14 +25,9 @@ variable (qs : sv_query sv_T)
 lemma shift_qs_add {T : Type} (qs' : sv_query T) (A B : ℕ) : (shift_qs A (shift_qs B qs')) = (shift_qs (A + B) qs') := by
   apply funext; simp [shift_qs, add_assoc]
 
-local instance : MeasurableSpace (List ℕ) where
-  MeasurableSet' _ := True
-  measurableSet_empty := by simp only
-  measurableSet_compl := by simp only [imp_self, implies_true]
-  measurableSet_iUnion := by simp only [implies_true]
-
+local instance : MeasurableSpace (List ℕ) := ⊤
 local instance : DiscreteMeasurableSpace (List ℕ) where
-  forall_measurableSet := by simp only [MeasurableSpace.measurableSet_top, implies_true]
+  forall_measurableSet _ := .congr trivial rfl
 
 lemma privSparseAux_DP
     (HDP : ∀ N H, ∀ ε : NNReal, (ε = ε₁ / ε₂) -> dps.prop (sv1_aboveThresh_PMF (shift_qs N qs) T H ε₁ ε₂) ε)

SampCert/DifferentialPrivacy/RenyiDivergence.lean

@@ -398,7 +398,7 @@ theorem Renyi_Jensen_strict_real [t2 : MeasurableSingletonClass T] [tcount : Cou
       · rename_i Heqx
         -- Rewrite the average
         rw [MeasureTheory.average] at Heqx
-        rw [MeasureTheory.integral_countable'] at Heqx
+        rw [MeasureTheory.integral_countable] at Heqx
         · simp at Heqx
           conv at Heqx =>
             rhs

SampCert/DifferentialPrivacy/ZeroConcentrated/AdaptiveComposition.lean

@@ -92,10 +92,10 @@ lemma privComposeAdaptive_renyi_bound {nq1 : List T → PMF U} {nq2 : U -> List
   -- Apply chain rule, and simplify powers
   conv =>
     enter [1, 1, a, 1, b]
-    rw [privComposeChainRule]
-    rw [privComposeChainRule]
-    rw [ENNReal.mul_rpow_of_ne_top (PMF.apply_ne_top _ _) (PMF.apply_ne_top _ _)]
-    rw [ENNReal.mul_rpow_of_ne_top (PMF.apply_ne_top _ _) (PMF.apply_ne_top _ _)]
+    erw [privComposeChainRule]
+    erw [privComposeChainRule]
+    erw [ENNReal.mul_rpow_of_ne_top (PMF.apply_ne_top _ _) (PMF.apply_ne_top _ _)]
+    erw [ENNReal.mul_rpow_of_ne_top (PMF.apply_ne_top _ _) (PMF.apply_ne_top _ _)]
 
   -- Bring sup into the sum
   rw [<- ENNReal.tsum_mul_right]

SampCert/DifferentialPrivacy/ZeroConcentrated/ConcentratedBound.lean

@@ -188,7 +188,7 @@ theorem Renyi_divergence_bound {σ : ℝ} (h : σ ≠ 0) (μ : ℤ) (α : ℝ) (
       left
       simp
       ring_nf
-    have E : ∀ x : ℤ, x * μ * α * 2 + (-x ^ 2 - μ ^ 2 * α) = - (x - α * μ)^2 + α * (α -1) * μ^2 := by
+    have E : ∀ x : ℤ, (x : ℝ) * μ * α * 2 - x ^ 2 - μ ^ 2 * α = - (x - α * μ)^2 + α * (α -1) * μ^2 := by
       intro x
       ring_nf
     conv =>
@@ -264,7 +264,7 @@ theorem Renyi_divergence_bound {σ : ℝ} (h : σ ≠ 0) (μ : ℤ) (α : ℝ) (
         right
         left
         ring_nf
-      have X : ∀ x : ℤ, x * ↑μ * α * 2 + (-x ^ 2 - μ ^ 2 * α) = -(x - α * μ)^2 + α * (α -1) * μ^2 := by
+      have X : ∀ x : ℤ, (x : ℝ) * ↑μ * α * 2 - x ^ 2 - μ ^ 2 * α = -(x - α * μ)^2 + α * (α -1) * μ^2 := by
         intro x
         ring_nf
       conv =>
@@ -371,10 +371,10 @@ lemma SG_Renyi_shift {σ : ℝ} (h : σ ≠ 0) (α : ℝ) (μ ν τ : ℤ) :
       rw [Int.cast_add]
       rw [add_sub_assoc]
       rw [add_sub_assoc]
-    have X : ∀ x : ℤ, ↑x * ↑β * 2 - ↑x * ↑μ * α * 2 + (↑x * α * ↑ν * 2 - ↑x * ↑ν * 2) + (↑x ^ 2 - ↑β * ↑μ * α * 2) +
-                (↑β * α * ↑ν * 2 - ↑β * ↑ν * 2) +
+    have X : ∀ x : ℤ, (x : ℝ) * ↑β * 2 - ↑x * ↑μ * α * 2 + ↑x * α * ↑ν * 2 - ↑x * ↑ν * 2 + ↑x ^ 2 - ↑β * ↑μ * α * 2 +
+                ↑β * α * ↑ν * 2 - ↑β * ↑ν * 2 +
               ↑β ^ 2 +
-            (↑μ ^ 2 * α - α * ↑ν ^ 2) +
+            ↑μ ^ 2 * α - α * ↑ν ^ 2 +
           ↑ν ^ 2 =
           (↑x ^ 2 - 2 * x * (-↑β + ↑μ * α - α * ↑ν + ↑ν)) + (- ↑β * ↑μ * α * 2 + ↑β * α * ↑ν * 2 - ↑β * ↑ν * 2 + ↑β ^ 2 + ↑μ ^ 2 * α - α * ↑ν ^ 2 + ↑ν ^ 2) := by
       intro x
@@ -490,7 +490,7 @@ theorem Renyi_Gauss_summable {σ : ℝ} (h : σ ≠ 0) (μ ν : ℤ) (α : ℝ)
     ring_nf
 
   have X : ∀ x : ℤ,
-    ↑x * ↑μ * α * 2 - ↑x * α * ↑ν * 2 + ↑x * ↑ν * 2 + (-↑x ^ 2 - ↑μ ^ 2 * α) + (α * ↑ν ^ 2 - ↑ν ^ 2)
+    (x : ℝ) * ↑μ * α * 2 - ↑x * α * ↑ν * 2 + ↑x * ↑ν * 2 - ↑x ^ 2 - ↑μ ^ 2 * α + α * ↑ν ^ 2 - ↑ν ^ 2
            = - ((↑x ^ 2 - 2 * x * (↑μ * α - α * ↑ν + ↑ν)) + (↑μ ^ 2 * α - α * ↑ν ^ 2 + ↑ν ^ 2)) := by
         intro x
         ring_nf
@@ -620,7 +620,7 @@ theorem discrete_GaussianGenSample_ZeroConcentrated {α : ℝ} (h : 1 < α) (num
     cases num
     cases den
     simp
-    apply And.intro <;> linarith
+    constructor <;> (intro h; exact absurd (Nat.cast_eq_zero.mp h) (by omega))
   have Hpmf (w : ℤ) : (discrete_gaussian_pmf A w = DiscreteGaussianGenPMF num den w) := by
     simp [discrete_gaussian_pmf]
     simp [DiscreteGaussianGenPMF]
@@ -657,8 +657,8 @@ theorem discrete_GaussianGenSample_ZeroConcentrated {α : ℝ} (h : 1 < α) (num
       · simp
       apply pow_pos
       apply mul_pos
-      · positivity
-      · apply inv_pos.mpr; positivity
+      · exact NNReal.coe_pos.mpr (Nat.cast_pos.mpr Ha)
+      · apply inv_pos.mpr; exact NNReal.coe_pos.mpr (Nat.cast_pos.mpr Hb)
     congr
     rw [ENNReal.ofReal_mul ?G1]
     case G1 => simp
@@ -668,8 +668,9 @@ theorem discrete_GaussianGenSample_ZeroConcentrated {α : ℝ} (h : 1 < α) (num
     rw [ENNReal.ofReal_mul (by positivity)]
     rw [ENNReal.ofReal_pow (by positivity)]
     rw [ENNReal.ofReal_pow (by positivity)]
-    rw [ENNReal.ofReal_inv_of_pos (by positivity)]
-    rw [ENNReal.ofReal_coe_nnreal, ENNReal.ofReal_coe_nnreal]
+    rw [ENNReal.ofReal_coe_nnreal]
+    rw [ENNReal.ofReal_inv_of_pos (by exact NNReal.coe_pos.mpr (Nat.cast_pos.mpr Hb))]
+    rw [ENNReal.ofReal_coe_nnreal]
     rw [← mul_pow]
 
 end SLang