Merge remote-tracking branch 'upstream/main' into documentation

SampCert/DifferentialPrivacy/ZeroConcentrated/ConcentratedBound.lean

@@ -75,6 +75,7 @@ theorem SG_Renyi_simplify {σ : ℝ} (h : σ ≠ 0) (μ ν : ℤ) (α : ℝ) :
   conv =>
     left
     rw [← mul_assoc]
+  rfl
 
 noncomputable def RenyiDivergence' (p q : T → ℝ) (α : ℝ) : ℝ :=
   (1 / (α - 1)) * Real.log (∑' x : T, (p x)^α  * (q x)^(1 - α))

SampCert/DifferentialPrivacy/ZeroConcentrated/Foundations/Composition/Properties.lean

@@ -18,10 +18,7 @@ theorem ENNReal_toTeal_NZ (x : ENNReal) (h1 : x ≠ 0) (h2 : x ≠ ⊤) :
   unfold ENNReal.toReal
   unfold ENNReal.toNNReal
   simp
-  intro H
-  cases H
-  . contradiction
-  . contradiction
+  constructor ; any_goals trivial
 
 theorem simp_α_1 {α : ℝ} (h : 1 < α) : 0 < α := by
   apply @lt_trans _ _ _ 1 _ _ h
@@ -82,8 +79,8 @@ theorem compose_sum_rw (nq1 nq2 : List T → SLang ℤ) (b c : ℤ) (l : List T)
     rw [A]
   rw [ENNReal.tsum_eq_add_tsum_ite b]
   simp
-  have B : ∀ x : ℤ, (@ite ℝ≥0∞ (x = b) (instDecidableEqInt x b) 0
-    (@ite ℝ≥0∞ (b = x) (instDecidableEqInt b x) (nq1 l x * ∑' (a_1 : ℤ), @ite ℝ≥0∞ (c = a_1) (instDecidableEqInt c a_1) (nq2 l a_1) 0) 0)) = 0 := by
+  have B : ∀ x : ℤ, (@ite ℝ≥0∞ (x = b) (x.instDecidableEq b) 0
+    (@ite ℝ≥0∞ (b = x) (b.instDecidableEq x) (nq1 l x * ∑' (a_1 : ℤ), @ite ℝ≥0∞ (c = a_1) (c.instDecidableEq a_1) (nq2 l a_1) 0) 0)) = 0 := by
     intro x
     split
     . simp
@@ -102,7 +99,7 @@ theorem compose_sum_rw (nq1 nq2 : List T → SLang ℤ) (b c : ℤ) (l : List T)
   congr 1
   rw [ENNReal.tsum_eq_add_tsum_ite c]
   simp
-  have C :∀ x : ℤ,  (@ite ℝ≥0∞ (x = c) (propDecidable (x = c)) 0 (@ite ℝ≥0∞ (c = x) (instDecidableEqInt c x) (nq2 l x) 0)) = 0 := by
+  have C :∀ x : ℤ,  (@ite ℝ≥0∞ (x = c) (propDecidable (x = c)) 0 (@ite ℝ≥0∞ (c = x) (c.instDecidableEq x) (nq2 l x) 0)) = 0 := by
     intro x
     split
     . simp
@@ -193,13 +190,6 @@ theorem DPCompose_NonZeroNQ {nq1 nq2 : List T → SLang ℤ} (nn1 : NonZeroNQ nq
   replace nn2 := nn2 l b
   simp [Compose]
   exists a
-  simp
-  intro H
-  cases H
-  . rename_i H
-    contradiction
-  . rename_i H
-    contradiction
 
 theorem DPCompose_NonTopNQ {nq1 nq2 : List T → SLang ℤ} (nt1 : NonTopNQ nq1) (nt2 : NonTopNQ nq2) :
   NonTopNQ (Compose nq1 nq2) := by

SampCert/DifferentialPrivacy/ZeroConcentrated/Foundations/Mechanism/Properties.lean

@@ -49,7 +49,7 @@ theorem NoisedQueryDP (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+) (bounded_
   . have A : (α * ↑↑ε₁ ^ 2 * (↑↑ε₂ ^ 2)⁻¹) ≤ (α * ↑↑ε₁ ^ 2 * (↑↑ε₂ ^ 2)⁻¹) := le_refl (α * ↑↑ε₁ ^ 2 * (↑↑ε₂ ^ 2)⁻¹)
     have B : 0 ≤ (α * ↑↑ε₁ ^ 2 * (↑↑ε₂ ^ 2)⁻¹) := by
       simp
-      apply @le_trans ℝ _ 0 1 α (instStrictOrderedCommRingReal.proof_3) (le_of_lt h1)
+      apply @le_trans ℝ _ 0 1 α (zero_le_one' ℝ) (le_of_lt h1)
     apply mul_le_mul A _ _ B
     . apply sq_le_sq.mpr
       simp only [abs_cast]
@@ -84,7 +84,7 @@ theorem NoisedQuery_NonTopNQ (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+) :
   rw [ENNReal.tsum_eq_add_tsum_ite (n - query l)]
   simp
   have X : ∀ x : ℤ, (@ite ℝ≥0∞ (x = n - query l) (propDecidable (x = n - query l)) 0
-    (@ite ℝ≥0∞ (n = x + query l) (instDecidableEqInt n (x + query l))
+    (@ite ℝ≥0∞ (n = x + query l) (n.instDecidableEq (x + query l))
   (ENNReal.ofReal (discrete_gaussian (↑↑Δ * ↑↑ε₂ / ↑↑ε₁) 0 ↑x)) 0)) = 0 := by
     intro x
     split
@@ -116,7 +116,7 @@ theorem NoisedQuery_NonTopSum (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+) :
   simp [NonTopSum, NoisedQuery, DiscreteGaussianGenSample]
   intro l
   have X : ∀ n: ℤ, ∀ x : ℤ, (@ite ℝ≥0∞ (x = n - query l) (propDecidable (x = n - query l)) 0
-    (@ite ℝ≥0∞ (n = x + query l) (instDecidableEqInt n (x + query l))
+    (@ite ℝ≥0∞ (n = x + query l) (n.instDecidableEq (x + query l))
     (ENNReal.ofReal (discrete_gaussian (↑↑Δ * ↑↑ε₂ / ↑↑ε₁) 0 ↑x)) 0)) = 0 := by
     intro n x
     split
@@ -158,7 +158,7 @@ theorem NoisedQuery_NonTopRDNQ (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+)
   simp [NonTopRDNQ, NoisedQuery, DiscreteGaussianGenSample]
   intro α _ l₁ l₂ _
   have A : ∀ x_1 x : ℤ, (@ite ℝ≥0∞ (x_1 = x - query l₁) (propDecidable (x_1 = x - query l₁)) 0
-  (@ite ℝ≥0∞ (x = x_1 + query l₁) (instDecidableEqInt x (x_1 + query l₁))
+  (@ite ℝ≥0∞ (x = x_1 + query l₁) (x.instDecidableEq (x_1 + query l₁))
   (ENNReal.ofReal (discrete_gaussian (↑↑Δ * ↑↑ε₂ / ↑↑ε₁) 0 ↑x_1)) 0 )) = 0 := by
     intro x y
     split
@@ -169,7 +169,7 @@ theorem NoisedQuery_NonTopRDNQ (query : List T → ℤ) (Δ ε₁ ε₂ : ℕ+)
         simp at h1
       . simp
   have B : ∀ x_1 x : ℤ, (@ite ℝ≥0∞ (x_1 = x - query l₂) (propDecidable (x_1 = x - query l₂)) 0
-    (@ite ℝ≥0∞ (x = x_1 + query l₂) (instDecidableEqInt x (x_1 + query l₂))
+    (@ite ℝ≥0∞ (x = x_1 + query l₂) (x.instDecidableEq (x_1 + query l₂))
   (ENNReal.ofReal (discrete_gaussian (↑↑Δ * ↑↑ε₂ / ↑↑ε₁) 0 ↑x_1)) 0)) = 0 := by
     intro x y
     split

SampCert/DifferentialPrivacy/ZeroConcentrated/Foundations/Postprocessing/Properties.lean

@@ -147,6 +147,7 @@ theorem δpmf_conv (nq : SLang U) (a : ℤ) (x : {n | a = f n}) (h1 : ∑' (i :
     right
     left
     left
+  rfl
 
 theorem δpmf_conv' (nq : SLang U) (f : U → ℤ) (a : ℤ) (h1 : ∑' (i : ↑{n | a = f n}), nq ↑i ≠ 0) (h2 : ∑' (i : ↑{n | a = f n}), nq ↑i ≠ ⊤) :
   (fun x : {n | a = f n} => nq x * (∑' (x : {n | a = f n}), nq x)⁻¹) = (δpmf nq f a h1 h2) := by

SampCert/DifferentialPrivacy/ZeroConcentrated/Queries/BoundedSum/Properties.lean

@@ -19,7 +19,7 @@ namespace SLang
 theorem BoundedSumQuerySensitivity (U : ℕ+) : sensitivity (BoundedSumQuery U) U := by
   simp [sensitivity, BoundedSumQuery]
   intros l₁ l₂ H
-  have A : ∀ n : ℕ, (@min ℤ instMinInt (n : ℤ) (U : ℤ) = n) ∨ (@min ℤ instMinInt n U = U) := by
+  have A : ∀ n : ℕ, (min (n : ℤ) (U : ℤ) = n) ∨ (min (n : ℤ) U = U) := by
     intro n
     simp
     exact Nat.le_total n ↑U

SampCert/Extractor/Extension.lean

@@ -13,7 +13,7 @@ structure State where
   map : SMap Name String := {}
   decls : List String := []
   inlines : List String := []
-  glob : SMap Name MDef := {}
+  glob : SMap String MDef := {}
   deriving Inhabited
 
 def State.switch (s : State) : State :=

SampCert/Foundations/Auto.lean

@@ -10,13 +10,9 @@ attribute [simp] Pure.pure
 attribute [simp] CoeT.coe
 attribute [simp] instCoeT
 attribute [simp] CoeHTCT.coe
-attribute [simp] instCoeHTCT_1
 attribute [simp] CoeHTC.coe
-attribute [simp] instCoeHTC_1
 attribute [simp] CoeOTC.coe
-attribute [simp] instCoeOTC_1
 attribute [simp] CoeTC.coe
-attribute [simp] instCoeTC_1
 attribute [simp] Coe.coe
 attribute [simp] optionCoe
 attribute [simp] CoeOut.coe

SampCert/Foundations/UniformP2.lean

@@ -106,24 +106,20 @@ theorem uniformPowerOfTwoSample_apply (n : PNat) (x : Nat) (h : x < 2 ^ (log 2 n
 Evaluates the ``uniformPowerOfTwoSample`` distribution at a point outside of its support
 -/
 @[simp]
-theorem uniformPowerOfTwoSample_apply' (n : PNat) (x : Nat) (h : x ≥ 2 ^ (log 2 n)) :
-  uniformPowerOfTwoSample n x = 0 := by
-  simp only [uniformPowerOfTwoSample, Lean.Internal.coeM, Bind.bind, Pure.pure, CoeT.coe,
-    CoeHTCT.coe, CoeHTC.coe, CoeOTC.coe, CoeOut.coe, toSLang_apply, PMF.bind_apply,
-    uniformOfFintype_apply, Fintype.card_fin, cast_pow, cast_ofNat, PMF.pure_apply,
-    ENNReal.tsum_eq_zero, _root_.mul_eq_zero, ENNReal.inv_eq_zero, ENNReal.pow_eq_top_iff,
-    ENNReal.two_ne_top, ne_eq, log_eq_zero_iff, reduceLE, or_false, not_lt, false_and, false_or]
+theorem UniformPowerOfTwoSample_apply' (n : PNat) (x : Nat) (h : x ≥ 2 ^ (log 2 n)) :
+  UniformPowerOfTwoSample n x = 0 := by
+  simp [UniformPowerOfTwoSample]
   intro i
   cases i
   rename_i i P
   simp only
-  split
-  . rename_i h'
-    subst h'
-    have A : x < 2 ^ log 2 ↑n ↔ ¬ x ≥ 2 ^ log 2 ↑n := by exact lt_iff_not_le
-    rw [A] at P
-    contradiction
-  . simp
+  have A : i < 2 ^ log 2 ↑n ↔ ¬ i ≥ 2 ^ log 2 ↑n := by exact lt_iff_not_le
+  rw [A] at P
+  simp at P
+  by_contra CONTRA
+  subst CONTRA
+  replace A := A.1 P
+  contradiction
 
 lemma if_simpl_up2 (n : PNat) (x x_1: Fin (2 ^ log 2 ↑n)) :
   (@ite ENNReal (x_1 = x) (propDecidable (x_1 = x)) 0 (@ite ENNReal ((@Fin.val (2 ^ log 2 ↑n) x) = (@Fin.val (2 ^ log 2 ↑n) x_1)) (propDecidable ((@Fin.val (2 ^ log 2 ↑n) x) = (@Fin.val (2 ^ log 2 ↑n) x_1))) 1 0)) = 0 := by
@@ -172,5 +168,3 @@ theorem uniformPowerOfTwoSample_normalizes (n : PNat) :
   . exact ENNReal.summable
 
 end SLang
-
-#lint docBlame

SampCert/Samplers/BernoulliNegativeExponential/Properties.lean

@@ -560,7 +560,7 @@ theorem BernoulliExpNegSampleUnitAux_apply' (num : ℕ) (den : ℕ+) (n : ℕ) (
   . contradiction
   . rename_i n
     let m : ℕ+ := ⟨ succ n , by exact Fin.pos { val := n, isLt := le.refl } ⟩
-    have A : succ n = m := rfl
+    have A : n + 1 = m := rfl
     rw [A]
     rw [BernoulliExpNegSampleUnitAux_apply num den m wf]
     split
@@ -731,7 +731,7 @@ theorem mass_simpl (n : ℕ) (γ : ENNReal) (h : n ≥ 2) :
       rw [B] at A
       clear B
       rw [← A]
-      simp only [cast_mul, ENNReal.nat_cast_sub, cast_one]
+      simp only [cast_mul, ENNReal.natCast_sub, cast_one]
     . simp only [ne_eq, cast_eq_zero, ENNReal.sub_eq_top_iff, ENNReal.natCast_ne_top,
       ENNReal.one_ne_top, not_false_eq_true, and_true, or_true]
     . simp only [ne_eq, ENNReal.natCast_ne_top, not_false_eq_true, true_or]
@@ -756,10 +756,10 @@ theorem mass_simpl (n : ℕ) (γ : ENNReal) (h : n ≥ 2) :
         have OR : n = 1 ∨ n ≥ 2 := by
           clear IH γ X
           cases n
-          . simp only [zero_eq, reduceSucc, ge_iff_le, reduceLE] at h
+          . simp at h
           . rename_i n
             cases n
-            . simp only [zero_eq, reduceSucc, ge_iff_le, reduceLE, or_false]
+            . simp
             . rename_i n
               right
               exact AtLeastTwo.prop
@@ -989,6 +989,7 @@ theorem series_step_3 (γ : ENNReal) :
     right
     intro n
     rw [mass_simpl (2 * (n + 1)) γ (A n)]
+  rfl
 
 noncomputable def mass'' (n : ℕ) (γ : ℝ) := (γ^n * (((n)!) : ℝ)⁻¹)
 

SampCert/Samplers/Gaussian/Properties.lean

@@ -83,9 +83,9 @@ theorem DiscreteGaussianSampleLoop_normalizes (num den t : ℕ+) :
 @[simp]
 theorem ite_simpl_1' (num den t : PNat) (x : ℤ) (n : ℤ) :
   (@ite ENNReal (x = n) (propDecidable (x = n)) 0
-  (@ite ENNReal (n = x) (Int.instDecidableEqInt n x)
-  (ENNReal.ofReal ((rexp (↑↑t)⁻¹ - 1) / (rexp (↑↑t)⁻¹ + 1) * rexp (-(|↑x| / ↑↑t))) *
-    ENNReal.ofReal (rexp (-(↑(Int.natAbs (Int.sub (|x| * ↑↑t * ↑↑den) ↑↑num)) ^ 2 / ((2 : ℕ+) * ↑↑num * ↑↑t ^ 2 * ↑↑den)))))
+  (@ite ENNReal (n = x) (n.instDecidableEq x)
+  (ENNReal.ofReal (((t : ℝ)⁻¹.exp - 1) / ((t : ℝ)⁻¹.exp + 1) * (-(@abs ℝ DistribLattice.toLattice AddGroupWithOne.toAddGroup ↑x / (t : ℝ))).exp) *
+    ENNReal.ofReal (-(((|x| * t * den).sub num).natAbs ^ 2 / ((2 : ℕ+) * num * (t : ℝ) ^ 2 * den))).exp)
   0)) = 0 := by
   split
   . simp
@@ -101,7 +101,7 @@ theorem DiscreteGaussianSampleLoop_apply_true (num den t : ℕ+) (n : ℤ) :
     = ENNReal.ofReal ((rexp (t)⁻¹ - 1) / (rexp (t)⁻¹ + 1)) * ENNReal.ofReal (rexp (-(Int.natAbs n / t)) *
     rexp (-((Int.natAbs (Int.sub (|n| * t * den) ↑↑num)) ^ 2 / ((2 : ℕ+) * num * ↑↑t ^ 2 * den)))) := by
   simp only [DiscreteGaussianSampleLoop, Bind.bind, Int.natCast_natAbs, Pure.pure, SLang.bind_apply,
-    DiscreteLaplaceSample_apply, NNReal.coe_nat_cast, PNat.one_coe, cast_one, NNReal.coe_one,
+    DiscreteLaplaceSample_apply, NNReal.coe_natCast, PNat.one_coe, cast_one, NNReal.coe_one,
     div_one, one_div, Int.cast_abs, SLang.pure_apply, Prod.mk.injEq, mul_ite,
     mul_one, mul_zero, tsum_bool, and_false, ↓reduceIte, and_true, BernoulliExpNegSample_apply_true,
     cast_pow, NNReal.coe_pow, PNat.mul_coe, PNat.pow_coe, cast_mul, NNReal.coe_mul, zero_add]
@@ -254,7 +254,7 @@ theorem DiscreteGaussianSample_apply (num : PNat) (den : PNat) (x : ℤ) :
 
   simp only [ENNReal.tsum_prod', tsum_bool, ↓reduceIte, DiscreteGaussianSampleLoop_apply_true,
     PNat.mk_coe, cast_add, cast_one, Int.ofNat_ediv, PNat.pow_coe, cast_pow, zero_add, ite_mul,
-    zero_mul, SLang.pure_apply, NNReal.coe_nat_cast, div_pow]
+    zero_mul, SLang.pure_apply, NNReal.coe_natCast, div_pow]
   rw [ENNReal.tsum_eq_add_tsum_ite x]
   conv =>
     left
@@ -372,6 +372,6 @@ theorem DiscreteGaussianSample_normalizes (num : PNat) (den : PNat) :
     apply discrete_gaussian_normalizes A
   . intro n
     apply discrete_gaussian_nonneg A 0 n
-  . apply discrete_gaussian_summable A 0
+  . apply discrete_gaussian_summable A
 
 end SLang

SampCert/Samplers/GaussianGen/Properties.lean

@@ -17,7 +17,7 @@ namespace SLang
 
 theorem if_simple_GaussianGen (x_1 x μ : ℤ) :
   (@ite ENNReal (x_1 = x - μ) (propDecidable (x_1 = x - μ)) 0
-  (@ite ENNReal (x = x_1 + μ) (Int.instDecidableEqInt x (x_1 + μ))
+  (@ite ENNReal (x = x_1 + μ) (x.instDecidableEq (x_1 + μ))
   (ENNReal.ofReal (gauss_term_ℝ (↑↑num / ↑↑den) 0 ↑x_1 / ∑' (x : ℤ), gauss_term_ℝ (↑↑num / ↑↑den) 0 ↑x)) 0)) = 0 := by
   split
   . simp