{"action":"closed","issue":{"url":"https://api.github.com/repos/abella-prover/abella/issues/106","repository_url":"https://api.github.com/repos/abella-prover/abella","labels_url":"https://api.github.com/repos/abella-prover/abella/issues/106/labels{/name}","comments_url":"https://api.github.com/repos/abella-prover/abella/issues/106/comments","events_url":"https://api.github.com/repos/abella-prover/abella/issues/106/events","html_url":"https://github.com/abella-prover/abella/issues/106","id":344539948,"node_id":"MDU6SXNzdWUzNDQ1Mzk5NDg=","number":106,"title":"Error in renaming of bound variables in metaterms","user":{"login":"yvting","id":320428,"node_id":"MDQ6VXNlcjMyMDQyOA==","avatar_url":"https://avatars3.githubusercontent.com/u/320428?v=4","gravatar_id":"","url":"https://api.github.com/users/yvting","html_url":"https://github.com/yvting","followers_url":"https://api.github.com/users/yvting/followers","following_url":"https://api.github.com/users/yvting/following{/other_user}","gists_url":"https://api.github.com/users/yvting/gists{/gist_id}","starred_url":"https://api.github.com/users/yvting/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/yvting/subscriptions","organizations_url":"https://api.github.com/users/yvting/orgs","repos_url":"https://api.github.com/users/yvting/repos","events_url":"https://api.github.com/users/yvting/events{/privacy}","received_events_url":"https://api.github.com/users/yvting/received_events","type":"User","site_admin":false},"labels":[{"id":47891185,"node_id":"MDU6TGFiZWw0Nzg5MTE4NQ==","url":"https://api.github.com/repos/abella-prover/abella/labels/bug","name":"bug","color":"e11d21","default":true}],"state":"closed","locked":false,"assignee":{"login":"yvting","id":320428,"node_id":"MDQ6VXNlcjMyMDQyOA==","avatar_url":"https://avatars3.githubusercontent.com/u/320428?v=4","gravatar_id":"","url":"https://api.github.com/users/yvting","html_url":"https://github.com/yvting","followers_url":"https://api.github.com/users/yvting/followers","following_url":"https://api.github.com/users/yvting/following{/other_user}","gists_url":"https://api.github.com/users/yvting/gists{/gist_id}","starred_url":"https://api.github.com/users/yvting/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/yvting/subscriptions","organizations_url":"https://api.github.com/users/yvting/orgs","repos_url":"https://api.github.com/users/yvting/repos","events_url":"https://api.github.com/users/yvting/events{/privacy}","received_events_url":"https://api.github.com/users/yvting/received_events","type":"User","site_admin":false},"assignees":[{"login":"yvting","id":320428,"node_id":"MDQ6VXNlcjMyMDQyOA==","avatar_url":"https://avatars3.githubusercontent.com/u/320428?v=4","gravatar_id":"","url":"https://api.github.com/users/yvting","html_url":"https://github.com/yvting","followers_url":"https://api.github.com/users/yvting/followers","following_url":"https://api.github.com/users/yvting/following{/other_user}","gists_url":"https://api.github.com/users/yvting/gists{/gist_id}","starred_url":"https://api.github.com/users/yvting/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/yvting/subscriptions","organizations_url":"https://api.github.com/users/yvting/orgs","repos_url":"https://api.github.com/users/yvting/repos","events_url":"https://api.github.com/users/yvting/events{/privacy}","received_events_url":"https://api.github.com/users/yvting/received_events","type":"User","site_admin":false}],"milestone":null,"comments":2,"created_at":"2018-07-25T17:38:00Z","updated_at":"2018-07-28T14:39:21Z","closed_at":"2018-07-28T14:39:21Z","author_association":"CONTRIBUTOR","body":"Renaming of bound variables in a metaterm does not check clash of names between renamed variables and top-level constants\r\n\r\nConsider the following (contrived) example:\r\n```\r\nSet instantiations on.\r\n\r\nKind i   type.\r\n\r\nType p2   i.\r\n\r\nTheorem rename_failure: forall (p:i), \r\n   false \\/ forall (p:i), false \\/ forall (p1:i), p2 = p1.\r\nintros. right. intros. right. intros. search.\r\n```\r\nTo prove `rename_failure`, the first `intro` introduces a new eigenvariable named `p`. The second `intro` introduces a variable named `p1` which is the first fresh name that does not conflict with `p`. This triggers the renaming of bound variable `p1`. Because the renaming process does not consider conflicts with top-level constants, it wrongly decides that `p2` is the first fresh name that does not capture free variables after renaming. As such, the final goal becomes `forall (p2:i), p2 = p2` which is provable.\r\n\r\nUsing `rename_failure`, we can easily prove `false`, as follows:\r\n```\r\nTheorem all_eq : forall (p:i), p2 = p.\r\nintros. apply rename_failure with p = p2.\r\n  case H1. apply H2 with p = p2. case H3. \r\n  apply H4 with p1 = p. search.\r\n\r\nType q    i.\r\n\r\nTheorem unsound: false.\r\nassert (p2 = q -> false). backchain H1. backchain all_eq.\r\n```"}}
{"actor":{"display_login":"yvting"}}