enc_true

formal source

  13@[simp] lemma enc_false (R : Fin n → Bool) : enc (n:=n) false R = R := by
  14  funext i; simp [enc]
  15
  16@[simp] lemma enc_true (R : Fin n → Bool) : enc (n:=n) true R = (fun i => ! (R i)) := by
  17  funext i; simp [enc]
  18
  19/-- Restrict a full word to a queried index set `M`. -/
  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]