{"version":3,"policy":"oa-lean-v1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","profile":"std","imports":["Std","Batteries","Lean.Elab.Tactic.Omega"],"statement_hash":"71cacefe3ca4d1d0022708dec6804efdf1bd68d8398fbe0d361d8acb1386e486","problem":{"id":39,"title":"Weidner semidirect add/multiply: reordering and arbitrary history permutation","description":"Concrete integer building blocks from the semidirect-product CRDT paper: multiplying after adding agrees with adding the transformed amount after multiplying, and transforming an add by any permutation of multiplication messages yields the same result. This does not assert correctness of the general distributed construction or floating-point Collabs implementation.","statement":"(∀ 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)","profile":"std","module_pins":[{"id":3,"hash":"150ecbd7daaa885e0a25599b4b57955654f32f8cd6a2a4d39585ed0e09db66e9"}],"module_context":[{"id":3,"hash":"150ecbd7daaa885e0a25599b4b57955654f32f8cd6a2a4d39585ed0e09db66e9","namespace":"SemidirectArithmetic","source":"namespace Hunch.SemidirectArithmetic\ndef addEffect : (Int → Int → Int) :=\n  fun a x => x + a\n\ndef multiplyEffect : (Int → Int → Int) :=\n  fun m x => m * x\n\ndef transformAdd : (Int → Int → Int) :=\n  fun m a => m * a\n\ndef transformHistory : (List Int → Int → Int) :=\n  fun ms a => ms.foldr (fun m acc => m * acc) a\n\ntheorem reordering : (∀ m a x : Int, multiplyEffect m (addEffect a x) = addEffect (transformAdd m a) (multiplyEffect m x)) :=\n  by\n    intro m a x\n    exact Int.mul_add m x a\n\ntheorem actions_commute : (∀ m n a : Int, transformAdd m (transformAdd n a) = transformAdd n (transformAdd m a)) :=\n  by\n    intro m n a\n    exact Int.mul_left_comm m n a\n\ntheorem action_composition : (∀ m n a : Int, transformAdd (m*n) a = transformAdd m (transformAdd n a)) :=\n  by\n    intro m n a\n    exact Int.mul_assoc m n a\n\ntheorem history_permutation : (∀ (xs ys : List Int), List.Perm xs ys → ∀ a : Int, transformHistory xs a = transformHistory ys a) :=\n  by\n    intro xs ys h\n    induction h with\n    | nil => intro a; rfl\n    | cons m h ih =>\n      intro a\n      exact congrArg (fun z => m * z) (ih a)\n    | swap m n rest =>\n      intro a\n      exact Int.mul_left_comm n m (transformHistory rest a)\n    | trans h1 h2 ih1 ih2 =>\n      intro a\n      exact (ih1 a).trans (ih2 a)\n\nend Hunch.SemidirectArithmetic\n"}],"scope":{"obligations":["merge_commutation"],"assumptions":["Compared multiplication histories are permutations, including equal multiplicities."],"cost_metric":"none","model_scope":"Unbounded integer register and a finite history of multiply actions.","implementation":"","correspondence":"algorithm_model","limitations":["No causal network, author preservation, duplicate suppression or IEEE-754 arithmetic is modeled; these are required for the broader CRDT claim."]}},"source":"import Std\nimport Batteries\nimport Lean.Elab.Tactic.Omega\n\nnamespace Hunch.SemidirectArithmetic\ndef addEffect : (Int → Int → Int) :=\n  fun a x => x + a\n\ndef multiplyEffect : (Int → Int → Int) :=\n  fun m x => m * x\n\ndef transformAdd : (Int → Int → Int) :=\n  fun m a => m * a\n\ndef transformHistory : (List Int → Int → Int) :=\n  fun ms a => ms.foldr (fun m acc => m * acc) a\n\ntheorem reordering : (∀ m a x : Int, multiplyEffect m (addEffect a x) = addEffect (transformAdd m a) (multiplyEffect m x)) :=\n  by\n    intro m a x\n    exact Int.mul_add m x a\n\ntheorem actions_commute : (∀ m n a : Int, transformAdd m (transformAdd n a) = transformAdd n (transformAdd m a)) :=\n  by\n    intro m n a\n    exact Int.mul_left_comm m n a\n\ntheorem action_composition : (∀ m n a : Int, transformAdd (m*n) a = transformAdd m (transformAdd n a)) :=\n  by\n    intro m n a\n    exact Int.mul_assoc m n a\n\ntheorem history_permutation : (∀ (xs ys : List Int), List.Perm xs ys → ∀ a : Int, transformHistory xs a = transformHistory ys a) :=\n  by\n    intro xs ys h\n    induction h with\n    | nil => intro a; rfl\n    | cons m h ih =>\n      intro a\n      exact congrArg (fun z => m * z) (ih a)\n    | swap m n rest =>\n      intro a\n      exact Int.mul_left_comm n m (transformHistory rest a)\n    | trans h1 h2 ih1 ih2 =>\n      intro a\n      exact (ih1 a).trans (ih2 a)\n\nend Hunch.SemidirectArithmetic\n\ndef 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))\n\n#check OA_statement\n","proof":null}