payload: {"action":"opened","issue":{"url":"https://api.github.com/repos/math-comp/math-comp/issues/407","repository_url":"https://api.github.com/repos/math-comp/math-comp","labels_url":"https://api.github.com/repos/math-comp/math-comp/issues/407/labels{/name}","comments_url":"https://api.github.com/repos/math-comp/math-comp/issues/407/comments","events_url":"https://api.github.com/repos/math-comp/math-comp/issues/407/events","html_url":"https://github.com/math-comp/math-comp/issues/407","id":516839890,"node_id":"MDU6SXNzdWU1MTY4Mzk4OTA=","number":407,"title":"Big operators over setoids","user":{"login":"chdoc","id":20443222,"node_id":"MDQ6VXNlcjIwNDQzMjIy","avatar_url":"https://avatars0.githubusercontent.com/u/20443222?v=4","gravatar_id":"","url":"https://api.github.com/users/chdoc","html_url":"https://github.com/chdoc","followers_url":"https://api.github.com/users/chdoc/followers","following_url":"https://api.github.com/users/chdoc/following{/other_user}","gists_url":"https://api.github.com/users/chdoc/gists{/gist_id}","starred_url":"https://api.github.com/users/chdoc/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/chdoc/subscriptions","organizations_url":"https://api.github.com/users/chdoc/orgs","repos_url":"https://api.github.com/users/chdoc/repos","events_url":"https://api.github.com/users/chdoc/events{/privacy}","received_events_url":"https://api.github.com/users/chdoc/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2019-11-03T14:56:54Z","updated_at":"2019-11-03T14:56:54Z","closed_at":null,"author_association":"NONE","body":"In a recent development we used big operators in a context where we only had a (commutative)  monoid up to some equivalence relation. As a consequence, I ended up porting quite a few of the lemmas from `bigop.v` to our setting, including some of the nontrivial ones such as `perm_big`, `reindex_onto` and `partition_big`\r\n\r\nCurrently, our setup is with respect to a `setoid` type structure and a `monoidLaws` class for commutative monoids. \r\n\r\n```coq\r\nStructure setoid := Setoid { car:> Type; eqv: relation car; Eqv: Equivalence eqv }.\r\nInfix \"≡\" := eqv (at level 79).\r\n\r\nClass monoidLaws {X : setoid} (mon0 : X) (mon2 : X -> X -> X) :=\r\n  MonoidLaws {\r\n      mon_eqv: Proper (eqv ==> eqv ==> eqv) mon2;\r\n      monA: forall x y z, mon2 x (mon2 y z) ≡ mon2 (mon2 x y) z;\r\n      monC: forall x y, mon2 x y ≡ mon2 y x;\r\n      monU: forall x, mon2 x mon0 ≡ x\r\n    }.\r\n```\r\nWe then prove lemmas in the following form:\r\n```coq\r\nperm_big\r\n     : forall (X : setoid) (mon0 : X) (mon2 : X -> X -> X), monoidLaws mon0 mon2 ->\r\n       forall (I : eqType) (r1 r2 : seq I) (P : pred I) (F : I -> X), perm_eq r1 r2 -> \r\n       \\big[mon2/mon0]_(i <- r1 | P i) F i ≡ \\big[mon2/mon0]_(i <- r2 | P i) F i\r\n```\r\nSo the question is whether there is any interest in integrating this into mathcomp and, if so, what would be the right way to do it. In particular, the following questions should be answered before I even embark on creating a pull request:\r\n\r\n1. What is the proper setup of structures/classes in this setting from the mathcomp perspective?\r\n2. How to deal with the fact that the setoid-based lemmas subsume the equivalence-based lemmas? (naming conventions, compatibility, avoiding code duplication)"}}
other: {"actor":{"display_login":"chdoc"}}