{"action":"created","issue":{"url":"https://api.github.com/repos/FStarLang/FStar/issues/95","labels_url":"https://api.github.com/repos/FStarLang/FStar/issues/95/labels{/name}","comments_url":"https://api.github.com/repos/FStarLang/FStar/issues/95/comments","events_url":"https://api.github.com/repos/FStarLang/FStar/issues/95/events","html_url":"https://github.com/FStarLang/FStar/issues/95","id":51476129,"number":95,"title":"\"logic\" qualifier for inductive relations","user":{"login":"catalin-hritcu","id":5850655,"avatar_url":"https://avatars.githubusercontent.com/u/5850655?v=3","gravatar_id":"","url":"https://api.github.com/users/catalin-hritcu","html_url":"https://github.com/catalin-hritcu","followers_url":"https://api.github.com/users/catalin-hritcu/followers","following_url":"https://api.github.com/users/catalin-hritcu/following{/other_user}","gists_url":"https://api.github.com/users/catalin-hritcu/gists{/gist_id}","starred_url":"https://api.github.com/users/catalin-hritcu/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/catalin-hritcu/subscriptions","organizations_url":"https://api.github.com/users/catalin-hritcu/orgs","repos_url":"https://api.github.com/users/catalin-hritcu/repos","events_url":"https://api.github.com/users/catalin-hritcu/events{/privacy}","received_events_url":"https://api.github.com/users/catalin-hritcu/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/FStarLang/FStar/labels/enhancement","name":"enhancement","color":"84b6eb"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":1,"created_at":"2014-12-09T20:18:30Z","updated_at":"2015-02-11T10:50:00Z","closed_at":null,"body":"[Nik's original message on this]\r\nBTW, in order to be able to reason about these kind of types as predicates in the Z3, I propose using the \"logic\" qualifier. This will result in providing axioms to Z3 corresponding to the validity of the R predicate.\r\n\r\nFor example, in addition to the usual data type axioms, for an inductive type tagged with the \"logic\" qualifier as above, we'd  generate in Z3:\r\n```\r\nassert (forall t1 t2 e. Valid (typing empty e (TArrow t1 t2)) /\\ Valid (halts e) /\\ (forall e1. Valid (R t1 e1) ==> Valid (R t2 (EApp e e1)) ==> Valid (R (TArrow t1 t2) e)\r\n```\r\nWe would also generate the corresponding inversion axioms."},"comment":{"url":"https://api.github.com/repos/FStarLang/FStar/issues/comments/73863008","html_url":"https://github.com/FStarLang/FStar/issues/95#issuecomment-73863008","issue_url":"https://api.github.com/repos/FStarLang/FStar/issues/95","id":73863008,"user":{"login":"catalin-hritcu","id":5850655,"avatar_url":"https://avatars.githubusercontent.com/u/5850655?v=3","gravatar_id":"","url":"https://api.github.com/users/catalin-hritcu","html_url":"https://github.com/catalin-hritcu","followers_url":"https://api.github.com/users/catalin-hritcu/followers","following_url":"https://api.github.com/users/catalin-hritcu/following{/other_user}","gists_url":"https://api.github.com/users/catalin-hritcu/gists{/gist_id}","starred_url":"https://api.github.com/users/catalin-hritcu/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/catalin-hritcu/subscriptions","organizations_url":"https://api.github.com/users/catalin-hritcu/orgs","repos_url":"https://api.github.com/users/catalin-hritcu/repos","events_url":"https://api.github.com/users/catalin-hritcu/events{/privacy}","received_events_url":"https://api.github.com/users/catalin-hritcu/received_events","type":"User","site_admin":false},"created_at":"2015-02-11T10:50:00Z","updated_at":"2015-02-11T10:50:00Z","body":"Any progress on proper support for inductive relations? Seems that we're going to need this big time if we want to prove tinyfstar in F*"}}