{"action":"closed","issue":{"url":"https://api.github.com/repos/UniMath/UniMath/issues/187","labels_url":"https://api.github.com/repos/UniMath/UniMath/issues/187/labels{/name}","comments_url":"https://api.github.com/repos/UniMath/UniMath/issues/187/comments","events_url":"https://api.github.com/repos/UniMath/UniMath/issues/187/events","html_url":"https://github.com/UniMath/UniMath/issues/187","id":111009237,"number":187,"title":"associativity of existing operations","user":{"login":"DanGrayson","id":700228,"avatar_url":"https://avatars.githubusercontent.com/u/700228?v=3","gravatar_id":"","url":"https://api.github.com/users/DanGrayson","html_url":"https://github.com/DanGrayson","followers_url":"https://api.github.com/users/DanGrayson/followers","following_url":"https://api.github.com/users/DanGrayson/following{/other_user}","gists_url":"https://api.github.com/users/DanGrayson/gists{/gist_id}","starred_url":"https://api.github.com/users/DanGrayson/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/DanGrayson/subscriptions","organizations_url":"https://api.github.com/users/DanGrayson/orgs","repos_url":"https://api.github.com/users/DanGrayson/repos","events_url":"https://api.github.com/users/DanGrayson/events{/privacy}","received_events_url":"https://api.github.com/users/DanGrayson/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":{"login":"DanGrayson","id":700228,"avatar_url":"https://avatars.githubusercontent.com/u/700228?v=3","gravatar_id":"","url":"https://api.github.com/users/DanGrayson","html_url":"https://github.com/DanGrayson","followers_url":"https://api.github.com/users/DanGrayson/followers","following_url":"https://api.github.com/users/DanGrayson/following{/other_user}","gists_url":"https://api.github.com/users/DanGrayson/gists{/gist_id}","starred_url":"https://api.github.com/users/DanGrayson/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/DanGrayson/subscriptions","organizations_url":"https://api.github.com/users/DanGrayson/orgs","repos_url":"https://api.github.com/users/DanGrayson/repos","events_url":"https://api.github.com/users/DanGrayson/events{/privacy}","received_events_url":"https://api.github.com/users/DanGrayson/received_events","type":"User","site_admin":false},"milestone":null,"comments":5,"created_at":"2015-10-12T16:23:45Z","updated_at":"2015-10-15T14:13:05Z","closed_at":"2015-10-15T14:13:05Z","body":"It turns out nicely that stnsum, stnprod, and my product operation in a monoid\r\nover a finite sequence are all left associative, and that the parser is left\r\nassociative for ```+``` and ```*```.  But, Nat.mul defines the product\r\n```m*n``` as a right associated sum of copies of n!  One result is that ```1*m```\r\ndoes not reduce to m, and it's important for it to do so, because stnprod\r\nactually returns not ```a*b*c*d``` but ```1*a*b*c*d``` -- the induction starts\r\nwith the empty product.  Similarly, stnsum starts its induction with an empty\r\nsum, but luckily ```0+m``` reduces to m.\r\n\r\nWe can fix this (see code below), but then a lot of proofs that Vladimir and I\r\ndid for natural numbers have to be changed.\r\n\r\nAnother idea would be to change the code for stnsum and stnprod so they treat\r\nsequences of length 1 as a special case, enabling stnprod to return\r\n```a*b*c*d```, which is intuitively what people expect, anyway.  But then\r\ntheorems proving things about stnsum and stnprod by induction will have to be\r\nchanged, to do a similar double induction.\r\n\r\nDiscussion?\r\n\r\nHere is demo code.\r\n\r\n```\r\n(* confirm and repair some aspects of operations on [nat] *)\r\n\r\nGoal ∀ n, 0+n = n.\r\nProof. reflexivity. Defined.\r\n\r\nGoal ∀ n, n+0 = n.\r\nProof. try reflexivity. Abort.\r\n\r\nGoal ∀ n, n*0 = 0.\r\nProof. try reflexivity. Abort.\r\n\r\nGoal ∀ n, 0*n = 0.\r\nProof. reflexivity. Defined.\r\n\r\nGoal ∀ n, n*1 = n.\r\nProof. try reflexivity. Abort.\r\n\r\nGoal ∀ n, 1*n = n.\r\nProof. try reflexivity. Abort.\r\n\r\n(* That failure is not good, and Nat.mul defines multiplication as a right-associative sum,\r\n   whereas the parser treats \"+\" and \"*\" as left associative.  \r\n   We redefine multiplication in nat here. *)\r\n\r\nFixpoint mul n m := match n with | 0 => 0 | S p => p * m + m end\r\n                    where \"n * m\" := (mul n m) : nat_scope.\r\n\r\n(* make sure we didn't spoil anything else *)\r\n\r\nGoal ∀ n, n*0 = 0.\r\nProof. try reflexivity. Abort.\r\n\r\nGoal ∀ n, 0*n = 0.\r\nProof. reflexivity. Defined.\r\n\r\nGoal ∀ n, n*1 = n.\r\nProof. try reflexivity. Abort.\r\n\r\nGoal ∀ n, 1*n = n.\r\nProof. reflexivity. Defined.\r\n```\r\n\r\nAnd here is Coq's definition:\r\n```\r\nFixpoint mul n m :=\r\n  match n with\r\n  | 0 => 0\r\n  | S p => m + p * m\r\n  end\r\n\r\nwhere \"n * m\" := (mul n m) : nat_scope.\r\n```"}}