import Init

def OA_statement : Prop := ((fun (cost : List (Sum (Option Nat) (Option Nat)) → Nat) =>
(fun (apply : List (Sum (Option Nat) (Option Nat)) → List Nat → Option (List Nat)) =>
(fun (best : List (Sum (Option Nat) (Option Nat)) → List (Sum (Option Nat) (Option Nat)) → List (Sum (Option Nat) (Option Nat)) → List (Sum (Option Nat) (Option Nat))) =>
(fun (diff : Nat → List Nat → List Nat → List (Sum (Option Nat) (Option Nat))) =>
∀ (xs ys : List Nat) (fuel : Nat), xs.length + ys.length ≤ fuel →
 apply (diff fuel xs ys) xs = some ys ∧
 ∀ script : List (Sum (Option Nat) (Option Nat)), apply script xs = some ys → cost (diff fuel xs ys) ≤ cost script
) (fun fuel => Nat.rec (fun _ _ : List Nat => [])
 (fun _ recur xs ys => match xs, ys with
 | [], _ => ys.map (fun y => Sum.inr (some y))
 | _, [] => List.replicate xs.length (Sum.inr none)
 | x :: xt, y :: yt => if x = y then Sum.inl none :: recur xt yt
   else best (Sum.inl (some y) :: recur xt yt)
             (Sum.inr none :: recur xt ys)
             (Sum.inr (some y) :: recur xs yt)) fuel)
) (fun a b c => if cost a ≤ cost b ∧ cost a ≤ cost c then a else if cost b ≤ cost c then b else c)
) (fun script => List.rec (fun xs : List Nat => some xs)
 (fun edit _ rest xs => match edit, xs with
 | .inl none, x :: xt => (rest xt).map (fun ys => x :: ys)
 | .inl (some y), _ :: xt => (rest xt).map (fun ys => y :: ys)
 | .inr none, _ :: xt => rest xt
 | .inr (some y), _ => (rest xs).map (fun ys => y :: ys)
 | _, [] => none) script)
) (fun script => script.foldr (fun edit n => match edit with | .inl none => n | _ => n + 1) 0))

theorem OA_target : OA_statement :=
  by
  
    have main : ∀ (cost : List (Sum (Option Nat) (Option Nat)) → Nat)
        (apply : List (Sum (Option Nat) (Option Nat)) → List Nat → Option (List Nat))
        (best : List (Sum (Option Nat) (Option Nat)) → List (Sum (Option Nat) (Option Nat)) → List (Sum (Option Nat) (Option Nat)) → List (Sum (Option Nat) (Option Nat)))
        (diff : Nat → List Nat → List Nat → List (Sum (Option Nat) (Option Nat))),
        cost [] = 0 →
        (∀ s, cost (Sum.inl none :: s) = cost s) →
        (∀ y s, cost (Sum.inl (some y) :: s) = cost s + 1) →
        (∀ s, cost (Sum.inr none :: s) = cost s + 1) →
        (∀ y s, cost (Sum.inr (some y) :: s) = cost s + 1) →
        (∀ xs, apply [] xs = some xs) →
        (∀ s x xt, apply (Sum.inl none :: s) (x :: xt) = (apply s xt).map (fun ys => x :: ys)) →
        (∀ s y x xt, apply (Sum.inl (some y) :: s) (x :: xt) = (apply s xt).map (fun ys => y :: ys)) →
        (∀ s x xt, apply (Sum.inr none :: s) (x :: xt) = apply s xt) →
        (∀ s y xs, apply (Sum.inr (some y) :: s) xs = (apply s xs).map (fun ys => y :: ys)) →
        (∀ s, apply (Sum.inl none :: s) [] = none) →
        (∀ s y, apply (Sum.inl (some y) :: s) [] = none) →
        (∀ s, apply (Sum.inr none :: s) [] = none) →
        (∀ a b c, best a b c = if cost a ≤ cost b ∧ cost a ≤ cost c then a else if cost b ≤ cost c then b else c) →
        (∀ a b, diff 0 a b = []) →
        (∀ f ys, diff (f + 1) [] ys = ys.map (fun y => Sum.inr (some y))) →
        (∀ f x xt, diff (f + 1) (x :: xt) [] = List.replicate (xt.length + 1) (Sum.inr none)) →
        (∀ f x xt y yt, diff (f + 1) (x :: xt) (y :: yt) =
          if x = y then Sum.inl none :: diff f xt yt
          else best (Sum.inl (some y) :: diff f xt yt) (Sum.inr none :: diff f xt (y :: yt)) (Sum.inr (some y) :: diff f (x :: xt) yt)) →
        ∀ (xs ys : List Nat) (fuel : Nat), xs.length + ys.length ≤ fuel →
          apply (diff fuel xs ys) xs = some ys ∧
          ∀ script, apply script xs = some ys → cost (diff fuel xs ys) ≤ cost script := by
      intro cost apply best diff hc0 hc1 hc2 hc3 hc4 ha0 ha1 ha2 ha3 ha4 ha5 ha5' ha6 hb hd0 hd1 hd2 hd3
      have bestFacts : ∀ a b c,
          (cost (best a b c) ≤ cost a ∧ cost (best a b c) ≤ cost b ∧ cost (best a b c) ≤ cost c) ∧
          (best a b c = a ∨ best a b c = b ∨ best a b c = c) := by
        intro a b c
        rw [hb]
        split
        next h1 => exact ⟨⟨Nat.le_refl _, h1.1, h1.2⟩, Or.inl rfl⟩
        next h1 =>
          split
          next h2 => exact ⟨⟨by omega, Nat.le_refl _, h2⟩, Or.inr (Or.inl rfl)⟩
          next h2 => exact ⟨⟨by omega, by omega, Nat.le_refl _⟩, Or.inr (Or.inr rfl)⟩
      have FI : ∀ f g a b, a.length + b.length ≤ f → a.length + b.length ≤ g → diff f a b = diff g a b := by
        intro f
        induction f with
        | zero =>
          intro g a b hf hg
          have ha : a = [] := List.eq_nil_of_length_eq_zero (by omega)
          have hb' : b = [] := List.eq_nil_of_length_eq_zero (by omega)
          subst ha
          subst hb'
          cases g with
          | zero => rfl
          | succ g => rw [hd0, hd1]; rfl
        | succ f ih =>
          intro g a b hf hg
          cases g with
          | zero =>
            have ha : a = [] := List.eq_nil_of_length_eq_zero (by omega)
            have hb' : b = [] := List.eq_nil_of_length_eq_zero (by omega)
            subst ha
            subst hb'
            rw [hd0, hd1]
            rfl
          | succ g =>
            cases a with
            | nil => rw [hd1, hd1]
            | cons x xt =>
              cases b with
              | nil => rw [hd2, hd2]
              | cons y yt =>
                simp only [List.length_cons] at hf hg
                rw [hd3, hd3, ih g xt yt (by omega) (by omega),
                  ih g xt (y :: yt) (by simp only [List.length_cons]; omega) (by simp only [List.length_cons]; omega),
                  ih g (x :: xt) yt (by simp only [List.length_cons]; omega) (by simp only [List.length_cons]; omega)]
      have insApply : ∀ (b xs : List Nat), apply (b.map (fun y => Sum.inr (some y))) xs = some (b ++ xs) := by
        intro b xs
        induction b with
        | nil => exact ha0 xs
        | cons y bt ih =>
          rw [List.map_cons, ha4, ih]
          rfl
      have delApply : ∀ (l : List Nat), apply (List.replicate l.length (Sum.inr none)) l = some [] := by
        intro l
        induction l with
        | nil => exact ha0 []
        | cons x xt ih =>
          show apply (Sum.inr none :: List.replicate xt.length (Sum.inr none)) (x :: xt) = some []
          rw [ha3, ih]
      have insCost : ∀ (b : List Nat), cost (b.map (fun y => Sum.inr (some y))) = b.length := by
        intro b
        induction b with
        | nil => exact hc0
        | cons y bt ih =>
          rw [List.map_cons, hc4, ih]
          rfl
      have delCost : ∀ n, cost (List.replicate n (Sum.inr none)) = n := by
        intro n
        induction n with
        | zero => exact hc0
        | succ n ih =>
          show cost (Sum.inr none :: List.replicate n (Sum.inr none)) = n + 1
          rw [hc3, ih]
      have CORR : ∀ f a b, a.length + b.length ≤ f → apply (diff f a b) a = some b := by
        intro f
        induction f with
        | zero =>
          intro a b h
          have ha : a = [] := List.eq_nil_of_length_eq_zero (by omega)
          have hb' : b = [] := List.eq_nil_of_length_eq_zero (by omega)
          subst ha
          subst hb'
          rw [hd0, ha0]
        | succ f ih =>
          intro a b h
          cases a with
          | nil =>
            rw [hd1, insApply, List.append_nil]
          | cons x xt =>
            cases b with
            | nil =>
              rw [hd2]
              exact delApply (x :: xt)
            | cons y yt =>
              simp only [List.length_cons] at h
              rw [hd3]
              split
              next hxy =>
                subst hxy
                rw [ha1, ih xt yt (by omega)]
                rfl
              next hxy =>
                rcases (bestFacts (Sum.inl (some y) :: diff f xt yt) (Sum.inr none :: diff f xt (y :: yt))
                    (Sum.inr (some y) :: diff f (x :: xt) yt)).2 with e | e | e
                · rw [e, ha2, ih xt yt (by omega)]
                  rfl
                · rw [e, ha3, ih xt (y :: yt) (by simp only [List.length_cons]; omega)]
                · rw [e, ha4, ih (x :: xt) yt (by simp only [List.length_cons]; omega)]
                  rfl
      obtain ⟨D, hD⟩ : ∃ D : List Nat → List Nat → Nat, ∀ f a b, a.length + b.length ≤ f → cost (diff f a b) = D a b :=
        ⟨fun a b => cost (diff (a.length + b.length) a b), fun f a b h => by
          rw [FI f (a.length + b.length) a b h (Nat.le_refl _)]⟩
      have D0 : ∀ b, D [] b = b.length := by
        intro b
        rw [← hD (b.length + 1) [] b (by simp only [List.length_nil]; omega), hd1, insCost]
      have Dnil : ∀ a, D a [] = a.length := by
        intro a
        cases a with
        | nil => rw [D0]
        | cons x xt =>
          rw [← hD (xt.length + 1 + 1) (x :: xt) [] (by simp only [List.length_cons, List.length_nil]; omega), hd2, delCost]
          rfl
      have D2eq : ∀ x xt yt, D (x :: xt) (x :: yt) = D xt yt := by
        intro x xt yt
        rw [← hD (xt.length + yt.length + 1 + 1) (x :: xt) (x :: yt) (by simp only [List.length_cons]; omega), hd3]
        split
        next _ =>
          rw [hc1, hD (xt.length + yt.length + 1) xt yt (by omega)]
        next h => exact absurd rfl h
      have D2ne : ∀ x xt y yt, x ≠ y →
          D (x :: xt) (y :: yt) ≤ D xt yt + 1 ∧ D (x :: xt) (y :: yt) ≤ D xt (y :: yt) + 1 ∧
          D (x :: xt) (y :: yt) ≤ D (x :: xt) yt + 1 ∧
          (D (x :: xt) (y :: yt) = D xt yt + 1 ∨ D (x :: xt) (y :: yt) = D xt (y :: yt) + 1 ∨
            D (x :: xt) (y :: yt) = D (x :: xt) yt + 1) := by
        intro x xt y yt hne
        have hf := hD (xt.length + yt.length + 1 + 1) (x :: xt) (y :: yt) (by simp only [List.length_cons]; omega)
        rw [hd3] at hf
        split at hf
        next h => exact absurd h hne
        next _ =>
          have e1 : cost (Sum.inl (some y) :: diff (xt.length + yt.length + 1) xt yt) = D xt yt + 1 := by
            rw [hc2, hD (xt.length + yt.length + 1) xt yt (by omega)]
          have e2 : cost (Sum.inr none :: diff (xt.length + yt.length + 1) xt (y :: yt)) = D xt (y :: yt) + 1 := by
            rw [hc3, hD (xt.length + yt.length + 1) xt (y :: yt) (by simp only [List.length_cons]; omega)]
          have e3 : cost (Sum.inr (some y) :: diff (xt.length + yt.length + 1) (x :: xt) yt) = D (x :: xt) yt + 1 := by
            rw [hc4, hD (xt.length + yt.length + 1) (x :: xt) yt (by simp only [List.length_cons]; omega)]
          obtain ⟨⟨b1, b2, b3⟩, bc⟩ := bestFacts (Sum.inl (some y) :: diff (xt.length + yt.length + 1) xt yt)
            (Sum.inr none :: diff (xt.length + yt.length + 1) xt (y :: yt))
            (Sum.inr (some y) :: diff (xt.length + yt.length + 1) (x :: xt) yt)
          rw [hf, e1] at b1
          rw [hf, e2] at b2
          rw [hf, e3] at b3
          refine ⟨b1, b2, b3, ?_⟩
          rcases bc with e | e | e
          · rw [e, e1] at hf
            exact Or.inl hf.symm
          · rw [e, e2] at hf
            exact Or.inr (Or.inl hf.symm)
          · rw [e, e3] at hf
            exact Or.inr (Or.inr hf.symm)
      have FOUR : ∀ n a b, a.length + b.length ≤ n → ∀ c,
          D a (c :: b) ≤ D a b + 1 ∧ D (c :: a) b ≤ D a b + 1 ∧
          D a b ≤ D a (c :: b) + 1 ∧ D a b ≤ D (c :: a) b + 1 := by
        intro n
        induction n with
        | zero =>
          intro a b h c
          have ha : a = [] := List.eq_nil_of_length_eq_zero (by omega)
          have hb' : b = [] := List.eq_nil_of_length_eq_zero (by omega)
          subst ha
          subst hb'
          have e1 := D0 [c]
          have e2 := Dnil [c]
          have e3 := D0 []
          simp only [List.length_cons, List.length_nil] at e1 e2 e3
          omega
        | succ n ih =>
          intro a b h c
          refine ⟨?_, ?_, ?_, ?_⟩
          · cases a with
            | nil =>
              have e1 := D0 (c :: b)
              have e2 := D0 b
              simp only [List.length_cons] at e1
              omega
            | cons x at' =>
              cases b with
              | nil =>
                have e1 := Dnil at'
                have e2 := Dnil (x :: at')
                simp only [List.length_cons] at e2
                by_cases hxc : x = c
                · subst hxc
                  rw [D2eq]
                  omega
                · have := (D2ne x at' c [] hxc).1
                  omega
              | cons y bt =>
                simp only [List.length_cons] at h
                by_cases hxc : x = c
                · subst hxc
                  rw [D2eq]
                  exact (ih at' (y :: bt) (by simp only [List.length_cons]; omega) x).2.2.2
                · exact (D2ne x at' c (y :: bt) hxc).2.2.1
          · cases b with
            | nil =>
              have e1 := Dnil (c :: a)
              have e2 := Dnil a
              simp only [List.length_cons] at e1
              omega
            | cons y bt =>
              cases a with
              | nil =>
                have e1 := D0 bt
                have e2 := D0 (y :: bt)
                simp only [List.length_cons] at e2
                by_cases hcy : c = y
                · subst hcy
                  rw [D2eq]
                  omega
                · have := (D2ne c [] y bt hcy).1
                  omega
              | cons x at' =>
                simp only [List.length_cons] at h
                by_cases hcy : c = y
                · subst hcy
                  rw [D2eq]
                  exact (ih (x :: at') bt (by simp only [List.length_cons]; omega) c).2.2.1
                · exact (D2ne c (x :: at') y bt hcy).2.1
          · cases a with
            | nil =>
              have e1 := D0 (c :: b)
              have e2 := D0 b
              simp only [List.length_cons] at e1
              omega
            | cons x at' =>
              cases b with
              | nil =>
                have e1 := Dnil at'
                have e2 := Dnil (x :: at')
                simp only [List.length_cons] at e2
                simp only [List.length_cons, List.length_nil] at h
                by_cases hxc : x = c
                · subst hxc
                  rw [D2eq]
                  omega
                · have i1 := (ih at' [] (by simp only [List.length_nil]; omega) c).2.2.1
                  rcases (D2ne x at' c [] hxc).2.2.2 with e | e | e <;> omega
              | cons y bt =>
                simp only [List.length_cons] at h
                by_cases hxc : x = c
                · subst hxc
                  rw [D2eq]
                  exact (ih at' (y :: bt) (by simp only [List.length_cons]; omega) x).2.1
                · have i1 := (ih at' (y :: bt) (by simp only [List.length_cons]; omega) x).2.1
                  have i2 := (ih at' (y :: bt) (by simp only [List.length_cons]; omega) c).2.2.1
                  rcases (D2ne x at' c (y :: bt) hxc).2.2.2 with e | e | e <;> omega
          · cases b with
            | nil =>
              have e1 := Dnil (c :: a)
              have e2 := Dnil a
              simp only [List.length_cons] at e1
              omega
            | cons y bt =>
              cases a with
              | nil =>
                have e1 := D0 bt
                have e2 := D0 (y :: bt)
                simp only [List.length_cons] at e2
                simp only [List.length_cons, List.length_nil] at h
                by_cases hcy : c = y
                · subst hcy
                  rw [D2eq]
                  omega
                · have i1 := (ih [] bt (by simp only [List.length_nil]; omega) c).2.2.2
                  rcases (D2ne c [] y bt hcy).2.2.2 with e | e | e <;> omega
              | cons x at' =>
                simp only [List.length_cons] at h
                by_cases hcy : c = y
                · subst hcy
                  rw [D2eq]
                  exact (ih (x :: at') bt (by simp only [List.length_cons]; omega) c).1
                · have i1 := (ih (x :: at') bt (by simp only [List.length_cons]; omega) y).1
                  have i2 := (ih (x :: at') bt (by simp only [List.length_cons]; omega) c).2.2.2
                  rcases (D2ne c (x :: at') y bt hcy).2.2.2 with e | e | e <;> omega
      have Drefl : ∀ a, D a a = 0 := by
        intro a
        induction a with
        | nil => rw [D0]; rfl
        | cons x xt ih => rw [D2eq, ih]
      have MIN : ∀ s a b, apply s a = some b → D a b ≤ cost s := by
        intro s
        induction s with
        | nil =>
          intro a b h
          rw [ha0] at h
          injection h with h
          subst h
          rw [Drefl]
          exact Nat.zero_le _
        | cons e s ih =>
          intro a b h
          rcases e with o | o <;> rcases o with _ | y
          · cases a with
            | nil => rw [ha5] at h; cases h
            | cons x xt =>
              rw [ha1] at h
              rw [hc1]
              rcases hs : apply s xt with _ | b'
              · rw [hs] at h
                cases h
              · rw [hs] at h
                injection h with h
                subst h
                rw [D2eq]
                exact ih xt b' hs
          · cases a with
            | nil => rw [ha5'] at h; cases h
            | cons x xt =>
              rw [ha2] at h
              rw [hc2]
              rcases hs : apply s xt with _ | b'
              · rw [hs] at h
                cases h
              · rw [hs] at h
                injection h with h
                subst h
                dsimp only
                have := ih xt b' hs
                by_cases hxy : x = y
                · subst hxy
                  rw [D2eq]
                  omega
                · have := (D2ne x xt y b' hxy).1
                  omega
          · cases a with
            | nil => rw [ha6] at h; cases h
            | cons x xt =>
              rw [ha3] at h
              rw [hc3]
              have := ih xt b h
              have := (FOUR (xt.length + b.length) xt b (Nat.le_refl _) x).2.1
              omega
          · rw [ha4] at h
            rw [hc4]
            rcases hs : apply s a with _ | b'
            · rw [hs] at h
              cases h
            · rw [hs] at h
              injection h with h
              subst h
              dsimp only
              have := ih a b' hs
              have := (FOUR (a.length + b'.length) a b' (Nat.le_refl _) y).1
              omega
      intro xs ys fuel hfuel
      refine ⟨CORR fuel xs ys hfuel, ?_⟩
      intro script hs
      rw [hD fuel xs ys hfuel]
      exact MIN script xs ys hs
    dsimp only [OA_statement]
    exact main _ _ _ _ rfl (fun _ => rfl) (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
      (fun _ => rfl) (fun _ _ _ => rfl) (fun _ _ _ _ => rfl) (fun _ _ _ => rfl) (fun _ _ _ => rfl)
      (fun _ => rfl) (fun _ _ => rfl) (fun _ => rfl) (fun _ _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl)
      (fun _ _ _ => rfl) (fun _ _ _ _ _ => rfl)

#print axioms OA_target
#check OA_target