{"action":"created","issue":{"url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/18","repository_url":"https://api.github.com/repos/mit-plv/fiat-crypto","labels_url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/18/labels{/name}","comments_url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/18/comments","events_url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/18/events","html_url":"https://github.com/mit-plv/fiat-crypto/pull/18","id":163498075,"number":18,"title":"Implement and prove Barrett reduction on Z","user":{"login":"JasonGross","id":396076,"avatar_url":"https://avatars.githubusercontent.com/u/396076?v=3","gravatar_id":"","url":"https://api.github.com/users/JasonGross","html_url":"https://github.com/JasonGross","followers_url":"https://api.github.com/users/JasonGross/followers","following_url":"https://api.github.com/users/JasonGross/following{/other_user}","gists_url":"https://api.github.com/users/JasonGross/gists{/gist_id}","starred_url":"https://api.github.com/users/JasonGross/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/JasonGross/subscriptions","organizations_url":"https://api.github.com/users/JasonGross/orgs","repos_url":"https://api.github.com/users/JasonGross/repos","events_url":"https://api.github.com/users/JasonGross/events{/privacy}","received_events_url":"https://api.github.com/users/JasonGross/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":4,"created_at":"2016-07-02T02:31:05Z","updated_at":"2016-07-02T16:22:10Z","closed_at":null,"pull_request":{"url":"https://api.github.com/repos/mit-plv/fiat-crypto/pulls/18","html_url":"https://github.com/mit-plv/fiat-crypto/pull/18","diff_url":"https://github.com/mit-plv/fiat-crypto/pull/18.diff","patch_url":"https://github.com/mit-plv/fiat-crypto/pull/18.patch"},"body":"This will serve as the high-level algorithm for modular reduction.\r\n\r\nWe follow Wikipedia very closely, except where we can do better (I\r\nbelieve @jadep is updating Wikipedia).\r\n\r\nQuestions:\r\n- [ ] Is there a cleaner proof of `r_small` (@jadep, how does this one compare to your paper one?)  The main bottlenecks in making it shorter are that we're missing rewriting mod AC, and that we can't rewrite with `<=` lemmas.  (We could add typeclass instances for `setoid_rewrite`, but this would likely make all other rewriting in `Z` slower.  And it would be a pain.)\r\n- [ ] How do we feel about interleaving the reference and the code, and about quoting Wikipedia (@andres-erbson, @achlipala)\r\n- [ ] How do we feel about the unicode notations used for readability by non-Coq'ers (@andres-erbson)\r\n\r\nAny other comments? (@agl @mschilder123)"},"comment":{"url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/comments/230109839","html_url":"https://github.com/mit-plv/fiat-crypto/pull/18#issuecomment-230109839","issue_url":"https://api.github.com/repos/mit-plv/fiat-crypto/issues/18","id":230109839,"user":{"login":"JasonGross","id":396076,"avatar_url":"https://avatars.githubusercontent.com/u/396076?v=3","gravatar_id":"","url":"https://api.github.com/users/JasonGross","html_url":"https://github.com/JasonGross","followers_url":"https://api.github.com/users/JasonGross/followers","following_url":"https://api.github.com/users/JasonGross/following{/other_user}","gists_url":"https://api.github.com/users/JasonGross/gists{/gist_id}","starred_url":"https://api.github.com/users/JasonGross/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/JasonGross/subscriptions","organizations_url":"https://api.github.com/users/JasonGross/orgs","repos_url":"https://api.github.com/users/JasonGross/repos","events_url":"https://api.github.com/users/JasonGross/events{/privacy}","received_events_url":"https://api.github.com/users/JasonGross/received_events","type":"User","site_admin":false},"created_at":"2016-07-02T16:22:10Z","updated_at":"2016-07-02T16:22:10Z","body":"Do we want to go all the way with the floor function notation, and make\r\n```coq\r\nLocal Notation \"⌊ x / y ⌋\" := (x / y) (only parsing).\r\n```\r\nso we don't need to keep reminding non-Coq'ers that `/` means truncated division?"}}
{"actor":{"display_login":"JasonGross"}}