{"action":"created","issue":{"url":"https://api.github.com/repos/jonsterling/JonPRL/issues/243","labels_url":"https://api.github.com/repos/jonsterling/JonPRL/issues/243/labels{/name}","comments_url":"https://api.github.com/repos/jonsterling/JonPRL/issues/243/comments","events_url":"https://api.github.com/repos/jonsterling/JonPRL/issues/243/events","html_url":"https://github.com/jonsterling/JonPRL/issues/243","id":108929581,"number":243,"title":"Respect for Functionality","user":{"login":"jozefg","id":814961,"avatar_url":"https://avatars.githubusercontent.com/u/814961?v=3","gravatar_id":"","url":"https://api.github.com/users/jozefg","html_url":"https://github.com/jozefg","followers_url":"https://api.github.com/users/jozefg/followers","following_url":"https://api.github.com/users/jozefg/following{/other_user}","gists_url":"https://api.github.com/users/jozefg/gists{/gist_id}","starred_url":"https://api.github.com/users/jozefg/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jozefg/subscriptions","organizations_url":"https://api.github.com/users/jozefg/orgs","repos_url":"https://api.github.com/users/jozefg/repos","events_url":"https://api.github.com/users/jozefg/events{/privacy}","received_events_url":"https://api.github.com/users/jozefg/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":7,"created_at":"2015-09-29T18:26:21Z","updated_at":"2015-09-30T15:19:48Z","closed_at":null,"body":"So this is a fun one. JonPRL's core sequence judgment is supposed to have a functionality requirement, essentially demanding that if `H, x : A >> B(x)` holds, then `H >> B(a) = B(a')` if `H >> a = a' : A`. Now if this isn't required all sorts of fun things can happen and currently it isn't. \r\n\r\nThe biggest offender that I'm aware of is `creflexivity`. It allows us to conclude that two variables are `ceq` when in fact they needn't be! `f ~ f` shouldn't hold if we're viewing `f` as a variable of type `A -> B` since we want to replace it with functions that are only pointwise equal.\r\n\r\nI don't see an immediate good solution to this, we could require that `creflexivity` only apply to closed terms (really bad), we could add a goal forcing us to show that all the variables we assert are `ceq` are still `ceq` when replaced by only equal terms (my preferred option) or something else.\r\n\r\nThoughts?"},"comment":{"url":"https://api.github.com/repos/jonsterling/JonPRL/issues/comments/144444228","html_url":"https://github.com/jonsterling/JonPRL/issues/243#issuecomment-144444228","issue_url":"https://api.github.com/repos/jonsterling/JonPRL/issues/243","id":144444228,"user":{"login":"jonsterling","id":55057,"avatar_url":"https://avatars.githubusercontent.com/u/55057?v=3","gravatar_id":"","url":"https://api.github.com/users/jonsterling","html_url":"https://github.com/jonsterling","followers_url":"https://api.github.com/users/jonsterling/followers","following_url":"https://api.github.com/users/jonsterling/following{/other_user}","gists_url":"https://api.github.com/users/jonsterling/gists{/gist_id}","starred_url":"https://api.github.com/users/jonsterling/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jonsterling/subscriptions","organizations_url":"https://api.github.com/users/jonsterling/orgs","repos_url":"https://api.github.com/users/jonsterling/repos","events_url":"https://api.github.com/users/jonsterling/events{/privacy}","received_events_url":"https://api.github.com/users/jonsterling/received_events","type":"User","site_admin":false},"created_at":"2015-09-30T15:19:48Z","updated_at":"2015-09-30T15:19:48Z","body":"@vrahli Thanks for the clarification; definitely makes sense that we wouldn't have to prove it for `FV(b)`! This is the one, then:\r\n\r\n````\r\n   H |- a = b in Base\r\n     By EqualInBase\r\n     H |- a ~ b\r\n     forall v in (free_vars a), H |- v in Base\r\n````"}}