{"action":"created","issue":{"url":"https://api.github.com/repos/leanprover/lean/issues/420","labels_url":"https://api.github.com/repos/leanprover/lean/issues/420/labels{/name}","comments_url":"https://api.github.com/repos/leanprover/lean/issues/420/comments","events_url":"https://api.github.com/repos/leanprover/lean/issues/420/events","html_url":"https://github.com/leanprover/lean/pull/420","id":56170675,"number":420,"title":"housecleaning","user":{"login":"avigad","id":2783534,"avatar_url":"https://avatars.githubusercontent.com/u/2783534?v=3","gravatar_id":"","url":"https://api.github.com/users/avigad","html_url":"https://github.com/avigad","followers_url":"https://api.github.com/users/avigad/followers","following_url":"https://api.github.com/users/avigad/following{/other_user}","gists_url":"https://api.github.com/users/avigad/gists{/gist_id}","starred_url":"https://api.github.com/users/avigad/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/avigad/subscriptions","organizations_url":"https://api.github.com/users/avigad/orgs","repos_url":"https://api.github.com/users/avigad/repos","events_url":"https://api.github.com/users/avigad/events{/privacy}","received_events_url":"https://api.github.com/users/avigad/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":14,"created_at":"2015-02-01T17:36:33Z","updated_at":"2015-02-01T20:00:51Z","closed_at":"2015-02-01T20:00:51Z","pull_request":{"url":"https://api.github.com/repos/leanprover/lean/pulls/420","html_url":"https://github.com/leanprover/lean/pull/420","diff_url":"https://github.com/leanprover/lean/pull/420.diff","patch_url":"https://github.com/leanprover/lean/pull/420.patch"},"body":"\r\nTwo run tests break with this, because a slightly modified dependency introduces a line \"warning: imported file uses sorry\". Leo, I think these are easy to fix, but if you tell me how I will do it in the future. (Is it just a matter of editing the file with the expected output?)\r\n\r\nI renamed logic.axioms.classical to logic.axioms.prop_complete. I also renamed logic.axioms.default to logic.axioms.classical. That way, either\r\n\r\n  import classical\r\n\r\nor \r\n\r\n  import logic.axioms.classical\r\n\r\nimports the classical axioms. I did this because a user might want to import the classical axioms without importing the whole library. \r\n\r\nWhen we import the classical axioms, the user now has \"by_cases\" and \"by_contradiction\" available at top level, like \"em\", rather than in namespace \"decidable\".\r\n\r\nI made some partial moves to put more notation for prod and sigma at top level, but some changes need discussion. Since prod and sigma are in init, I did not want to do anything dramatic.\r\n\r\nIdeally, I think the opening lines of logic.init.prod and logic.init.sigma should be parallel. We should have the following available at the top level:\r\n\r\n  prod: \\times, *, pair, pr1, pr2, (a, b)\r\n  sigma: \\Sigma, dpair, dpr1, dpr2, \\<a, b\\>\r\n\r\nWe should also have .1 and .2 in prod.ops and sigma.ops.\r\n\r\nOne issue is that the constructors for prod and sigma are now called prod.mk and sigma.mk. We have defined pair := @prod.mk and dpair := @sigma.mk. I am sure the internal code uses the names prod.mk and sigma.mk extensively, so I think it is o.k. to have pair and dpair as abbreviations.\r\n\r\nAnother issue is that the projections for both prod and sigma are already called pr1 and pr2. So if we define pr1 and pr2 at top level, then we will have a conflict if we open prod or sigma. Is there a way to protect the projections? If not, an alternative is to rename the internal projections proj1, proj2 (and maybe dproj1, dproj2 for sigma) -- but that probably involves changing a lot of code.\r\n\r\nAnyhow, I made some of the changes, but here is what is left to be done:\r\n\r\n(1) move the definition of sigma from init.sigma to init.datatypes, in parallel with int.prod, unless there is a reason that it is bad to introduce the dependency on int.datatypes.\r\n\r\n(2) move the \\times and * notation in init.prod outside the prod namespace. (I could have done that, but I was afraid to break something.)\r\n\r\n(3) Q: is there some way to define pr1 and pr2 at top level for prod, without introducing conflicts with \"open prod\" and \"open sigma\"?\r\n\r\nWhen all these changes are merged, I will have to update the tutorial. In particular, I will remove \"open prod\" and \"open sigma\" where possible, and give examples of by_contradiction and by_cases in the section on classical logic.\r\n\r\n\r\n\r\n"},"comment":{"url":"https://api.github.com/repos/leanprover/lean/issues/comments/72381184","html_url":"https://github.com/leanprover/lean/pull/420#issuecomment-72381184","issue_url":"https://api.github.com/repos/leanprover/lean/issues/420","id":72381184,"user":{"login":"leodemoura","id":2778936,"avatar_url":"https://avatars.githubusercontent.com/u/2778936?v=3","gravatar_id":"","url":"https://api.github.com/users/leodemoura","html_url":"https://github.com/leodemoura","followers_url":"https://api.github.com/users/leodemoura/followers","following_url":"https://api.github.com/users/leodemoura/following{/other_user}","gists_url":"https://api.github.com/users/leodemoura/gists{/gist_id}","starred_url":"https://api.github.com/users/leodemoura/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/leodemoura/subscriptions","organizations_url":"https://api.github.com/users/leodemoura/orgs","repos_url":"https://api.github.com/users/leodemoura/repos","events_url":"https://api.github.com/users/leodemoura/events{/privacy}","received_events_url":"https://api.github.com/users/leodemoura/received_events","type":"User","site_admin":false},"created_at":"2015-02-01T20:00:51Z","updated_at":"2015-02-01T20:00:51Z","body":"I have integrated the changes. \r\nI added instructions for fixing tests https://github.com/leanprover/lean/blob/master/doc/fixing_tests.md\r\nThey might be useful in the future."}}