restrict_extendMask

formal source

  40  extendMask (n:=n) M a i = false := by
  41  simp [extendMask, h]
  42
  43@[simp] lemma restrict_extendMask (M : Finset (Fin n)) (a : {i // i ∈ M} → Bool) :
  44  restrict (n:=n) (extendMask (n:=n) M a) M = a := by
  45  funext i
  46  simp [restrict, extendMask]
  47
  48/-- Any fixed-view decoder on a set `M` of queried indices can be fooled by a suitable `(b,R)`. -/
  49 theorem adversarial_failure (M : Finset (Fin n))
  50  (g : (({i // i ∈ M} → Bool)) → Bool) :
  51  ∃ (b : Bool) (R : Fin n → Bool),
  52    g (restrict (n:=n) (enc b R) M) ≠ b := by
  53  classical
  54  -- Pick an arbitrary local view `a` and force the decoder to predict `b' := g a`.
  55  let a : {i // i ∈ M} → Bool := fun _ => false
  56  let b' : Bool := g a
  57  -- Choose the true bit to be the opposite of the decoder's prediction.
  58  let b : Bool := ! b'
  59  -- Choose the mask so that the restricted encoding equals `a`.
  60  let R : Fin n → Bool :=
  61    if b then extendMask M (fun i => ! (a i)) else extendMask M a
  62  have hRestr : restrict (n:=n) (enc b R) M = a := by
  63    funext i
  64    dsimp [restrict, enc, R, extendMask]
  65    by_cases hb : b
  66    · -- b = true
  67      simp [hb, dif_pos i.property]
  68    · -- b = false
  69      simp [hb, dif_pos i.property]
  70  refine ⟨b, R, ?_⟩
  71  have hval' : g (restrict (n:=n) (enc b R) M) = g a := by
  72    simpa [hRestr]
  73  have hval : g (restrict (n:=n) (enc b R) M) = b' := by