{"action":"created","issue":{"url":"https://api.github.com/repos/FStarLang/FStar/issues/496","repository_url":"https://api.github.com/repos/FStarLang/FStar","labels_url":"https://api.github.com/repos/FStarLang/FStar/issues/496/labels{/name}","comments_url":"https://api.github.com/repos/FStarLang/FStar/issues/496/comments","events_url":"https://api.github.com/repos/FStarLang/FStar/issues/496/events","html_url":"https://github.com/FStarLang/FStar/issues/496","id":137180575,"number":496,"title":"[Help, Bug ?] Problem to prove a simple equality","user":{"login":"VincentCheval","id":6087949,"avatar_url":"https://avatars.githubusercontent.com/u/6087949?v=3","gravatar_id":"","url":"https://api.github.com/users/VincentCheval","html_url":"https://github.com/VincentCheval","followers_url":"https://api.github.com/users/VincentCheval/followers","following_url":"https://api.github.com/users/VincentCheval/following{/other_user}","gists_url":"https://api.github.com/users/VincentCheval/gists{/gist_id}","starred_url":"https://api.github.com/users/VincentCheval/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/VincentCheval/subscriptions","organizations_url":"https://api.github.com/users/VincentCheval/orgs","repos_url":"https://api.github.com/users/VincentCheval/repos","events_url":"https://api.github.com/users/VincentCheval/events{/privacy}","received_events_url":"https://api.github.com/users/VincentCheval/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2016-02-29T08:11:06Z","updated_at":"2016-02-29T10:47:25Z","closed_at":null,"body":"Hello,\r\n\r\nI'm having a problem to prove a simple lemma. Here is the code:\r\n\r\n```\r\n(*--build-config\r\n    other-files: FStar.FunctionalExtensionality.fst FStar.Set.fsi FStar.Set.fst\r\n --*)\r\n\r\nmodule Test\r\n\r\ntype term\r\n\r\nassume val order_term : term -> Tot lex_t\r\n\r\nassume val fold_left : p:(term -> Type) -> t:term -> ('a -> (t':term{ p t' }) -> Tot 'a) -> 'a -> Tot 'a\r\n\r\nval vars : t:term -> Tot (Set.set term) (decreases (order_term t))\r\nlet rec vars t =\r\n  fold_left (fun t' -> order_term t' << order_term t) t (fun acc t' -> Set.union acc (vars t')) Set.empty\r\n\r\nval lemma_test: t:term -> Lemma\r\n  (requires True)\r\n  (ensures (vars t = fold_left (fun t' -> order_term t' << order_term t) t (fun acc t' -> Set.union acc (vars t')) Set.empty))\r\nlet lemma_test t = ()\r\n```\r\n\r\nThe function `order_term` is there to ensure that F* can prove that `vars` is a total function. However, I don't understand why F* is not able to prove `lemma_test`. The equality `vars t = fold_left (fun t' -> order_term t' << order_term t) t (fun acc t' -> Set.union acc (vars t')) Set.empty` corresponds exactly to the definition of `vars`. When I replace the definition of `vars t` by something very simple (like `let vars t = Set.empty`) then the corresponding lemma can be verified:\r\n\r\n```\r\nval lemma_test: t:term -> Lemma\r\n  (requires True)\r\n  (ensures (vars t = Set.empty))\r\n```\r\nSo i'm guessing it has to do with the recursive call but I don't really get why.\r\n\r\nThanks for the help.\r\n\r\nVincent  "},"comment":{"url":"https://api.github.com/repos/FStarLang/FStar/issues/comments/190150942","html_url":"https://github.com/FStarLang/FStar/issues/496#issuecomment-190150942","issue_url":"https://api.github.com/repos/FStarLang/FStar/issues/496","id":190150942,"user":{"login":"VincentCheval","id":6087949,"avatar_url":"https://avatars.githubusercontent.com/u/6087949?v=3","gravatar_id":"","url":"https://api.github.com/users/VincentCheval","html_url":"https://github.com/VincentCheval","followers_url":"https://api.github.com/users/VincentCheval/followers","following_url":"https://api.github.com/users/VincentCheval/following{/other_user}","gists_url":"https://api.github.com/users/VincentCheval/gists{/gist_id}","starred_url":"https://api.github.com/users/VincentCheval/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/VincentCheval/subscriptions","organizations_url":"https://api.github.com/users/VincentCheval/orgs","repos_url":"https://api.github.com/users/VincentCheval/repos","events_url":"https://api.github.com/users/VincentCheval/events{/privacy}","received_events_url":"https://api.github.com/users/VincentCheval/received_events","type":"User","site_admin":false},"created_at":"2016-02-29T10:47:25Z","updated_at":"2016-02-29T10:47:25Z","body":"The problem definitely comes from the recursive call of `vars` in the function `fold_left`. I changed a bit the function `vars` to make it simpler as follows:\r\n\r\n```\r\nval vars : t:term -> Tot (Set.set term) (decreases (order_term t))\r\nlet rec vars t =\r\n  fold_left (fun t' -> order_term t' << order_term t) t (fun acc t' -> Set.union acc Set.empty) Set.empty\r\n\r\nval lemma_test: t:term -> Lemma\r\n  (requires True)\r\n  (ensures (vars t = fold_left (fun t' -> order_term t' << order_term t) t (fun acc t' -> Set.union acc Set.empty) Set.empty))\r\n  (decreases (order_term t))\r\nlet lemma_test t = ()\r\n```\r\n\r\nAnd in that case, the code can be verified. So it's the call `vars t'` that is problematic... but I still don't know why.\r\n\r\nVincent\r\n"}}