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

namespace Hunch.SemidirectArithmetic
def addEffect : (Int → Int → Int) :=
  fun a x => x + a

def multiplyEffect : (Int → Int → Int) :=
  fun m x => m * x

def transformAdd : (Int → Int → Int) :=
  fun m a => m * a

def transformHistory : (List Int → Int → Int) :=
  fun ms a => ms.foldr (fun m acc => m * acc) a

theorem reordering : (∀ m a x : Int, multiplyEffect m (addEffect a x) = addEffect (transformAdd m a) (multiplyEffect m x)) :=
  by
    intro m a x
    exact Int.mul_add m x a

theorem actions_commute : (∀ m n a : Int, transformAdd m (transformAdd n a) = transformAdd n (transformAdd m a)) :=
  by
    intro m n a
    exact Int.mul_left_comm m n a

theorem action_composition : (∀ m n a : Int, transformAdd (m*n) a = transformAdd m (transformAdd n a)) :=
  by
    intro m n a
    exact Int.mul_assoc m n a

theorem history_permutation : (∀ (xs ys : List Int), List.Perm xs ys → ∀ a : Int, transformHistory xs a = transformHistory ys a) :=
  by
    intro xs ys h
    induction h with
    | nil => intro a; rfl
    | cons m h ih =>
      intro a
      exact congrArg (fun z => m * z) (ih a)
    | swap m n rest =>
      intro a
      exact Int.mul_left_comm n m (transformHistory rest a)
    | trans h1 h2 ih1 ih2 =>
      intro a
      exact (ih1 a).trans (ih2 a)

end Hunch.SemidirectArithmetic

def OA_statement : Prop := ((∀ m a x : Int, Hunch.SemidirectArithmetic.multiplyEffect m (Hunch.SemidirectArithmetic.addEffect a x) = Hunch.SemidirectArithmetic.addEffect (Hunch.SemidirectArithmetic.transformAdd m a) (Hunch.SemidirectArithmetic.multiplyEffect m x)) ∧ (∀ (xs ys : List Int), List.Perm xs ys → ∀ a : Int, Hunch.SemidirectArithmetic.transformHistory xs a = Hunch.SemidirectArithmetic.transformHistory ys a))

theorem OA_target : OA_statement :=
  ⟨Hunch.SemidirectArithmetic.reordering, Hunch.SemidirectArithmetic.history_permutation⟩

#print axioms OA_target
#check OA_target