import Init

def OA_statement : Prop := (∀ (Row : Type) (leftRank rightRank actor sequence : Row → Nat),
(fun (keyBefore : Row → Row → Bool) =>
(fun (literalScan : Row → List Row → Nat → Bool → Nat → Nat) =>
(fun (stopPredicate : Row → Row → Bool) =>
(fun (clearPredicate : Row → Row → Bool) =>
(fun (startPredicate : Row → Row → Bool) =>
(fun (firstStop : Row → List Row → Nat) =>
(fun (lastClearBeforeStop : Row → List Row → Option Nat) =>
(fun (firstStartAfterClear : Row → List Row → Option Nat) =>
(fun (selectedDestination : Row → List Row → Nat → Nat) =>
∀ (incoming : Row) (rows : List Row) (position : Nat), literalScan incoming rows position false position = selectedDestination incoming rows position
) (fun incoming rows position => position + (firstStartAfterClear incoming rows).getD (firstStop incoming rows))
) (fun incoming rows =>
  ((((rows.take (firstStop incoming rows)).zipIdx).drop (((lastClearBeforeStop incoming rows).map Nat.succ).getD 0)).find? (fun pair => startPredicate incoming pair.1)).map Prod.snd)
) (fun incoming rows => ((((rows.take (firstStop incoming rows)).zipIdx).reverse.find?
    (fun pair => clearPredicate incoming pair.1)).map Prod.snd))
) (fun incoming rows => (((rows.zipIdx).find? (fun pair => stopPredicate incoming pair.1)).map
    Prod.snd).getD rows.length)
) (fun incoming other => decide ((leftRank other) = (leftRank incoming) ∧
    (rightRank other) < (rightRank incoming)))
) (fun incoming other => decide ((leftRank other) = (leftRank incoming) ∧
    (rightRank incoming) ≤ (rightRank other)))
) (fun incoming other => decide ((leftRank other) < (leftRank incoming)) ||
    (decide ((leftRank other) = (leftRank incoming) ∧
      (rightRank other) = (rightRank incoming)) && keyBefore incoming other))
) (fun incoming rows => List.foldr (fun other tail position scanning back =>
  if (leftRank other) = (leftRank incoming) then
        if (rightRank other) = (rightRank incoming) then
          if keyBefore incoming other then
            if scanning then back else position
          else tail (position + 1) false back
        else if (rightRank other) < (rightRank incoming) then
          tail (position + 1) true
            (if scanning then back else position)
        else tail (position + 1) false back
      else if (leftRank other) < (leftRank incoming) then
        if scanning then back else position
      else tail (position + 1) scanning back) (fun position scanning back => if scanning then back else position) rows)
) (fun incoming other => decide (actor incoming < actor other ∨ (actor incoming = actor other ∧ sequence incoming < sequence other))))

theorem OA_target : OA_statement :=
  by
    intro Row leftRank rightRank actor sequence
    let keyBefore : Row → Row → Bool := fun incoming other => decide (actor incoming < actor other ∨ (actor incoming = actor other ∧ sequence incoming < sequence other))
    let literalScan : Row → List Row → Nat → Bool → Nat → Nat := fun incoming rows => List.foldr (fun other tail position scanning back =>
      if (leftRank other) = (leftRank incoming) then
            if (rightRank other) = (rightRank incoming) then
              if keyBefore incoming other then
                if scanning then back else position
              else tail (position + 1) false back
            else if (rightRank other) < (rightRank incoming) then
              tail (position + 1) true
                (if scanning then back else position)
            else tail (position + 1) false back
          else if (leftRank other) < (leftRank incoming) then
            if scanning then back else position
          else tail (position + 1) scanning back) (fun position scanning back => if scanning then back else position) rows
    let stopPredicate : Row → Row → Bool := fun incoming other => decide ((leftRank other) < (leftRank incoming)) ||
        (decide ((leftRank other) = (leftRank incoming) ∧
          (rightRank other) = (rightRank incoming)) && keyBefore incoming other)
    let clearPredicate : Row → Row → Bool := fun incoming other => decide ((leftRank other) = (leftRank incoming) ∧
        (rightRank incoming) ≤ (rightRank other))
    let startPredicate : Row → Row → Bool := fun incoming other => decide ((leftRank other) = (leftRank incoming) ∧
        (rightRank other) < (rightRank incoming))
    let firstStop : Row → List Row → Nat := fun incoming rows => (((rows.zipIdx).find? (fun pair => stopPredicate incoming pair.1)).map
        Prod.snd).getD rows.length
    let lastClearBeforeStop : Row → List Row → Option Nat := fun incoming rows => ((((rows.take (firstStop incoming rows)).zipIdx).reverse.find?
        (fun pair => clearPredicate incoming pair.1)).map Prod.snd)
    let firstStartAfterClear : Row → List Row → Option Nat := fun incoming rows =>
      ((((rows.take (firstStop incoming rows)).zipIdx).drop (((lastClearBeforeStop incoming rows).map Nat.succ).getD 0)).find? (fun pair => startPredicate incoming pair.1)).map Prod.snd
    let selectedDestination : Row → List Row → Nat → Nat := fun incoming rows position => position + (firstStartAfterClear incoming rows).getD (firstStop incoming rows)
    change ∀ (incoming : Row) (rows : List Row) (position : Nat),
      literalScan incoming rows position false position = selectedDestination incoming rows position
    have firstStop_cons (incoming other : Row) (rows : List Row) :
        firstStop incoming (other :: rows) =
          if stopPredicate incoming other then 0 else firstStop incoming rows + 1 := by
      unfold firstStop
      cases hs : stopPredicate incoming other <;>
        simp [List.zipIdx_succ, List.find?_map,
          Option.map_map, Function.comp_def, hs]
      cases h : rows.zipIdx.find? (fun pair => stopPredicate incoming pair.1) <;>
        simp [Option.getD]
    
    have active_cons (incoming other : Row) (rows : List Row)
        (hs : stopPredicate incoming other = false) :
        (other :: rows).take (firstStop incoming (other :: rows)) =
          other :: rows.take (firstStop incoming rows) := by
      rw [firstStop_cons]
      simp [hs]
    
    have clear_cons (incoming other : Row) (rows : List Row)
        (hs : stopPredicate incoming other = false) :
        lastClearBeforeStop incoming (other :: rows) =
          ((lastClearBeforeStop incoming rows).map (· + 1)).or
            (if clearPredicate incoming other then some 0 else none) := by
      simp only [lastClearBeforeStop, active_cons incoming other rows hs,
        List.zipIdx_cons', List.reverse_cons, ← List.map_reverse,
        List.find?_append]
      cases hc : clearPredicate incoming other <;>
        simp [-List.map_reverse, List.find?_map, Option.map_map,
          Function.comp_def, Prod.map, hc]
      cases h : (rows.take (firstStop incoming rows)).zipIdx.reverse.find?
          (fun pair => clearPredicate incoming pair.1) <;> simp
    
    have start_cons_none (incoming other : Row) (rows : List Row)
        (hs : stopPredicate incoming other = false)
        (hc : lastClearBeforeStop incoming (other :: rows) = none) :
        firstStartAfterClear incoming (other :: rows) =
          if startPredicate incoming other then some 0 else
            (((rows.take (firstStop incoming rows)).zipIdx.find?
              (fun pair => startPredicate incoming pair.1)).map Prod.snd).map (· + 1) := by
      cases hstart : startPredicate incoming other <;>
        simp [firstStartAfterClear, hc, active_cons incoming other rows hs,
        List.zipIdx_succ, List.find?_map, hstart,
        Option.map_map, Function.comp_def]
    
    have start_cons_zero (incoming other : Row) (rows : List Row)
        (hs : stopPredicate incoming other = false)
        (hc : lastClearBeforeStop incoming (other :: rows) = some 0) :
        firstStartAfterClear incoming (other :: rows) =
          (((rows.take (firstStop incoming rows)).zipIdx.find?
            (fun pair => startPredicate incoming pair.1)).map Prod.snd).map (· + 1) := by
      simp [firstStartAfterClear, hc, active_cons incoming other rows hs,
        List.zipIdx_succ, List.find?_map,
        Option.map_map, Function.comp_def]
    
    have start_cons_succ (incoming other : Row) (rows : List Row) (c : Nat)
        (hs : stopPredicate incoming other = false)
        (hc : lastClearBeforeStop incoming (other :: rows) = some (c + 1)) :
        firstStartAfterClear incoming (other :: rows) =
          ((((rows.take (firstStop incoming rows)).zipIdx.drop (c + 1)).find?
            (fun pair => startPredicate incoming pair.1)).map Prod.snd).map (· + 1) := by
      simp [firstStartAfterClear, hc, active_cons incoming other rows hs,
        List.zipIdx_succ, ← List.map_drop, List.find?_map,
        Option.map_map, Function.comp_def]
    
    
    let selectedWithSaved (incoming : Row) (rows : List Row) (position : Nat)
        (saved : Option Nat) : Nat :=
      let inherited := if (lastClearBeforeStop incoming rows).isSome then none else saved
      (inherited.or ((firstStartAfterClear incoming rows).map (position + ·))).getD
        (position + firstStop incoming rows)
    
    have saved_nil (incoming : Row) (p : Nat) (s : Option Nat) :
        selectedWithSaved incoming [] p s = s.getD p := by
      cases s <;> rfl
    
    have saved_stop (incoming other : Row) (rows : List Row) (p : Nat)
        (s : Option Nat) (hs : stopPredicate incoming other = true) :
        selectedWithSaved incoming (other :: rows) p s = s.getD p := by
      simp [selectedWithSaved, firstStop_cons, hs, lastClearBeforeStop,
        firstStartAfterClear]
    
    have saved_skip (incoming other : Row) (rows : List Row) (p : Nat)
        (s : Option Nat) (hs : stopPredicate incoming other = false)
        (hc : clearPredicate incoming other = false)
        (ht : startPredicate incoming other = false) :
        selectedWithSaved incoming (other :: rows) p s =
          selectedWithSaved incoming rows (p + 1) s := by
      cases htail : lastClearBeforeStop incoming rows with
      | none =>
        have hhead : lastClearBeforeStop incoming (other :: rows) = none := by
          simp [clear_cons incoming other rows hs, htail, hc]
        simp only [selectedWithSaved, hhead, htail, start_cons_none incoming other rows hs hhead]
        simp [firstStartAfterClear, htail, firstStop_cons, hs, ht, Option.map_map,
          Function.comp_def, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm]
      | some c =>
        have hhead : lastClearBeforeStop incoming (other :: rows) = some (c + 1) := by
          simp [clear_cons incoming other rows hs, htail, hc]
        simp only [selectedWithSaved, hhead, htail, start_cons_succ incoming other rows c hs hhead]
        simp [firstStartAfterClear, htail, firstStop_cons, hs, Option.map_map,
          Function.comp_def, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm]
    
    have saved_start (incoming other : Row) (rows : List Row) (p : Nat)
        (s : Option Nat) (hs : stopPredicate incoming other = false)
        (hc : clearPredicate incoming other = false)
        (ht : startPredicate incoming other = true) :
        selectedWithSaved incoming (other :: rows) p s =
          selectedWithSaved incoming rows (p + 1) (some (s.getD p)) := by
      cases htail : lastClearBeforeStop incoming rows with
      | none =>
        have hhead : lastClearBeforeStop incoming (other :: rows) = none := by
          simp [clear_cons incoming other rows hs, htail, hc]
        cases s <;>
          simp only [selectedWithSaved, hhead, htail, start_cons_none incoming other rows hs hhead] <;>
          simp [firstStartAfterClear, htail, firstStop_cons, hs, ht, Option.map_map,
            Function.comp_def, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm]
      | some c =>
        have hhead : lastClearBeforeStop incoming (other :: rows) = some (c + 1) := by
          simp [clear_cons incoming other rows hs, htail, hc]
        simp only [selectedWithSaved, hhead, htail, start_cons_succ incoming other rows c hs hhead] <;>
        simp [firstStartAfterClear, htail, firstStop_cons, hs, Option.map_map,
          Function.comp_def, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm]
    
    have saved_clear (incoming other : Row) (rows : List Row) (p : Nat)
        (s : Option Nat) (hs : stopPredicate incoming other = false)
        (hc : clearPredicate incoming other = true) :
        selectedWithSaved incoming (other :: rows) p s =
          selectedWithSaved incoming rows (p + 1) none := by
      cases htail : lastClearBeforeStop incoming rows with
      | none =>
        have hhead : lastClearBeforeStop incoming (other :: rows) = some 0 := by
          simp [clear_cons incoming other rows hs, htail, hc]
        simp only [selectedWithSaved, hhead, htail, start_cons_zero incoming other rows hs hhead]
        simp [firstStartAfterClear, htail, firstStop_cons, hs, Option.map_map,
          Function.comp_def, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm]
      | some c =>
        have hhead : lastClearBeforeStop incoming (other :: rows) = some (c + 1) := by
          simp [clear_cons incoming other rows hs, htail, hc]
        simp only [selectedWithSaved, hhead, htail, start_cons_succ incoming other rows c hs hhead]
        simp [firstStartAfterClear, htail, firstStop_cons, hs, Option.map_map,
          Function.comp_def, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm]
    
    have literal_equals_saved (incoming : Row) (rows : List Row) (p : Nat)
        (scanning : Bool) (back : Nat) :
        literalScan incoming rows p scanning back =
          selectedWithSaved incoming rows p (if scanning then some back else none) := by
      induction rows generalizing p scanning back with
      | nil => cases scanning <;> simp [literalScan, saved_nil]
      | cons other rows ih =>
        by_cases hl : (leftRank other) = (leftRank incoming)
        · by_cases hr : (rightRank other) = (rightRank incoming)
          · cases hk : keyBefore incoming other
            · have hs : stopPredicate incoming other = false := by
                simp [stopPredicate, hl, hr, hk]
              have hc : clearPredicate incoming other = true := by
                simp [clearPredicate, hl, hr]
              cases scanning <;>
                simp [literalScan, hl, hr, hk, saved_clear incoming other rows p _ hs hc, ih]
            · have hs : stopPredicate incoming other = true := by
                simp [stopPredicate, hl, hr, hk]
              cases scanning <;>
                simp [literalScan, hl, hr, hk, saved_stop incoming other rows p _ hs]
          · by_cases hlt : (rightRank other) < (rightRank incoming)
            · have hs : stopPredicate incoming other = false := by
                simp [stopPredicate, hl, hr]
              have hc : clearPredicate incoming other = false := by
                simp [clearPredicate, hl, Nat.not_le_of_gt hlt]
              have ht : startPredicate incoming other = true := by
                simp [startPredicate, hl, hlt]
              cases scanning <;>
                simp [literalScan, hl, hr, hlt,
                  saved_start incoming other rows p _ hs hc ht, ih]
            · have hs : stopPredicate incoming other = false := by
                simp [stopPredicate, hl, hr]
              have hc : clearPredicate incoming other = true := by
                simp [clearPredicate, hl, Nat.le_of_not_gt hlt]
              cases scanning <;>
                simp [literalScan, hl, hr, hlt, saved_clear incoming other rows p _ hs hc, ih]
        · by_cases hlt : (leftRank other) < (leftRank incoming)
          · have hs : stopPredicate incoming other = true := by
              simp [stopPredicate, hl, hlt]
            cases scanning <;>
              simp [literalScan, hl, hlt, saved_stop incoming other rows p _ hs]
          · have hs : stopPredicate incoming other = false := by
              simp [stopPredicate, hl, hlt]
            have hc : clearPredicate incoming other = false := by simp [clearPredicate, hl]
            have ht : startPredicate incoming other = false := by simp [startPredicate, hl]
            cases scanning <;>
              simp [literalScan, hl, hlt, saved_skip incoming other rows p _ hs hc ht, ih]
    
    have initialized_selection (incoming : Row) (rows : List Row) (p : Nat) :
        selectedWithSaved incoming rows p none = selectedDestination incoming rows p := by
      cases hs : firstStartAfterClear incoming rows <;>
        simp [selectedWithSaved, selectedDestination, hs]
    intro incoming rows position
    rw [literal_equals_saved]
    exact initialized_selection incoming rows position

#print axioms OA_target
#check OA_target