{"version":3,"kind":"module","module":{"id":3,"user_id":"cef483b5-8f5a-40e6-b0b3-f82d7a8be13a","title":"Weidner semidirect add/multiply: reordering and history permutation","namespace":"SemidirectArithmetic","description":"Unbounded integer reference model for the add/multiply example in Composing and Decomposing Op-Based CRDTs with Semidirect Products. Proves transformed-add reordering, commuting multiply actions, action composition, and invariance of transformation under any permutation of multiplication messages. Does not model causal delivery, author metadata, duplicate suppression, reset, general semidirect-product correctness, or JavaScript floating-point arithmetic.","profile":"std","declarations":[{"kind":"definition","name":"addEffect","type":"Int → Int → Int","value":"fun a x => x + a"},{"kind":"definition","name":"multiplyEffect","type":"Int → Int → Int","value":"fun m x => m * x"},{"kind":"definition","name":"transformAdd","type":"Int → Int → Int","value":"fun m a => m * a"},{"kind":"definition","name":"transformHistory","type":"List Int → Int → Int","value":"fun ms a => ms.foldr (fun m acc => m * acc) a"},{"kind":"lemma","name":"reordering","type":"∀ m a x : Int, multiplyEffect m (addEffect a x) = addEffect (transformAdd m a) (multiplyEffect m x)","value":"by\n  intro m a x\n  exact Int.mul_add m x a"},{"kind":"lemma","name":"actions_commute","type":"∀ m n a : Int, transformAdd m (transformAdd n a) = transformAdd n (transformAdd m a)","value":"by\n  intro m n a\n  exact Int.mul_left_comm m n a"},{"kind":"lemma","name":"action_composition","type":"∀ m n a : Int, transformAdd (m*n) a = transformAdd m (transformAdd n a)","value":"by\n  intro m n a\n  exact Int.mul_assoc m n a"},{"kind":"lemma","name":"history_permutation","type":"∀ (xs ys : List Int), List.Perm xs ys → ∀ a : Int, transformHistory xs a = transformHistory ys a","value":"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)"}],"module_pins":[],"module_context":[],"module_hash":"150ecbd7daaa885e0a25599b4b57955654f32f8cd6a2a4d39585ed0e09db66e9","status":"verified","check_log":"'_private.0.Hunch.SemidirectArithmetic.addEffect' does not depend on any axioms\n'_private.0.Hunch.SemidirectArithmetic.multiplyEffect' does not depend on any axioms\n'_private.0.Hunch.SemidirectArithmetic.transformAdd' does not depend on any axioms\n'_private.0.Hunch.SemidirectArithmetic.transformHistory' does not depend on any axioms\n'_private.0.Hunch.SemidirectArithmetic.reordering' depends on axioms: [propext]\n'_private.0.Hunch.SemidirectArithmetic.actions_commute' depends on axioms: [propext]\n'_private.0.Hunch.SemidirectArithmetic.action_composition' depends on axioms: [propext]\n'_private.0.Hunch.SemidirectArithmetic.history_permutation' depends on axioms: [propext]\n'_private.0.OA_target' does not depend on any axioms\nOA_target : OA_statement","axioms":["propext"],"created_at":1791446137,"checked_at":1791446161,"hidden_at":null,"secondary_status":"not_run","secondary_details":null,"origin_submission_id":null,"origin_source_hash":null},"problem":{"statement":"True","profile":"std","module_context":[],"module_pins":[],"module_declarations":[{"kind":"definition","name":"addEffect","type":"Int → Int → Int","value":"fun a x => x + a"},{"kind":"definition","name":"multiplyEffect","type":"Int → Int → Int","value":"fun m x => m * x"},{"kind":"definition","name":"transformAdd","type":"Int → Int → Int","value":"fun m a => m * a"},{"kind":"definition","name":"transformHistory","type":"List Int → Int → Int","value":"fun ms a => ms.foldr (fun m acc => m * acc) a"},{"kind":"lemma","name":"reordering","type":"∀ m a x : Int, multiplyEffect m (addEffect a x) = addEffect (transformAdd m a) (multiplyEffect m x)","value":"by\n  intro m a x\n  exact Int.mul_add m x a"},{"kind":"lemma","name":"actions_commute","type":"∀ m n a : Int, transformAdd m (transformAdd n a) = transformAdd n (transformAdd m a)","value":"by\n  intro m n a\n  exact Int.mul_left_comm m n a"},{"kind":"lemma","name":"action_composition","type":"∀ m n a : Int, transformAdd (m*n) a = transformAdd m (transformAdd n a)","value":"by\n  intro m n a\n  exact Int.mul_assoc m n a"},{"kind":"lemma","name":"history_permutation","type":"∀ (xs ys : List Int), List.Perm xs ys → ∀ a : Int, transformHistory xs a = transformHistory ys a","value":"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)"}],"namespace":"SemidirectArithmetic"},"profile":"std","policy":"oa-lean-v1","lean_commit":"62b6a2291302d4bbeace37642a066b7510d0145c","proof":"by trivial","statement_hash":"494cd5346575cc8ca180c5212480b7f23c5adefc25326303724bc72576e2df9d","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 := (True)\n\ntheorem OA_target : OA_statement :=\n  by trivial\n\n#print axioms Hunch.SemidirectArithmetic.addEffect\n#print axioms Hunch.SemidirectArithmetic.multiplyEffect\n#print axioms Hunch.SemidirectArithmetic.transformAdd\n#print axioms Hunch.SemidirectArithmetic.transformHistory\n#print axioms Hunch.SemidirectArithmetic.reordering\n#print axioms Hunch.SemidirectArithmetic.actions_commute\n#print axioms Hunch.SemidirectArithmetic.action_composition\n#print axioms Hunch.SemidirectArithmetic.history_permutation\n#print axioms OA_target\n#check OA_target\n"}