import Std
import Batteries
import Lean.Elab.Tactic.Omega

namespace Hunch.PositionEncoding
def digitCode : (Nat → Nat) :=
  fun d => if d < 26 then 65 + d else 71 + d

def parseDigit : (Nat → Nat) :=
  fun c => c - (if c ≥ 97 then 71 else 65)

theorem digit_roundtrip : (∀ d : Nat, d < 52 → parseDigit (digitCode d) = d) :=
  by
    intro d hd
    unfold parseDigit digitCode
    split <;> split <;> omega

theorem digit_order : (∀ a b : Nat, a < 52 → b < 52 → (digitCode a < digitCode b ↔ a < b)) :=
  by
    intro a b ha hb
    unfold digitCode
    split <;> split <;> omega

theorem common_prefix : (∀ (stem xs ys : List Nat), List.Lex (· < ·) xs ys → List.Lex (· < ·) (stem ++ xs) (stem ++ ys)) :=
  by
    intro stem xs ys h
    induction stem with
    | nil => exact h
    | cons a stem ih => exact List.Lex.cons ih

theorem suffix_stable : (∀ (xs ys leftTail rightTail : List Nat), List.Lex (· < ·) xs ys → (¬ ∃ tail : List Nat, ys = xs ++ tail) → List.Lex (· < ·) (xs ++ leftTail) (ys ++ rightTail)) :=
  by
    intro xs ys leftTail rightTail h
    induction h with
    | nil =>
      intro hn
      exact False.elim (hn ⟨_, rfl⟩)
    | rel hab =>
      intro _
      exact List.Lex.rel hab
    | cons h ih =>
      intro hn
      apply List.Lex.cons
      apply ih
      intro hp
      obtain ⟨tail, eq⟩ := hp
      apply hn
      exact ⟨tail, congrArg (List.cons _) eq⟩

theorem run_separation : (∀ (stem leftLabel rightLabel leftRun rightRun : List Nat), List.Lex (· < ·) leftLabel rightLabel → (¬ ∃ tail : List Nat, rightLabel = leftLabel ++ tail) → List.Lex (· < ·) (stem ++ (leftLabel ++ leftRun)) (stem ++ (rightLabel ++ rightRun))) :=
  by
    intro stem leftLabel rightLabel leftRun rightRun h hn
    exact common_prefix stem _ _ (suffix_stable _ _ _ _ h hn)

theorem side_bracketing : (∀ (stem tail : List Nat) (n : Nat), List.Lex (· < ·) (stem ++ (2*n :: tail)) (stem ++ [2*n+1]) ∧ List.Lex (· < ·) (stem ++ [2*n+1]) (stem ++ ((2*n+1) :: (0 :: tail)))) :=
  by
    intro stem tail n
    constructor
    · apply common_prefix
      apply List.Lex.rel
      omega
    · apply common_prefix
      exact List.Lex.cons List.Lex.nil

end Hunch.PositionEncoding

def OA_statement : Prop := (∀ (stem leftLabel rightLabel leftRun rightRun : List Nat), List.Lex (· < ·) leftLabel rightLabel → (¬ ∃ tail : List Nat, rightLabel = leftLabel ++ tail) → List.Lex (· < ·) (stem ++ (leftLabel ++ leftRun)) (stem ++ (rightLabel ++ rightRun)))

theorem OA_target : OA_statement :=
  Hunch.PositionEncoding.run_separation

#print axioms OA_target
#check OA_target