import Init

def OA_statement : Prop := (∀ (State Op : Type) (step undo : Op → State → Option State),
 (∀ op s t, step op s = some t → undo op t = some s) →
 ∀ (ops : List Op) (s t : State),
 ops.foldl (fun prior op => prior.bind (step op)) (some s) = some t →
 ops.reverse.foldl (fun prior op => prior.bind (undo op)) (some t) = some s)

theorem OA_target : OA_statement :=
  by
    intro State Op step undo inverse
    have failure : ∀ (ops : List Op), ops.foldl (fun prior op => prior.bind (step op)) none = none := by
      intro ops
      induction ops with
      | nil => rfl
      | cons op ops ih => simpa only [List.foldl_cons, Option.bind_none] using ih
    intro ops
    induction ops with
    | nil =>
      intro s t h
      simpa only [List.foldl_nil, List.reverse_nil] using h.symm
    | cons op ops ih =>
      intro s t h
      change ops.foldl (fun prior op => prior.bind (step op)) (step op s) = some t at h
      cases first : step op s with
      | none =>
        rw [first, failure] at h
        cases h
      | some mid =>
        have tail := ih mid t (by simpa only [first] using h)
        simp only [List.reverse_cons, List.foldl_append, List.foldl_cons, List.foldl_nil]
        rw [tail]
        exact inverse op s mid first

#print axioms OA_target
#check OA_target