{"action":"created","issue":{"url":"https://api.github.com/repos/leanprover/lean/issues/1718","repository_url":"https://api.github.com/repos/leanprover/lean","labels_url":"https://api.github.com/repos/leanprover/lean/issues/1718/labels{/name}","comments_url":"https://api.github.com/repos/leanprover/lean/issues/1718/comments","events_url":"https://api.github.com/repos/leanprover/lean/issues/1718/events","html_url":"https://github.com/leanprover/lean/issues/1718","id":240039951,"number":1718,"title":"Annotation required for `eq.substr`","user":{"login":"ranweiler","id":515835,"avatar_url":"https://avatars2.githubusercontent.com/u/515835?v=3","gravatar_id":"","url":"https://api.github.com/users/ranweiler","html_url":"https://github.com/ranweiler","followers_url":"https://api.github.com/users/ranweiler/followers","following_url":"https://api.github.com/users/ranweiler/following{/other_user}","gists_url":"https://api.github.com/users/ranweiler/gists{/gist_id}","starred_url":"https://api.github.com/users/ranweiler/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ranweiler/subscriptions","organizations_url":"https://api.github.com/users/ranweiler/orgs","repos_url":"https://api.github.com/users/ranweiler/repos","events_url":"https://api.github.com/users/ranweiler/events{/privacy}","received_events_url":"https://api.github.com/users/ranweiler/received_events","type":"User","site_admin":false},"labels":[{"id":613148332,"url":"https://api.github.com/repos/leanprover/lean/labels/A-elaborator","name":"A-elaborator","color":"fbca04","default":false},{"id":48139196,"url":"https://api.github.com/repos/leanprover/lean/labels/question","name":"question","color":"cc317c","default":true}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":3,"created_at":"2017-07-02T22:54:37Z","updated_at":"2017-07-03T18:20:35Z","closed_at":null,"body":"### Prerequisites\r\n\r\n* [x] Put an X between the brackets on this line if you have done all of the following:\r\n    * Checked that your issue isn't already [filed](https://github.com/leanprover/lean/issues).\r\n        * Specifically, check out the [wishlist](https://github.com/leanprover/lean/issues?q=is%3Aissue+is%3Aopen+label%3AI-wishlist), open [RFCs](https://github.com/leanprover/lean/issues?q=is%3Aissue+is%3Aopen+label%3ARFC),\r\n        or [feature requests](https://github.com/leanprover/lean/issues?q=is%3Aissue+is%3Aopen+label%3AFeature).\r\n    * Reduced the issue to a self-contained, reproducible test case.\r\n\r\n### Description\r\n\r\nType checking fails when attempting to apply `eq.substr `, even though inlining its body succeeds.\r\n\r\n### Steps to Reproduce\r\n\r\n1. Consider the following development in a new file, say, `test.lean`:\r\n```lean\r\ntheorem my_theorem : ∀ (a b c d : ℕ),\r\n  d = c → a = b * c → a = b * d :=\r\ntake a b c d,\r\nassume h₀ : d = c,\r\nassume h₁ : a = b * c,\r\neq.subst (eq.symm h₀) h₁\r\n```\r\nThis type checks, and proof succeeds.\r\n\r\n2. Replace the final line of the proof with `eq.substr h₀ h₁`.\r\n3. Attempt to check the proof.\r\n\r\n\r\n**Expected behavior:**\r\nI expect to the use of `eq.substr` to type check.\r\n\r\n**Actual behavior:**\r\nThe new final line fails to type check with the error:\r\n```\r\n/home/joe/src/nt-proofs/test.lean:20:0: error: type mismatch at application\r\n  eq.substr h₀\r\nterm\r\n  h₀\r\nhas type\r\n  d = c\r\nbut is expected to have type\r\n  b * d = ?m_1\r\n```\r\nIf we add `set_option pp.all true` to the top of the file, the error message is:\r\n```\r\n/home/joe/src/nt-proofs/test.lean:22:0: error: type mismatch at application\r\n  @eq.substr.{1} nat (@eq.{1} nat a) ?m_1 (@has_mul.mul.{0} nat nat.has_mul b d) h₀\r\nterm\r\n  h₀\r\nhas type\r\n  @eq.{1} nat d c\r\nbut is expected to have type\r\n  @eq.{1} nat (@has_mul.mul.{0} nat nat.has_mul b d) ?m_1\r\n```\r\n\r\n**Reproduces how often:**\r\n100% reproducible.\r\n\r\n### Versions\r\n\r\nPlatform: Debian Linux 9 \"Stretch\", `Linux 4.9.0-3-amd64 #1 SMP Debian 4.9.30-2+deb9u1 (2017-06-18) x86_64 GNU/Linux`\r\nLean version: `Lean (version 3.2.1, commit f7fe2a775c14, Release)`\r\n\r\n### Additional Information\r\n\r\nI took a look at the definition of `eq.substr` in `init/logic.lean` and compared it to the definition of `eq.subst` in `init/core.lean`. The definition of `eq.subst` has the annotation `@[elab_as_eliminator, subst]`. If I make a copy of `eq.substr` in my test file, and add the (smaller) annotation `@[elab_as_eliminator]`, then the final line type checks.\r\n\r\nI poked around `frontends/elaborator.cpp` to see what this does (since it isn't seem to be documented [quite yet](https://github.com/leanprover/reference/tree/master/Attributes)), but I don't yet understand enough of Lean's internals to be able to confidently suggest any of: (1) this is expected behavior, (2) this is a bug, or (3) the `eq.substr` definition simply should have the annotation added.\r\n\r\nI'm still working through the \"Theorem Proving in Lean\" tutorial, but I've searched the docs extensively, and am having trouble meaningfully diagnosing what is going on myself. I'd love to have a sense of the following:\r\n1. Is there a way to manually/locally accomplish what is accomplished by the `elab_as_eliminator` annotation on the `eq.subst` definition? In other words, is there a way I could invoke `eq.substr` in the above example that would succeed, via perhaps a use of `@eq.substr` or `eq.rec_on`?\r\n1. Adding a file-local attribute like `local attribute [elab_as_eliminator] eq.substr` doesn't seem to have any effect (nor an error message or warning). Is this expected?\r\n1. Even having found a \"fix\", I don't yet understand how to relate the error message to what was going wrong. I instead relied on trial-and-error and browsing source code. What surprised me is that the error seemed to be about the type of `h₀`, the simple equality `d = c`, and not `h₁`, the argument for which Lean needs to infer the implicit predicate argument. In a case like this, should I, as a user, be able to work from the existing error message to the understanding that e.g. some sort of extra elimination is needed? If anything, it seemed like the error message was expecting the _wrong_ type. I'm guessing this has to do with elaborator internals, but maybe there's something simpler I'm currently ignorant of. Any pointers on how to think about this specific problem (and to better use the existing error messages) would be much appreciated!"},"comment":{"url":"https://api.github.com/repos/leanprover/lean/issues/comments/312708402","html_url":"https://github.com/leanprover/lean/issues/1718#issuecomment-312708402","issue_url":"https://api.github.com/repos/leanprover/lean/issues/1718","id":312708402,"user":{"login":"leodemoura","id":2778936,"avatar_url":"https://avatars1.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":"2017-07-03T18:20:35Z","updated_at":"2017-07-03T18:20:35Z","body":"@gebner @kha @jroesch We can try to improve the error message by checking whether the function has implicit arguments that require higher-order unification (e.g.,  `p : α → Prop` in the example above), and if does we append extra information in the error message (e.g., `function 'eq.substr' require higher-order unfication ...`). We may also try the `elab_as_eliminator` strategy, and if it succeeds, we also include the message `consider marking 'eq.substr' the attribute '[elab_as_eliminator]'`). What do you think?"}}
{"actor":{"display_login":"leodemoura"}}