probWhileSplit_add_r'

Author: mjdemedeiros

SampCert/DifferentialPrivacy/Queries/UnboundedMax/Properties.lean

@@ -27,6 +27,36 @@ noncomputable section
 
 namespace SLang
 
+
+/--
+Stronger congruence rule for probBind: The bound-to functions have to be equal only on the support of
+the bound-from function.
+-/
+lemma probBind_congr_strong (p : SLang T) (f : T -> SLang U) (g : T -> SLang U) (Hcong : ∀ t : T, p t ≠ 0 -> f t = g t) :
+    p >>= f = p >>= g := by
+  simp
+  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]
+  apply Hp
+
+
+
 /--
 ``SLang`` value obtained by applying a loop body exactly ``n`` times to a given distribution
 -/
@@ -217,61 +247,18 @@ lemma probWhileSplit_add_r' (cond : T → Bool) (body : T → SLang T) (m n : Na
     rename_i m''
     rw [bind_congr IH]
     clear IH
-    generalize HK : (probWhileSplit cond body (fun x => probZero) n) = K
     unfold probWhileSplit
     simp
     split <;> simp
-    · apply SLang.ext
-      simp
-      -- Monotonicity necessary here? Seems odd that I'd need it in the inductive proof but not the single step proof
-      -- However, maybe not so weird. The step I'm getting stuck on is proving asociativity, which didn't
-      -- need to happen in the 1 step proof.
-      sorry
+    · rename_i h
+      apply probBind_congr_strong
+      intro t _
+      simp [probWhileSplit]
     · rw [if_neg (by trivial)]
       simp
 
 
 
-/--
-Stronger congruence rule for probBind: The bound-to functions have to be equal only on the support of
-the bound-from function.
--/
-lemma probBind_congr_strong (p : SLang T) (f : T -> SLang U) (g : T -> SLang U) (Hcong : ∀ t : T, p t ≠ 0 -> f t = g t) :
-    p >>= f = p >>= g := by
-  simp
-  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]
-  apply Hp
-
-
-
-
-
-
-
-
-
-
-
-
-
-