Merge pull request #31 from leanprover/upgrade

chore: upgrade to Lean v4.9.0

SampCert/DifferentialPrivacy/Pure/Composition.lean

@@ -63,7 +63,6 @@ theorem privCompose_DP_bound {nq1 : Mechanism T U} {nq2 : Mechanism T V} {ε₁
             simp_all
             simp [division_def] at h1a
             rw [ENNReal.mul_top Hz''] at h1a
-            skip
             simp_all
         · cases (Classical.em (nq2 l₁ y = 0))
           · rename_i Hz''
@@ -73,7 +72,6 @@ theorem privCompose_DP_bound {nq1 : Mechanism T U} {nq2 : Mechanism T V} {ε₁
             simp_all
             simp [division_def] at h2a
             rw [ENNReal.mul_top Hz''] at h2a
-            skip
             simp_all
       · have A : nq1 l₁ x * nq2 l₁ y / (nq1 l₂ x * nq2 l₂ y) = (nq1 l₁ x / nq1 l₂ x) * (nq2 l₁ y / nq2 l₂ y) := by
           rw [division_def]

SampCert/DifferentialPrivacy/RenyiDivergence.lean

@@ -107,13 +107,8 @@ theorem RenyiDivergenceExpectation (p q : T → ENNReal) {α : ℝ} (h : 1 < α)
   ext x
   rw [AbsCts] at H
   generalize Hvq : q x = vq
-  cases vq <;> simp
-  · -- q x = ⊤
-    rw [ENNReal.zero_rpow_of_pos ?H]
-    case H => linarith
-    simp
-    right
-    apply h
+  cases vq <;> try simp_all
+  · linarith
   · rename_i vq'
     cases (Classical.em (vq' = 0))
     · -- q x = 0
@@ -128,7 +123,7 @@ theorem RenyiDivergenceExpectation (p q : T → ENNReal) {α : ℝ} (h : 1 < α)
     · -- q x ∈ ℝ+
       rename_i Hvq'
       generalize Hvp : p x = vp
-      cases vp <;> simp
+      cases vp
       · -- q x ∈ ℝ+, p x = ⊤
         rw [ENNReal.top_rpow_of_pos ?H]
         case H => linarith
@@ -142,10 +137,12 @@ theorem RenyiDivergenceExpectation (p q : T → ENNReal) {α : ℝ} (h : 1 < α)
           cases Hcont'
           · simp_all only [some_eq_coe, none_eq_top, zero_ne_top]
           · simp_all only [some_eq_coe, none_eq_top, top_rpow_of_neg, coe_ne_top, sub_neg, and_true]
-        · rw [top_mul']
-          split
-          · simp_all only [some_eq_coe, none_eq_top, zero_ne_top]
-          · rfl
+        · simp_all
+          rw [top_rpow_def]
+          split <;> try simp_all
+          split <;> try simp_all
+          · linarith
+          · linarith
       · rename_i vp
         cases (Classical.em (vq' = 0))
         · -- q x ∈ ℝ+, p x = 0
@@ -337,10 +334,10 @@ theorem Renyi_Jensen_strict_real (f : T → ℝ) (q : PMF T) (α : ℝ) (h : 1 <
       right
       simp at HR
       -- Because T is discrete, almost-everywhere equality should become equality
-      have HR' := @Filter.EventuallyEq.eventually _ _ (q.toMeasure.ae) f (Function.const T (⨍ (x : T), f x ∂q.toMeasure)) HR
+      have HR' := @Filter.EventuallyEq.eventually _ _ (ae q.toMeasure) f (Function.const T (⨍ (x : T), f x ∂q.toMeasure)) HR
       simp [Filter.Eventually] at HR'
       -- The measure of the compliment of the set in HR' is zero
-      simp [MeasureTheory.Measure.ae] at HR'
+      simp [ae] at HR'
       rw [PMF.toMeasure_apply _ _ ?Hmeas] at HR'
       case Hmeas =>
         apply (@measurableSet_discrete _ _ ?DM)

SampCert/DifferentialPrivacy/ZeroConcentrated/Composition.lean

@@ -43,7 +43,6 @@ theorem privCompose_zCDPBound {nq1 : Mechanism T U} {nq2 : Mechanism T V} {ε₁
   rw [DFunLike.coe]
   rw [PMF.instFunLike]
   simp
-  repeat rw [SLang.toPMF]
   have CG1 (b : U) : (nq1 l₂).val b ≠ ⊤ := by
     have H := PMF.apply_ne_top (nq1 l₂) b
     simp [DFunLike.coe, PMF.instFunLike] at H

SampCert/DifferentialPrivacy/ZeroConcentrated/ConcentratedBound.lean

@@ -538,7 +538,6 @@ theorem Renyi_Gauss_divergence_bound' {σ α : ℝ} (h : σ ≠ 0) (h' : 1 < α)
     unfold RenyiDivergence
     unfold RenyiDivergence_def
     unfold RenyiDivergence'
-    congr
     simp
     unfold discrete_gaussian_pmf
 
@@ -658,7 +657,6 @@ theorem discrete_GaussianGenSample_ZeroConcentrated {α : ℝ} (h : 1 < α) (num
           simp
     rw [X]
     rw [ENNReal.ofReal_div_of_pos]
-    congr
     simp
 
 end SLang

SampCert/DifferentialPrivacy/ZeroConcentrated/Mechanism/Properties.lean

@@ -212,9 +212,8 @@ theorem privNoisedQuery_zCDP (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+) (b
   simp [zCDP]
   apply And.intro
   · exact privNoisedQuery_AC query Δ ε₁ ε₂
-  · repeat any_goals constructor
-    . apply privNoisedQuery_zCDPBound
-      exact bounded_sensitivity
+  · apply privNoisedQuery_zCDPBound
+    exact bounded_sensitivity
 
 
 end SLang

SampCert/DifferentialPrivacy/ZeroConcentrated/Postprocessing.lean

@@ -188,7 +188,7 @@ theorem privPostPocess_DP_pre_reduct {U : Type} [m2 : MeasurableSpace U] [count
 
   -- Eliminate elements with probability zero
   split
-  case h.inl =>
+  case h.isTrue =>
     rename_i H
     repeat rw [condition_to_subset]
     rw [H]

SampCert/Util/Log.lean

@@ -143,15 +143,8 @@ lemma EReal_isReal_cases (w : EReal) : w = ⊥ ∨ w = ⊤ ∨ (∃ v : ℝ, w =
   cases w
   · left
     rfl
-  rename_i w'
-  cases w'
-  · right
-    left
-    rfl
-  rename_i wR
-  right
-  right
-  exists wR
+  simp_all
+  tauto
 
 syntax "case_EReal_isReal" term : tactic
 macro_rules
@@ -427,31 +420,24 @@ lemma elog_eexp {x : ENNReal} : eexp (elog x) = x := by
         simp
         rw [Hk]
 
+
 @[simp]
 lemma eexp_elog {w : EReal} : (elog (eexp w)) = w := by
   cases w
   · simp [eexp, elog]
-    rfl
-  · simp [eexp, elog]
+  · simp only [eexp, elog]
     rename_i v'
-    cases v'
-    · simp
-      rfl
-    · simp
-      rename_i v''
-      simp [ENNReal.ofReal]
-      split
-      · rename_i Hcont
-        have Hcont' : 0 < rexp v'' := by exact exp_pos v''
+    simp [Real.toEReal, ENNReal.ofReal]
+    split
+    · rename_i Hcont
+      have Hcont' : 0 < rexp v' := by exact exp_pos v'
+      linarith
+    · rename_i H
+      have RW : (max (rexp v') 0) = (rexp v') := by
+        apply max_eq_left_iff.mpr
         linarith
-      · rename_i H
-        have RW : (max (rexp v'') 0) = (rexp v'') := by
-          apply max_eq_left_iff.mpr
-          linarith
-        simp [RW]
-        clear RW
-        simp [Real.toEReal]
-
+      simp [RW]
+  · simp [eexp, elog]
 
 lemma elog_ENNReal_ofReal_of_pos {x : ℝ} (H : 0 < x) : (ENNReal.ofReal x).elog = x.log.toEReal := by
   simp [ENNReal.ofReal, ENNReal.elog, ENNReal.toEReal]
@@ -501,27 +487,24 @@ lemma eexp_injective {w z : EReal} : eexp w = eexp z -> w = z := by
   intro H
   cases w <;> cases z <;> try tauto
   · rename_i v
-    cases v <;> simp at *
-    rename_i v'
-    have Hv' := exp_pos v'
+    simp [Real.toEReal] at H
+    exfalso
+    have Hv' := exp_pos v
     linarith
   · rename_i v
-    cases v <;> simp at *
-    rename_i v'
-    have Hv' := exp_pos v'
+    simp [Real.toEReal] at H
+    have Hv' := exp_pos v
     linarith
   · rename_i v₁ v₂
-    cases v₁ <;> cases v₂ <;> simp at *
     congr
-    rename_i v₁' v₂'
-    simp [ENNReal.ofReal] at H
+    simp [Real.toEReal, ENNReal.ofReal] at H
     apply NNReal.coe_inj.mpr at H
     simp at H
     have RW (r : ℝ) : (max (rexp r) 0) = (rexp r) := by
       apply max_eq_left_iff.mpr
       exact exp_nonneg r
-    rw [RW v₁'] at H
-    rw [RW v₂'] at H
+    rw [RW v₁] at H
+    rw [RW v₂] at H
     exact exp_eq_exp.mp H
 
 
@@ -677,7 +660,6 @@ lemma mul_mul_inv_le_mul_cancel {x y : ENNReal} : (x * y⁻¹) * y ≤ x := by
   cases (Classical.em (y' = 0))
   · simp_all
   rename_i Hy'
-  simp
   rw [← coe_inv Hy']
   rw [← coe_mul]
   rw [← coe_mul]
@@ -697,85 +679,55 @@ lemma mul_mul_inv_eq_mul_cancel {x y : ENNReal} (H : y = 0 -> x = 0) (H2 : ¬(x
   cases (Classical.em (y' = 0))
   · simp_all
   rename_i Hy'
-  simp
   rw [← coe_inv Hy']
   rw [← coe_mul]
   rw [← coe_mul]
   rw [mul_right_comm]
   rw [mul_inv_cancel_right₀ Hy' x']
 
 lemma ereal_smul_le_left {w z : EReal} (s : EReal) (Hr1 : 0 < s) (Hr2 : s < ⊤) (H : s * w ≤ s * z) : w ≤ z := by
-  have defTop : some none = (⊤ : EReal) := by simp [Top.top]
-  have defBot : none = (⊥ : EReal) := by simp [Bot.bot]
-
   cases s
   · exfalso
-    rw [defBot] at Hr1
-    simp_all only [not_lt_bot]
-  rename_i s_nnr
-  cases s_nnr
-  · rw [defTop] at Hr2
-    exfalso
-    simp_all only [EReal.zero_lt_top, lt_self_iff_false]
-  rename_i s_R
-  have Hsr : some (some s_R) = Real.toEReal s_R := by simp [Real.toEReal]
-  rw [Hsr] at H
-  rw [Hsr] at Hr1
-  rw [Hsr] at Hr2
-  clear Hsr
-
-  cases w
-  · apply left_eq_inf.mp
-    rfl
-  rename_i w_nnr
-  cases w_nnr
-  · simp [defTop] at H
-    rw [EReal.mul_top_of_pos Hr1] at H
-    have X1 : z = ⊤ := by
-      cases z
-      · exfalso
-        simp at H
-        rw [defBot] at H
-        rw [EReal.mul_bot_of_pos] at H
-        · cases H
-        · apply Hr1
-      rename_i z_nnr
-      cases z_nnr
-      · simp [Top.top]
-      exfalso
-      apply top_le_iff.mp at H
-      rename_i z_R
-      have Hzr : some (some z_R) = Real.toEReal z_R := by simp [Real.toEReal]
-      rw [Hzr] at H
-      rw [<- EReal.coe_mul] at H
-      cases H
-    rw [defTop, X1]
-  rename_i w_R
-  cases z
-  · simp [defBot] at H
-    rw [EReal.mul_bot_of_pos] at H
-    apply le_bot_iff.mp at H
-    · rw [defBot]
-      have Hwr : some (some w_R) = Real.toEReal w_R := by simp [Real.toEReal]
-      rw [Hwr] at H
-      rw [<- EReal.coe_mul] at H
-      cases H
-    · apply Hr1
-  rename_i z_nnr
-  cases z_nnr
-  · exact right_eq_inf.mp rfl
-  rename_i z_R
-  have Hwr : some (some w_R) = Real.toEReal w_R := by simp [Real.toEReal]
-  have Hzr : some (some z_R) = Real.toEReal z_R := by simp [Real.toEReal]
-  rw [Hwr, Hzr] at H
-  rw [Hwr, Hzr]
-  clear Hwr
-  clear Hzr
-  apply EReal.coe_le_coe_iff.mpr
-  repeat rw [<- EReal.coe_mul] at H
-  apply EReal.coe_le_coe_iff.mp at H
-  apply le_of_mul_le_mul_left H
-  exact EReal.coe_pos.mp Hr1
+    simp at Hr1
+  · rename_i s_R
+    have Hsr : some (some s_R) = Real.toEReal s_R := by simp [Real.toEReal]
+    rw [<- Hsr] at H
+    rw [<- Hsr] at Hr1
+    rw [<- Hsr] at Hr2
+    clear Hsr
+
+    cases w
+    · apply left_eq_inf.mp
+      rfl
+    rename_i w_R
+    cases z
+    · rw [EReal.mul_bot_of_pos] at H
+      apply le_bot_iff.mp at H
+      · have Hwr : some (some s_R) = Real.toEReal s_R := by simp [Real.toEReal]
+        rw [Hwr] at H
+        rw [<- EReal.coe_mul] at H
+        cases H
+      · apply Hr1
+    rename_i z_R
+    have Hsr : some (some s_R) = Real.toEReal s_R := by simp [Real.toEReal]
+    rw [Hsr] at H
+
+    apply EReal.coe_le_coe_iff.mpr
+    repeat rw [<- EReal.coe_mul] at H
+    apply EReal.coe_le_coe_iff.mp at H
+    · apply le_of_mul_le_mul_left H
+      exact EReal.coe_pos.mp Hr1
+    · exact OrderTop.le_top w_R.toEReal
+    · rw [EReal.mul_top_of_pos] at H
+      · simp_all
+        case_EReal_isReal z
+        · rw [EReal.mul_bot_of_pos] at H
+          · cases H
+          · exact Hr1
+        · simp [Real.toEReal] at H
+          cases H
+      · exact Hr1
+  · simp at Hr2
 
 lemma ereal_smul_eq_left {w z : EReal} (s : EReal) (Hr1 : 0 < s) (Hr2 : s < ⊤) (H : s * w = s * z) : w = z := by
   apply LE.le.antisymm