restrict_enc_false

formal source

  20def restrict (f : Fin n → Bool) (M : Finset (Fin n)) : {i // i ∈ M} → Bool :=
  21  fun i => f i.val
  22
  23@[simp] lemma restrict_enc_false (R : Fin n → Bool) (M : Finset (Fin n)) :
  24  restrict (n:=n) (enc false R) M = restrict (n:=n) R M := by
  25  funext i; simp [restrict, enc]
  26
  27@[simp] lemma restrict_enc_true (R : Fin n → Bool) (M : Finset (Fin n)) :
  28  restrict (n:=n) (enc true R) M = (fun i => ! (restrict (n:=n) R M i)) := by
  29  funext i; simp [restrict, enc]
  30
  31/-- Extend a partial assignment on `M` to a full mask by defaulting to `false` off `M`. -/
  32def extendMask (M : Finset (Fin n)) (a : {i // i ∈ M} → Bool) : Fin n → Bool :=
  33  fun i => if h : i ∈ M then a ⟨i, h⟩ else false
  34
  35@[simp] lemma extendMask_in (M : Finset (Fin n)) (a : {i // i ∈ M} → Bool) {i : Fin n} (h : i ∈ M) :
  36  extendMask (n:=n) M a i = a ⟨i, h⟩ := by
  37  simp [extendMask, h]
  38
  39@[simp] lemma extendMask_notin (M : Finset (Fin n)) (a : {i // i ∈ M} → Bool) {i : Fin n} (h : i ∉ M) :
  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