sgl_vote_bridge

import Definitions.Def_sgl_casc_loop
import Definitions.Def_sgl_xor_bridge

/-!
# Votes on tapes are votes on booleans

The cascade folds cells; the counting argument folds booleans.  This module
carries the fold across `TapeSymbol.bit`, level by level, and iterated.
-/

namespace SipserGacsLautemann

/-- Every third boolean, starting at the first. -/
def bthird0 : List Bool → List Bool
  | x :: _ :: _ :: r => x :: bthird0 r
  | x :: _ :: [] => [x]
  | x :: [] => [x]
  | [] => []

/-- Every third boolean, starting at the second. -/
def bthird1 : List Bool → List Bool
  | _ :: y :: _ :: r => y :: bthird1 r
  | _ :: y :: [] => [y]
  | _ :: [] => []
  | [] => []

/-- Every third boolean, starting at the third. -/
def bthird2 : List Bool → List Bool
  | _ :: _ :: z :: r => z :: bthird2 r
  | _ :: _ :: [] => []
  | _ :: [] => []
  | [] => []

/-- The stride combination, on booleans. -/
def zip3Maj : List Bool → List Bool → List Bool → List Bool
  | [], _, _ => []
  | a :: as, bs, cs =>
      majorityVoteConstruction a (bs.headD false) (cs.headD false) ::
        zip3Maj as bs.tail cs.tail

/-- One cascade level, on booleans. -/
def boolFoldLevel (bs : List Bool) : List Bool :=
  zip3Maj (bthird0 bs) (bthird1 bs) (bthird2 bs)

theorem bthird_map (bs : List Bool) :
    third0 (bs.map TapeSymbol.bit) = (bthird0 bs).map TapeSymbol.bit ∧
    third1 (bs.map TapeSymbol.bit) = (bthird1 bs).map TapeSymbol.bit ∧
    third2 (bs.map TapeSymbol.bit) = (bthird2 bs).map TapeSymbol.bit := by
  induction bs using bthird0.induct with
  | case1 x d e r ih =>
      refine ⟨?_, ?_, ?_⟩
      · show TapeSymbol.bit x :: third0 (r.map TapeSymbol.bit) = _
        rw [ih.1]
        rfl
      · show TapeSymbol.bit d :: third1 (r.map TapeSymbol.bit) = _
        rw [ih.2.1]
        rfl
      · show TapeSymbol.bit e :: third2 (r.map TapeSymbol.bit) = _
        rw [ih.2.2]
        rfl
  | case2 x d => exact ⟨rfl, rfl, rfl⟩
  | case3 x => exact ⟨rfl, rfl, rfl⟩
  | case4 => exact ⟨rfl, rfl, rfl⟩

theorem foldCells_map_bit :
    ∀ (as bs cs : List Bool),
      foldCells (fun x y z => majorityVoteConstruction x y z)
        (as.map TapeSymbol.bit) (bs.map TapeSymbol.bit)
        (cs.map TapeSymbol.bit) =
      (zip3Maj as bs cs).map TapeSymbol.bit := by
  intro as
  induction as with
  | nil => intro bs cs; rfl
  | cons a as ih =>
      intro bs cs
      show TapeSymbol.bit (majorityVoteConstruction (cellBool
          (TapeSymbol.bit a))
        (cellBool ((bs.map TapeSymbol.bit).headD TapeSymbol.blank))
        (cellBool ((cs.map TapeSymbol.bit).headD TapeSymbol.blank))) ::
        foldCells (fun x y z => majorityVoteConstruction x y z)
          (as.map TapeSymbol.bit) (bs.map TapeSymbol.bit).tail
          (cs.map TapeSymbol.bit).tail = _
      have hb : cellBool ((bs.map TapeSymbol.bit).headD TapeSymbol.blank) =
          bs.headD false := by
        cases bs <;> rfl
      have hc : cellBool ((cs.map TapeSymbol.bit).headD TapeSymbol.blank) =
          cs.headD false := by
        cases cs <;> rfl
      have hbt : (bs.map TapeSymbol.bit).tail = bs.tail.map TapeSymbol.bit := by
        cases bs <;> rfl
      have hct : (cs.map TapeSymbol.bit).tail = cs.tail.map TapeSymbol.bit := by
        cases cs <;> rfl
      rw [hb, hc, hbt, hct, ih bs.tail cs.tail]
      rfl

theorem foldLevel_map_bit (bs : List Bool) :
    foldLevel (bs.map TapeSymbol.bit) =
      (boolFoldLevel bs).map TapeSymbol.bit := by
  unfold foldLevel boolFoldLevel
  obtain ⟨h0, h1, h2⟩ := bthird_map bs
  rw [h0, h1, h2, foldCells_map_bit]

theorem foldLevel_iterate_map_bit (k : Nat) (bs : List Bool) :
    foldLevel^[k] (bs.map TapeSymbol.bit) =
      (boolFoldLevel^[k] bs).map TapeSymbol.bit := by
  induction k generalizing bs with
  | zero => rfl
  | succ k ih =>
      rw [Function.iterate_succ_apply, Function.iterate_succ_apply,
        foldLevel_map_bit, ih]


/-- The leaves of a ternary sample, left to right. -/
def sampleLeaves {Ω : Type*} : ∀ d, TernarySampleConstruction Ω d → List Ω
  | 0, x => [x]
  | d + 1, s =>
      sampleLeaves d s.1 ++ (sampleLeaves d s.2.1 ++ sampleLeaves d s.2.2)

theorem sampleLeaves_length {Ω : Type*} :
    ∀ (d : Nat) (s : TernarySampleConstruction Ω d),
      (sampleLeaves d s).length = 3 ^ d := by
  intro d
  induction d with
  | zero => intro s; rfl
  | succ d ih =>
      intro s
      show (sampleLeaves d s.1 ++ (sampleLeaves d s.2.1 ++
        sampleLeaves d s.2.2)).length = 3 ^ (d + 1)
      rw [List.length_append, List.length_append, ih, ih, ih]
      ring

theorem zip3Maj_length : ∀ (as bs cs : List Bool),
    (zip3Maj as bs cs).length = as.length := by
  intro as
  induction as with
  | nil => intro bs cs; rfl
  | cons a as ih => intro bs cs; simp [zip3Maj, ih]

theorem bthird_length (m : Nat) (u : List Bool) (hu : u.length = 3 * m) :
    (bthird0 u).length = m ∧ (bthird1 u).length = m ∧
      (bthird2 u).length = m := by
  have h := third_lengths m (u.map TapeSymbol.bit) (by simpa using hu)
  obtain ⟨g0, g1, g2⟩ := bthird_map u
  refine ⟨?_, ?_, ?_⟩
  · have := h.1
    rw [g0, List.length_map] at this
    exact this
  · have := h.2.1
    rw [g1, List.length_map] at this
    exact this
  · have := h.2.2
    rw [g2, List.length_map] at this
    exact this

/-- The residue classes split over an append at a full group boundary. -/
theorem bthird_append : ∀ (m : Nat) (u v : List Bool),
    u.length = 3 * m →
    bthird0 (u ++ v) = bthird0 u ++ bthird0 v ∧
    bthird1 (u ++ v) = bthird1 u ++ bthird1 v ∧
    bthird2 (u ++ v) = bthird2 u ++ bthird2 v := by
  intro m
  induction m with
  | zero =>
      intro u v hu
      have : u = [] := List.length_eq_zero_iff.mp (by simpa using hu)
      subst this
      exact ⟨rfl, rfl, rfl⟩
  | succ m ih =>
      intro u v hu
      rcases u with _ | ⟨x, _ | ⟨y, _ | ⟨z, u'⟩⟩⟩
      · simp at hu
      · simp at hu; omega
      · simp at hu; omega
      · have hu' : u'.length = 3 * m := by simp at hu; omega
        obtain ⟨i0, i1, i2⟩ := ih u' v hu'
        refine ⟨?_, ?_, ?_⟩
        · show x :: bthird0 (u' ++ v) = (x :: bthird0 u') ++ bthird0 v
          rw [i0]
          rfl
        · show y :: bthird1 (u' ++ v) = (y :: bthird1 u') ++ bthird1 v
          rw [i1]
          rfl
        · show z :: bthird2 (u' ++ v) = (z :: bthird2 u') ++ bthird2 v
          rw [i2]
          rfl

theorem zip3Maj_append : ∀ (a1 b1 c1 a2 b2 c2 : List Bool),
    a1.length = b1.length → a1.length = c1.length →
    zip3Maj (a1 ++ a2) (b1 ++ b2) (c1 ++ c2) =
      zip3Maj a1 b1 c1 ++ zip3Maj a2 b2 c2 := by
  intro a1
  induction a1 with
  | nil =>
      intro b1 c1 a2 b2 c2 hb hc
      have hbnil : b1 = [] := List.length_eq_zero_iff.mp (by simpa using
        hb.symm)
      have hcnil : c1 = [] := List.length_eq_zero_iff.mp (by simpa using
        hc.symm)
      subst hbnil
      subst hcnil
      rfl
  | cons a as ih =>
      intro b1 c1 a2 b2 c2 hb hc
      rcases b1 with _ | ⟨b, bs⟩
      · simp at hb
      rcases c1 with _ | ⟨c, cs⟩
      · simp at hc
      show majorityVoteConstruction a (((b :: bs) ++ b2).headD false)
          (((c :: cs) ++ c2).headD false) ::
          zip3Maj (as ++ a2) (((b :: bs) ++ b2).tail)
            (((c :: cs) ++ c2).tail) = _
      rw [show ((b :: bs) ++ b2).headD false = b from rfl,
        show ((c :: cs) ++ c2).headD false = c from rfl,
        show ((b :: bs) ++ b2).tail = bs ++ b2 from rfl,
        show ((c :: cs) ++ c2).tail = cs ++ c2 from rfl,
        ih bs cs a2 b2 c2 (by simpa using hb) (by simpa using hc)]
      rfl

/-- One fold level splits over a group-aligned append. -/
theorem boolFoldLevel_append (m : Nat) (u v : List Bool)
    (hu : u.length = 3 * m) :
    boolFoldLevel (u ++ v) = boolFoldLevel u ++ boolFoldLevel v := by
  unfold boolFoldLevel
  obtain ⟨a0, a1, a2⟩ := bthird_append m u v hu
  obtain ⟨l0, l1, l2⟩ := bthird_length m u hu
  rw [a0, a1, a2, zip3Maj_append (bthird0 u) (bthird1 u) (bthird2 u) _ _ _
    (by rw [l0, l1]) (by rw [l0, l2])]

theorem boolFoldLevel_length (m : Nat) (u : List Bool)
    (hu : u.length = 3 * m) : (boolFoldLevel u).length = m := by
  unfold boolFoldLevel
  rw [zip3Maj_length]
  exact (bthird_length m u hu).1

/-- Iterated folds split over three power-aligned blocks. -/
theorem boolFoldLevel_iterate_append :
    ∀ (k : Nat) (u v w : List Bool),
      u.length = 3 ^ k → v.length = 3 ^ k → w.length = 3 ^ k →
      boolFoldLevel^[k] (u ++ (v ++ w)) =
        boolFoldLevel^[k] u ++
          (boolFoldLevel^[k] v ++ boolFoldLevel^[k] w) := by
  intro k
  induction k with
  | zero => intro u v w _ _ _; rfl
  | succ k ih =>
      intro u v w hu hv hw
      have h3 : (3:Nat) ^ (k + 1) = 3 * 3 ^ k := by ring
      rw [Function.iterate_succ_apply, Function.iterate_succ_apply,
        Function.iterate_succ_apply, Function.iterate_succ_apply]
      rw [boolFoldLevel_append (3 ^ k) u (v ++ w) (by omega),
        boolFoldLevel_append (3 ^ k) v w (by omega)]
      exact ih _ _ _
        (boolFoldLevel_length (3 ^ k) u (by omega))
        (boolFoldLevel_length (3 ^ k) v (by omega))
        (boolFoldLevel_length (3 ^ k) w (by omega))

/-- **The fold computes the ternary vote.** -/
theorem boolFoldLevel_vote {Ω : Type*} (vote : Ω → Bool) :
    ∀ (d : Nat) (s : TernarySampleConstruction Ω d),
      boolFoldLevel^[d] ((sampleLeaves d s).map vote) =
        [ternaryVoteConstruction vote d s] := by
  intro d
  induction d with
  | zero => intro s; rfl
  | succ d ih =>
      intro s
      show boolFoldLevel^[d + 1]
        ((sampleLeaves d s.1 ++ (sampleLeaves d s.2.1 ++
          sampleLeaves d s.2.2)).map vote) = _
      rw [List.map_append, List.map_append]
      have hl1 : ((sampleLeaves d s.1).map vote).length = 3 ^ d := by
        rw [List.length_map, sampleLeaves_length]
      have hl2 : ((sampleLeaves d s.2.1).map vote).length = 3 ^ d := by
        rw [List.length_map, sampleLeaves_length]
      have hl3 : ((sampleLeaves d s.2.2).map vote).length = 3 ^ d := by
        rw [List.length_map, sampleLeaves_length]
      rw [Function.iterate_succ_apply',
        boolFoldLevel_iterate_append d _ _ _ hl1 hl2 hl3,
        ih s.1, ih s.2.1, ih s.2.2]
      rfl


/-! ## The block sample: consecutive chunks, recursively -/

/-- Split a bit string of length `3k` into three consecutive blocks. -/
def blockSplit (k : Nat) :
    BitString (3 * k) ≃ BitString k × BitString k × BitString k where
  toFun f :=
    (fun i => f ⟨i.val, by omega⟩,
     fun i => f ⟨k + i.val, by omega⟩,
     fun i => f ⟨2 * k + i.val, by omega⟩)
  invFun t := fun j =>
    if h1 : j.val < k then t.1 ⟨j.val, h1⟩
    else if h2 : j.val < 2 * k then t.2.1 ⟨j.val - k, by omega⟩
    else t.2.2 ⟨j.val - 2 * k, by omega⟩
  left_inv f := by
    funext j
    by_cases h1 : j.val < k
    · simp only [dif_pos h1]
    · by_cases h2 : j.val < 2 * k
      · simp only [dif_neg h1, dif_pos h2]
        have hj : (⟨k + (j.val - k), by omega⟩ : Fin (3 * k)) = j :=
          Fin.ext (show k + (j.val - k) = j.val by omega)
        rw [hj]
      · simp only [dif_neg h1, dif_neg h2]
        have hlt := j.isLt
        have hj : (⟨2 * k + (j.val - 2 * k), by omega⟩ : Fin (3 * k)) = j :=
          Fin.ext (show 2 * k + (j.val - 2 * k) = j.val by omega)
        rw [hj]
  right_inv t := by
    refine Prod.ext ?_ (Prod.ext ?_ ?_)
    · funext i
      show (if h1 : i.val < k then _ else _) = t.1 i
      rw [dif_pos i.isLt]
    · funext i
      show (if h1 : k + i.val < k then _ else
        if h2 : k + i.val < 2 * k then _ else _) = t.2.1 i
      have hi := i.isLt
      rw [dif_neg (by omega), dif_pos (by omega)]
      have hj : (⟨k + i.val - k, by omega⟩ : Fin k) = i :=
        Fin.ext (show k + i.val - k = i.val by omega)
      rw [hj]
    · funext i
      show (if h1 : 2 * k + i.val < k then _ else
        if h2 : 2 * k + i.val < 2 * k then _ else _) = t.2.2 i
      have hi := i.isLt
      rw [dif_neg (by omega), dif_neg (by omega)]
      have hj : (⟨2 * k + i.val - 2 * k, by omega⟩ : Fin k) = i :=
        Fin.ext (show 2 * k + i.val - 2 * k = i.val by omega)
      rw [hj]

/-- The consecutive-block sample of a bit string. -/
def blockTernaryEquiv (rb : Nat) :
    ∀ d, BitString (rb * 3 ^ d) ≃
      TernarySampleConstruction (BitString rb) d
  | 0 =>
      Equiv.arrowCongr (finCongr (by ring)) (Equiv.refl Bool)
  | d + 1 =>
      ((Equiv.arrowCongr (finCongr (by ring)) (Equiv.refl Bool)).trans
        (blockSplit (rb * 3 ^ d))).trans
        (Equiv.prodCongr (blockTernaryEquiv rb d)
          (Equiv.prodCongr (blockTernaryEquiv rb d)
            (blockTernaryEquiv rb d)))

/-- Consecutive segments of a boolean list, as chunk lists. -/
def chunkSeg (r : List Bool) (offset rb : Nat) : Nat → List (List Bool)
  | 0 => []
  | n + 1 => segList r offset rb :: chunkSeg r (offset + rb) rb n

theorem chunkSeg_append (r : List Bool) (rb : Nat) :
    ∀ (a b : Nat) (offset : Nat),
      chunkSeg r offset rb (a + b) =
        chunkSeg r offset rb a ++ chunkSeg r (offset + rb * a) rb b := by
  intro a
  induction a with
  | zero =>
      intro b offset
      simp [chunkSeg]
  | succ a ih =>
      intro b offset
      show chunkSeg r offset rb (a + 1 + b) = _
      rw [show a + 1 + b = (a + b) + 1 by omega]
      show segList r offset rb :: chunkSeg r (offset + rb) rb (a + b) = _
      rw [ih b (offset + rb)]
      show segList r offset rb ::
        (chunkSeg r (offset + rb) rb a ++
          chunkSeg r (offset + rb + rb * a) rb b) = _
      rw [show offset + rb + rb * a = offset + rb * (a + 1) by ring]
      rfl


/-- **The block sample reads consecutive chunks.** -/
theorem blockTernaryEquiv_leaves (rb : Nat) (r : List Bool) :
    ∀ (d : Nat) (offset : Nat),
      (sampleLeaves d (blockTernaryEquiv rb d
        (fun j => r.getD (offset + j.val) false))).map
          BitString.toList =
        chunkSeg r offset rb (3 ^ d) := by
  intro d
  induction d with
  | zero =>
      intro offset
      show [BitString.toList ((Equiv.arrowCongr
        (finCongr (by ring : rb * 3 ^ 0 = rb)) (Equiv.refl Bool))
        (fun j => r.getD (offset + j.val) false))] = _
      show [BitString.toList (fun i : Fin rb =>
        r.getD (offset + ((finCongr
          (by ring : rb * 3 ^ 0 = rb)).symm i).val) false)] = _
      have harg : (fun i : Fin rb =>
          r.getD (offset + ((finCongr
            (by ring : rb * 3 ^ 0 = rb)).symm i).val) false) =
          fun i : Fin rb => r.getD (offset + i.val) false := by
        funext i
        congr 1
      rw [harg]
      show [List.ofFn (fun i : Fin rb => r.getD (offset + i.val) false)] = _
      rfl
  | succ d ih =>
      intro offset
      set F : BitString (rb * 3 ^ (d + 1)) :=
        fun j => r.getD (offset + j.val) false with hF
      set G : BitString (3 * (rb * 3 ^ d)) :=
        (Equiv.arrowCongr (finCongr (by ring :
          rb * 3 ^ (d + 1) = 3 * (rb * 3 ^ d))) (Equiv.refl Bool)) F with hG
      have hGval : ∀ j : Fin (3 * (rb * 3 ^ d)),
          G j = r.getD (offset + j.val) false := by
        intro j
        show F ((finCongr (by ring :
          rb * 3 ^ (d + 1) = 3 * (rb * 3 ^ d))).symm j) = _
        rw [hF]
        congr 1
      have hb1 : (blockSplit (rb * 3 ^ d) G).1 =
          fun j : Fin (rb * 3 ^ d) => r.getD (offset + j.val) false := by
        funext j
        show G ⟨j.val, by omega⟩ = _
        rw [hGval ⟨j.val, by omega⟩]
      have hb2 : (blockSplit (rb * 3 ^ d) G).2.1 =
          fun j : Fin (rb * 3 ^ d) =>
            r.getD ((offset + rb * 3 ^ d) + j.val) false := by
        funext j
        show G ⟨rb * 3 ^ d + j.val, by omega⟩ = _
        rw [hGval ⟨rb * 3 ^ d + j.val, by omega⟩]
        show r.getD (offset + (rb * 3 ^ d + j.val)) false = _
        congr 1
        omega
      have hb3 : (blockSplit (rb * 3 ^ d) G).2.2 =
          fun j : Fin (rb * 3 ^ d) =>
            r.getD ((offset + 2 * (rb * 3 ^ d)) + j.val) false := by
        funext j
        show G ⟨2 * (rb * 3 ^ d) + j.val, by omega⟩ = _
        rw [hGval ⟨2 * (rb * 3 ^ d) + j.val, by omega⟩]
        show r.getD (offset + (2 * (rb * 3 ^ d) + j.val)) false = _
        congr 1
        omega
      show (sampleLeaves (d + 1)
        ((Equiv.prodCongr (blockTernaryEquiv rb d)
          (Equiv.prodCongr (blockTernaryEquiv rb d)
            (blockTernaryEquiv rb d)))
          (blockSplit (rb * 3 ^ d) G))).map BitString.toList = _
      show ((sampleLeaves d (blockTernaryEquiv rb d
          (blockSplit (rb * 3 ^ d) G).1)) ++
        ((sampleLeaves d (blockTernaryEquiv rb d
          (blockSplit (rb * 3 ^ d) G).2.1)) ++
         (sampleLeaves d (blockTernaryEquiv rb d
          (blockSplit (rb * 3 ^ d) G).2.2)))).map BitString.toList = _
      rw [List.map_append, List.map_append, hb1, hb2, hb3,
        ih offset, ih (offset + rb * 3 ^ d),
        ih (offset + 2 * (rb * 3 ^ d))]
      rw [show (3:Nat) ^ (d + 1) = 3 ^ d + (3 ^ d + 3 ^ d) by ring]
      rw [chunkSeg_append r rb (3 ^ d) (3 ^ d + 3 ^ d) offset,
        chunkSeg_append r rb (3 ^ d) (3 ^ d) (offset + rb * 3 ^ d)]
      rw [show offset + rb * 3 ^ d + rb * 3 ^ d =
        offset + 2 * (rb * 3 ^ d) by ring]

end SipserGacsLautemann