import Init

def OA_statement : Prop := ((fun (indexOf : (Nat×Nat)→(List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→Option Nat) =>
(fun (leftAfter : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→Option (Nat×Nat)→Except Nat Nat) =>
(fun (rightBefore : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→Option (Nat×Nat)→Except Nat Nat) =>
(fun (idBefore : (Nat×Nat)→(Nat×Nat)→Bool) =>
(fun (scan : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))→Nat→Nat→Nat→Nat→Bool→Nat→Except Nat Nat) =>
(fun (insert : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))→Except Nat (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))) =>
(fun (apply : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))→Except Nat (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))) =>
(fun (visible : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→(List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))) =>
(fun (generate : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→(Nat×Nat)→(Sum (Nat×(Nat×Nat)×Nat) Nat)→Except Nat (Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))) =>
(fun (replayOps : List (Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))→(List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→Except Nat (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))) =>
(fun (replay : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))→Except Nat (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))) =>
(fun (ids : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))→List (Nat×Nat)) =>
(fun (validExtension : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))→((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat)))→Prop) =>
(fun (validHistory : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))→Prop) =>
(fun (reconstruct : List (Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))→(List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))→(List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))) =>
(fun (parentContext : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))→((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat)))→(List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))) =>
∀ (history : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat))))) (finalState : (List (((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat))×Bool))),
validHistory history→replay history = .ok finalState→∀ (event : ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat)))), event ∈ history→replay (parentContext history event) =
.ok (reconstruct ((parentContext history event).map (fun e => e.2.2.2)) finalState)
) (fun history event =>
history.filter (fun previous => event.2.1.any (fun id => id == previous.1)))
) (fun ops finalState =>
(fun (born dead : List (Nat×Nat)) =>
(finalState.filter (fun item => born.any (fun id => id == item.1.1))).map
(fun item => (item.1, dead.any (fun id => id == item.1.1))))
(ops.filterMap (fun op => match op with | .inl ins => some ins.1 | .inr _ => none))
(ops.filterMap (fun op => match op with | .inl _ => none | .inr target => some target)))
) (fun history =>
List.rec (fun _ : (List ((Nat×Nat)×List (Nat×Nat)×(Sum (Nat×(Nat×Nat)×Nat) Nat)×(Sum ((Nat×Nat)×(Nat×Nat)×Nat×Option (Nat×Nat)×Option (Nat×Nat)) (Nat×Nat)))) => True)
(fun event _ rest pre => validExtension pre event ∧ rest (pre ++ [event])) history [])
) (fun pre event =>
event.1 ∉ ids pre ∧
(∀ id ∈ event.2.1, id ∈ ids pre) ∧
(∀ previous ∈ pre, previous.1 ∈ event.2.1→∀ id ∈ previous.2.1, id ∈ event.2.1) ∧
(∀ previous ∈ pre, previous.1.1 = event.1.1→previous.1.2 < event.1.2 ∧ previous.1 ∈ event.2.1) ∧
∃ sourceState,
replay (pre.filter (fun previous => event.2.1.any (fun id => id == previous.1))) = .ok sourceState ∧
generate sourceState event.1 event.2.2.1 = .ok event.2.2.2)
) (fun history => history.map (fun event => event.1))
) (fun history =>
replayOps (history.map (fun event => event.2.2.2)) [])
) (fun ops start =>
ops.foldl (fun prior op => prior.bind (fun state => apply state op)) (.ok start))
) (fun state fresh edit =>
match edit with
| .inl (pos, label, payload) => do
if (visible state).length < pos then throw 4
(fun (left : Option (Nat×Nat)) => do
let start ← leftAfter state left
return .inl (fresh, label, payload, left, (state[start]?).map (fun x => x.1.1))) (if pos = 0 then none else ((visible state)[pos - 1]?).map (fun x => x.1.1))
| .inr pos => match (visible state)[pos]? with
| none => .error 4
| some item => .ok (.inr item.1.1))
) (fun state => state.filter (fun item => !item.2))
) (fun state op =>
match op with
| .inl ins => insert state ins
| .inr target =>
if (indexOf target state).isSome then
.ok (state.map fun item => if item.1.1 = target then (item.1, true) else item)
else .error 3)
) (fun state ins => do
if (indexOf ins.1 state).isSome then throw 1
let left ← leftAfter state ins.2.2.2.1
let right ← rightBefore state ins.2.2.2.2
if right < left then throw 2
let dest ← scan state ins left right state.length left false left
return state.take dest ++ [(ins, false)] ++ state.drop dest)
) (fun state ins left right fuel =>
Nat.rec
(fun i scanning back =>
if right ≤ i then .ok (if scanning then back else i) else .error 5)
(fun _ recur i scanning back => do
if right ≤ i then return if scanning then back else i
let other ← match state[i]? with
| none => .error 4
| some item => .ok item
if other.1.2.2.2.1 = ins.2.2.2.1 then
if other.1.2.2.2.2 = ins.2.2.2.2 then
if idBefore ins.1 other.1.1 then return if scanning then back else i
else recur (i + 1) false back
else
let otherRight ← rightBefore state other.1.2.2.2.2
if otherRight < right then recur (i + 1) true (if scanning then back else i)
else recur (i + 1) false back
else
let otherLeft ← leftAfter state other.1.2.2.2.1
if otherLeft < left then return if scanning then back else i
else recur (i + 1) scanning back)
fuel)
) (fun a b =>
a.1 < b.1 || (a.1 == b.1 && a.2 < b.2))
) (fun state origin =>
match origin with
| none => .ok state.length
| some id => match indexOf id state with
| none => .error 0
| some i => .ok i)
) (fun state origin =>
match origin with
| none => .ok 0
| some id => match indexOf id state with
| none => .error 0
| some i => .ok (i + 1))
) (fun id state =>
List.rec none (fun item _ tail => if item.1.1 = id then some 0 else tail.map Nat.succ) state))

theorem OA_target : OA_statement :=
  by
    have hAnyFalse : ∀ (α : Type) (xs : List α), xs.any (fun _ => false) = false := by
      intro α xs
      induction xs with
      | nil => rfl
      | cons a xs ih => simp [List.any_cons, ih]
    have hFilterFalse : ∀ (α : Type) (xs : List α), xs.filter (fun _ => false) = [] := by
      intro α xs
      induction xs with
      | nil => rfl
      | cons a xs ih => simp [ih]
    dsimp only [OA_statement]
    intro history finalState hValid hReplay event hMem
    by_cases hEmpty : event.2.1 = []
    · simp [hEmpty, hAnyFalse, hFilterFalse]
    · skip

#print axioms OA_target
#check OA_target