{"action":"created","issue":{"url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/issues/219","labels_url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/issues/219/labels{/name}","comments_url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/issues/219/comments","events_url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/issues/219/events","html_url":"https://github.com/HOL-Theorem-Prover/HOL/issues/219","id":52577662,"number":219,"title":"LEX needs mono and cong theorems","user":{"login":"xrchz","id":181254,"avatar_url":"https://avatars.githubusercontent.com/u/181254?v=3","gravatar_id":"","url":"https://api.github.com/users/xrchz","html_url":"https://github.com/xrchz","followers_url":"https://api.github.com/users/xrchz/followers","following_url":"https://api.github.com/users/xrchz/following{/other_user}","gists_url":"https://api.github.com/users/xrchz/gists{/gist_id}","starred_url":"https://api.github.com/users/xrchz/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/xrchz/subscriptions","organizations_url":"https://api.github.com/users/xrchz/orgs","repos_url":"https://api.github.com/users/xrchz/repos","events_url":"https://api.github.com/users/xrchz/events{/privacy}","received_events_url":"https://api.github.com/users/xrchz/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":10,"created_at":"2014-12-20T21:49:30Z","updated_at":"2015-09-08T06:00:43Z","closed_at":null,"body":"Inductive relations and recursive functions that recurse through `LEX` fail or get unprovable termination conditions. The following theorems need to be included somewhere (probably `pairTheory`). There may be issues since `pairTheory` is so early in the build sequence.\r\n```\r\nval LEX_CONG = store_thm(\"LEX_CONG\",\r\n  ``(R1 x1 x2 <=> R1' x1' x2') /\\\r\n    (~(R1 x1 x2) ==> ((x1 = x2) <=> (x1' = x2'))) /\\\r\n    (~(R1 x1 x2) ==> (R2 y1 y2 <=> R2' y1' y2'))\r\n    ==> ((R1 LEX R2) (x1,y1) (x2,y2) <=> (R1' LEX R2') (x1',y1') (x2',y2'))``,\r\n  SRW_TAC[][LEX_DEF_THM] THEN METIS_TAC[])\r\nval () = DefnBase.export_cong\"LEX_CONG\"\r\n\r\nval LEX_MONO = store_thm(\"LEX_MONO\",\r\n  ``(!x y. R1 x y ==> R2 x y) /\\\r\n    (!x y. R3 x y ==> R4 x y)\r\n    ==>\r\n    (R1 LEX R3) x y ==> (R2 LEX R4) x y``,\r\n  STRIP_TAC THEN\r\n  Cases_on`x` THEN Cases_on`y` THEN\r\n  SRW_TAC[][LEX_DEF_THM] THEN\r\n  PROVE_TAC[])\r\nval () = IndDefLib.export_mono\"LEX_MONO\"\r\n```\r\n\r\n<bountysource-plugin>\r\n---\r\nWant to back this issue? **[Post a bounty on it!](https://www.bountysource.com/issues/7166252-lex-needs-mono-and-cong-theorems?utm_campaign=plugin&utm_content=tracker%2F495335&utm_medium=issues&utm_source=github)** We accept bounties via [Bountysource](https://www.bountysource.com/?utm_campaign=plugin&utm_content=tracker%2F495335&utm_medium=issues&utm_source=github).\r\n</bountysource-plugin>"},"comment":{"url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/issues/comments/138445104","html_url":"https://github.com/HOL-Theorem-Prover/HOL/issues/219#issuecomment-138445104","issue_url":"https://api.github.com/repos/HOL-Theorem-Prover/HOL/issues/219","id":138445104,"user":{"login":"konrad-slind","id":1105935,"avatar_url":"https://avatars.githubusercontent.com/u/1105935?v=3","gravatar_id":"","url":"https://api.github.com/users/konrad-slind","html_url":"https://github.com/konrad-slind","followers_url":"https://api.github.com/users/konrad-slind/followers","following_url":"https://api.github.com/users/konrad-slind/following{/other_user}","gists_url":"https://api.github.com/users/konrad-slind/gists{/gist_id}","starred_url":"https://api.github.com/users/konrad-slind/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/konrad-slind/subscriptions","organizations_url":"https://api.github.com/users/konrad-slind/orgs","repos_url":"https://api.github.com/users/konrad-slind/repos","events_url":"https://api.github.com/users/konrad-slind/events{/privacy}","received_events_url":"https://api.github.com/users/konrad-slind/received_events","type":"User","site_admin":false},"created_at":"2015-09-08T06:00:43Z","updated_at":"2015-09-08T06:00:43Z","body":"OK good. I modified the relation to be a recursive function (just an\nexample for testing).\nTurns out that comparisonTheory.list_cmp_cong is a good template to use for\nstating LLEX_CONG. Really, I am not sure that LLEX is useful, but if\nyou think it is, please do add LLEX_CONG to the system.\n\nCheers,\nKonrad.\n\n********************************************************************************\n\nload \"stringLib\";\n\nopen pairTheory comparisonTheory; (* source in HOLDIR/src/enumfset *)\n\n(*---------------------------------------------------------------------------*)\n(* Datatype of first-order terms.\n *)\n(*---------------------------------------------------------------------------*)\n\nval _ = Hol_datatype\n  `term\n     = Var of string\n     | App of string => term list`;\n\nval term_size_def = fetch \"-\" \"term_size_def\";\n\nval LEX_CONG = Q.store_thm\n(\"LEX_CONG\",\n `!R1 R2 v1 v2 R1' R2' v1' v2'.\n     (v1 = v1') /\\ (v2 = v2') /\\\n     (!a b c d. (v1' = (a,b)) /\\ (v2' = (c,d)) ==> (R1 a c = R1' a c)) /\\\n     (!a b c d. (v1' = (a,b)) /\\ (v2' = (c,d)) /\\ (a=c) ==> (R2 b d = R2' b\nd))\n   ==>\n    ($LEX R1 R2 v1 v2 = $LEX R1' R2' v1' v2')`,\n SIMP_TAC std_ss [LEX_DEF,FORALL_PROD] THEN METIS_TAC[]);\n\nval LLEX_CONG = Q.store_thm\n(\"LLEX_CONG\",\n `!R l1 l2 R' l1' l2'.\n    (l1 = l1') /\\ (l2 = l2') /\\\n    (!a b. MEM a l1' /\\ MEM b l2' ==> (R a b = R' a b))\n    ==>\n    (LLEX R l1 l2 = LLEX R' l1' l2')`,\n GEN_TAC THEN Induct THENL [ALL_TAC, GEN_TAC] THEN Induct THEN RW_TAC\nlist_ss []\n   THEN RW_TAC list_ss [listTheory.LLEX_THM]\n   THEN FULL_SIMP_TAC list_ss []\n   THEN METIS_TAC[]);\n\nval _ = List.app DefnBase.add_cong [LEX_CONG,LLEX_CONG];\n\n(*---------------------------------------------------------------------------*)\n(* Example\n  *)\n(*---------------------------------------------------------------------------*)\n\nval lt_string_def =\n Define\n  `lt_string s1 s2 = (string_cmp s1 s2 = Less)`;\n\nval lt_term_def = tDefine\n \"lt_term\"\n `(lt_term (Var s1) (Var s2) = lt_string s1 s2) /\\\n  (lt_term (Var _) (App _ _) = T) /\\\n  (lt_term (App _ _) (Var _) = F) /\\\n  (lt_term (App f flist) (App g glist) = (lt_string LEX (LLEX lt_term))\n(f,flist) (g,glist))`\n (WF_REL_TAC `measure (term_size o FST)`\n   THEN Induct_on `flist`\n   THEN RW_TAC list_ss [term_size_def]\n   THENL\n     [ALL_TAC, RES_TAC THEN POP_ASSUM (MP_TAC o SPEC_ALL)]\n   THEN DECIDE_TAC);\n\n\nOn Mon, Sep 7, 2015 at 6:52 PM, Ramana Kumar <notifications@github.com>\nwrote:\n\n> Regarding examples, my use of LLEX is here:\n> https://github.com/CakeML/cakeml/blob/master/hol-light/standard/syntax/holSyntaxScript.sml#L131\n>\n> —\n> Reply to this email directly or view it on GitHub\n> <https://github.com/HOL-Theorem-Prover/HOL/issues/219#issuecomment-138393698>\n> .\n>\n"}}