{"action":"created","issue":{"url":"https://api.github.com/repos/coq/coq/issues/9028","repository_url":"https://api.github.com/repos/coq/coq","labels_url":"https://api.github.com/repos/coq/coq/issues/9028/labels{/name}","comments_url":"https://api.github.com/repos/coq/coq/issues/9028/comments","events_url":"https://api.github.com/repos/coq/coq/issues/9028/events","html_url":"https://github.com/coq/coq/issues/9028","id":382315834,"node_id":"MDU6SXNzdWUzODIzMTU4MzQ=","number":9028,"title":"destructing an n-tuple takes O(n^2.5) time","user":{"login":"andres-erbsen","id":918403,"node_id":"MDQ6VXNlcjkxODQwMw==","avatar_url":"https://avatars0.githubusercontent.com/u/918403?v=4","gravatar_id":"","url":"https://api.github.com/users/andres-erbsen","html_url":"https://github.com/andres-erbsen","followers_url":"https://api.github.com/users/andres-erbsen/followers","following_url":"https://api.github.com/users/andres-erbsen/following{/other_user}","gists_url":"https://api.github.com/users/andres-erbsen/gists{/gist_id}","starred_url":"https://api.github.com/users/andres-erbsen/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/andres-erbsen/subscriptions","organizations_url":"https://api.github.com/users/andres-erbsen/orgs","repos_url":"https://api.github.com/users/andres-erbsen/repos","events_url":"https://api.github.com/users/andres-erbsen/events{/privacy}","received_events_url":"https://api.github.com/users/andres-erbsen/received_events","type":"User","site_admin":false},"labels":[{"id":651324615,"node_id":"MDU6TGFiZWw2NTEzMjQ2MTU=","url":"https://api.github.com/repos/coq/coq/labels/kind:%20performance","name":"kind: performance","color":"9900cc","default":false}],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":3,"created_at":"2018-11-19T17:19:06Z","updated_at":"2018-11-20T17:33:22Z","closed_at":null,"author_association":"CONTRIBUTOR","body":"<!-- Thank you for your contribution.\r\n     Please complete the following information when reporting a bug. -->\r\n\r\n#### Version\r\n\r\n~~~~~\r\nThe Coq Proof Assistant, version 8.8.2 (October 2018)\r\ncompiled on Oct 1 2018 0:22:50 with OCaml 4.07.0\r\n~~~~~\r\n\r\n#### Operating system\r\n\r\nArch Linux, up to date as of yesterday.\r\n\r\n#### Description of the problem\r\n\r\ndestructing an n-tuple takes O(n^2.5) time, in proof and again in Qed.\r\n\r\nhttps://github.com/andres-erbsen/coq-experiments/commit/c2635094f254b63b1e25a6bb0d3ce716b1f4a585\r\n\r\nin short:\r\n\r\n~~~~~\r\nFixpoint exn (n:nat) :=\r\n  match n with O => False | S n => exists tt:unit, exn n end.\r\nGoal exn 1000 -> False. intro H. cbv in H. idtac \"\".\r\n  Time (repeat match goal with H:exists _, _ |-_=> destruct H end; assumption).\r\nTime Qed.\r\n(* Finished transaction in 7.444 secs (7.314u,0.079s) (successful) *)\r\n(* Finished transaction in 7.449 secs (7.404u,0.s) (successful) *)\r\n~~~~~\r\n\r\n<!-- It is helpful to provide enough information so that we can reproduce the bug.\r\n     In particular, please include a code example which produces it.\r\n     If the example is small, you can include it here between ``` ```.\r\n     Otherwise, please provide a link to a repository, a gist (https://gist.github.com)\r\n     or drag-and-drop a `.zip` archive. -->\r\n\r\nSurprisingly, using primitive projections makes the proof time significantly worse (though Qed time improves slightly). https://github.com/andres-erbsen/coq-experiments/commit/c2635094f254b63b1e25a6bb0d3ce716b1f4a585#diff-e49eb5f90ca1c823f445149990b558b2R1\r\n\r\nNote that Qed time measurements may be affected by #8236. Possibly related to #8245, #8244, #8237.\r\n\r\nAs `destruct` is very commonly used in proof scripts, I speculate that improving its asymptotic performance might give measurable benefits in existing developments."},"comment":{"url":"https://api.github.com/repos/coq/coq/issues/comments/440362031","html_url":"https://github.com/coq/coq/issues/9028#issuecomment-440362031","issue_url":"https://api.github.com/repos/coq/coq/issues/9028","id":440362031,"node_id":"MDEyOklzc3VlQ29tbWVudDQ0MDM2MjAzMQ==","user":{"login":"ppedrot","id":1202327,"node_id":"MDQ6VXNlcjEyMDIzMjc=","avatar_url":"https://avatars1.githubusercontent.com/u/1202327?v=4","gravatar_id":"","url":"https://api.github.com/users/ppedrot","html_url":"https://github.com/ppedrot","followers_url":"https://api.github.com/users/ppedrot/followers","following_url":"https://api.github.com/users/ppedrot/following{/other_user}","gists_url":"https://api.github.com/users/ppedrot/gists{/gist_id}","starred_url":"https://api.github.com/users/ppedrot/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/ppedrot/subscriptions","organizations_url":"https://api.github.com/users/ppedrot/orgs","repos_url":"https://api.github.com/users/ppedrot/repos","events_url":"https://api.github.com/users/ppedrot/events{/privacy}","received_events_url":"https://api.github.com/users/ppedrot/received_events","type":"User","site_admin":false},"created_at":"2018-11-20T17:33:22Z","updated_at":"2018-11-20T17:33:22Z","author_association":"MEMBER","body":"The Qed part is slow not due to the kernel, but because of evar normalization. Probably the fact that your term is big matters, in particular in the hidden branch types."}}
{"actor":{"display_login":"ppedrot"}}