{"action":"closed","issue":{"url":"https://api.github.com/repos/MetaCoq/MetaCoq/issues/9","labels_url":"https://api.github.com/repos/MetaCoq/MetaCoq/issues/9/labels{/name}","comments_url":"https://api.github.com/repos/MetaCoq/MetaCoq/issues/9/comments","events_url":"https://api.github.com/repos/MetaCoq/MetaCoq/issues/9/events","html_url":"https://github.com/MetaCoq/MetaCoq/issues/9","id":111708379,"number":9,"title":"Proposal for simplification of terms","user":{"login":"beta-ziliani","id":5183634,"avatar_url":"https://avatars.githubusercontent.com/u/5183634?v=3","gravatar_id":"","url":"https://api.github.com/users/beta-ziliani","html_url":"https://github.com/beta-ziliani","followers_url":"https://api.github.com/users/beta-ziliani/followers","following_url":"https://api.github.com/users/beta-ziliani/following{/other_user}","gists_url":"https://api.github.com/users/beta-ziliani/gists{/gist_id}","starred_url":"https://api.github.com/users/beta-ziliani/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/beta-ziliani/subscriptions","organizations_url":"https://api.github.com/users/beta-ziliani/orgs","repos_url":"https://api.github.com/users/beta-ziliani/repos","events_url":"https://api.github.com/users/beta-ziliani/events{/privacy}","received_events_url":"https://api.github.com/users/beta-ziliani/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/MetaCoq/MetaCoq/labels/enhancement","name":"enhancement","color":"84b6eb"},{"url":"https://api.github.com/repos/MetaCoq/MetaCoq/labels/question","name":"question","color":"cc317c"}],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":3,"created_at":"2015-10-15T21:09:47Z","updated_at":"2015-11-03T23:02:11Z","closed_at":"2015-11-03T23:02:11Z","body":"Right now simplification is done through the unit command (`retS`, `retW`, etc). One problem with this approach is that in a code like\r\n```\r\nA <- retS B;\r\nf A\r\n```\r\nwhere `f : B -> C`, the typechecker complains (reasonably) that A is not B. However, A is the normalized version of B, so actually *is* B. This problem introduces several inconveniences when trying to deal with normalized terms. My proposal is the following:\r\nCreate a definition isomorphic to the identity:\r\n```\r\nDefinition simpl {A} (x : A) := x.\r\n```\r\nIn the interpreter, the behavior is the same, except when it encounters a let-in. In that case, it figures out if the head of the definition in the let-in is a simpl, and then reduces the argument before expanding it. The example above can be rewritten as\r\n```\r\nlet A := simpl B in\r\nf A\r\n```\r\nAnd now it will first simplify B and then proceed to whatever `f A` is. This is implemented in the branch *simpl* if you want to check it out.\r\n\r\nSo what do you think? (Question for @yurug and/or any other participant!)"}}