{"id":38,"date":"2007-08-01T22:19:37","date_gmt":"2007-08-02T05:19:37","guid":{"rendered":"http:\/\/www.elbeno.com\/haskell_soe_blog\/?p=38"},"modified":"2008-01-08T07:09:43","modified_gmt":"2008-01-08T15:09:43","slug":"exercise-89","status":"publish","type":"post","link":"https:\/\/www.elbeno.com\/haskell_soe_blog\/?p=38","title":{"rendered":"Exercise 8.9"},"content":{"rendered":"<p>Proof from axioms is something that takes great care: it is all too easy to skip a step that &#8220;obviously follows&#8221; from the axioms without proving that step. I&#8217;m not convinced this is all correct&#8230;<\/p>\n<pre lang=\"haskell\">r\r\n\u00e2\u2030\u00a1 r `Intersect` univ [Axiom 4]\r\n\u00e2\u2030\u00a1 r `Intersect` (r `Union` Complement r) [Axiom 5]\r\n\u00e2\u2030\u00a1 (r `Intersect` r) `Union` (r `Intersect` Complement r) [Axiom 3]\r\n\u00e2\u2030\u00a1 (r `Intersect` r) `Union` Empty [Axiom 5]\r\n\u00e2\u2030\u00a1 (r `Intersect` r) [Axiom 4]\r\n\r\nLemma 1: r \u00e2\u2030\u00a1 (r `Intersect` r)\r\n\r\nr\r\n\u00e2\u2030\u00a1 r `Union` Empty [Axiom 4]\r\n\u00e2\u2030\u00a1 r `Union` (r `Intersect` Complement r) [Axiom 5]\r\n\u00e2\u2030\u00a1 (r `Union` r) `Intersect` (r `Union` Complement r) [Axiom 3]\r\n\u00e2\u2030\u00a1 (r `Union` r) `Intersect` univ [Axiom 5]\r\n\u00e2\u2030\u00a1 (r `Union` r) [Axiom 4]\r\n\r\nLemma 2: r \u00e2\u2030\u00a1 (r `Union` r)\r\n\r\nr `Union` univ\r\n\u00e2\u2030\u00a1 r `Union` (r `Union` Complement r) [Axiom 5]\r\n\u00e2\u2030\u00a1 (r `Union` r) `Union` Complement r [Axiom 1]\r\n\u00e2\u2030\u00a1 r `Union` Complement r [Lemma 2]\r\n\u00e2\u2030\u00a1 univ [Axiom 5]\r\n\r\nLemma 3: r `Union` univ \u00e2\u2030\u00a1 univ\r\n\r\nr `Intersect` Empty\r\n\u00e2\u2030\u00a1 r `Intersect` (r `Intersect` Complement r) [Axiom 5]\r\n\u00e2\u2030\u00a1 (r `Intersect` r) `Intersect` Complement r [Axiom 1]\r\n\u00e2\u2030\u00a1 r `Intersect` Complement r [Lemma 1]\r\n\u00e2\u2030\u00a1 Empty [Axiom 5]\r\n\r\nLemma 4: r `Intersect` Empty \u00e2\u2030\u00a1 Empty\r\n\r\nLet X = (r1 `Union` (r1 `Intersect` r2))\r\nX `Intersect` Complement r1\r\n\u00e2\u2030\u00a1 (r1 `Union` (r1 `Intersect` r2)) `Intersect` Complement r1\r\n\u00e2\u2030\u00a1 (r1 `Intersect` Complement r1) `Union`\r\n  ((r1 `Intersect` r2) `Intersect` Complement r1) [Axiom 3]\r\n\u00e2\u2030\u00a1 Empty `Union` ((r1 `Intersect` r2) `Intersect` Complement r1) [Axiom 5]\r\n\u00e2\u2030\u00a1 (r1 `Intersect` r2) `Intersect` Complement r1 [Axiom 4]\r\n\u00e2\u2030\u00a1 (r2 `Intersect` r1) `Intersect` Complement r1 [Axiom 2]\r\n\u00e2\u2030\u00a1 r2 `Intersect` (r1 `Intersect` Complement r1) [Axiom 1]\r\n\u00e2\u2030\u00a1 r2 `Intersect` Empty [Axiom 5]\r\n\u00e2\u2030\u00a1 Empty [Lemma 4]\r\n\u00e2\u02c6\u00b4 by Axiom 5, X = r1\r\n\r\nLemma 5: (r1 `Union` (r1 `Intersect` r2)) \u00e2\u2030\u00a1 r1\r\n\r\nr1 `Intersect` (r1 `Union` r2)\r\n\u00e2\u2030\u00a1 (r1 `Union` r1) `Intersect` (r1 `Union` r2) [Lemma 2]\r\n\u00e2\u2030\u00a1 r1 `Union` (r1 `Intersect` r2) [Axiom 3]\r\n\u00e2\u2030\u00a1 r1 [Lemma 5]\r\n\r\nLemma 6: (r1 `Intersect` (r1 `Union` r2)) \u00e2\u2030\u00a1 r1\r\n\r\nLet X = Complement (Complement r)\r\nX `Union` (Complement r)\r\n\u00e2\u2030\u00a1 Complement (Complement r) `Union` (Complement r)\r\n\u00e2\u2030\u00a1 univ [Axiom 5]\r\n\u00e2\u02c6\u00b4 by Axiom 5, X = r\r\n\r\nLemma 7: Complement (Complement r) \u00e2\u2030\u00a1 r\r\n\r\nLet X = Complement Empty\r\nX `Union` Empty\r\n\u00e2\u2030\u00a1 Complement Empty `Union` Empty\r\n\u00e2\u2030\u00a1 univ [Axiom 5]\r\n\u00e2\u02c6\u00b4 by Axiom 4, X = univ\r\n\r\nLemma 8: Complement Empty \u00e2\u2030\u00a1 univ\r\n\r\nComplement univ\r\n\u00e2\u2030\u00a1 Complement (Complement Empty) [Lemma 8]\r\n\u00e2\u2030\u00a1 Empty [Lemma 7]\r\n\r\nLemma 9: Complement univ \u00e2\u2030\u00a1 Empty\r\n\r\nLet X = Complement (r1 `Union` r2)\r\n(r1 `Union` r2) `Union` X\r\n\u00e2\u2030\u00a1 (r1 `Union` r2) `Union` Complement (r1 `Union` r2)\r\n\u00e2\u2030\u00a1 univ [Axiom 5]\r\n\r\nLet Y = Complement r1 `Intersect` Complement r2\r\n(r1 `Union` r2) `Union` Y\r\n\u00e2\u2030\u00a1 (r1 `Union` r2) `Union` (Complement r1 `Intersect` Complement r2)\r\n\u00e2\u2030\u00a1 ((r1 `Union` r2) `Union` Complement r1) `Intersect`\r\n  ((r1 `Union` r2) `Union` Complement r2) [Axiom 3]\r\n\u00e2\u2030\u00a1 ((r2 `Union` r1) `Union` Complement r1) `Intersect`\r\n  ((r1 `Union` r2) `Union` Complement r2) [Axiom 2]\r\n\u00e2\u2030\u00a1 (r2 `Union` (r1 `Union` Complement r1)) `Intersect`\r\n  ((r1 `Union` r2) `Union` Complement r2) [Axiom 1]\r\n\u00e2\u2030\u00a1 (r2 `Union` (r1 `Union` Complement r1)) `Intersect`\r\n  (r1 `Union` (r2 `Union` Complement r2)) [Axiom 1]\r\n\u00e2\u2030\u00a1 (r2 `Union` univ) `Intersect` (r1 `Union` (r2 `Union` Complement r2)) [Axiom 5]\r\n\u00e2\u2030\u00a1 (r2 `Union` univ) `Intersect` (r1 `Union` univ) [Axiom 5]\r\n\u00e2\u2030\u00a1 univ `Intersect` (r1 `Union` univ) [Lemma 3]\r\n\u00e2\u2030\u00a1 univ `Intersect` univ [Lemma 3]\r\n\u00e2\u2030\u00a1 univ [Lemma 3]\r\n\r\n\u00e2\u02c6\u00b4 X \u00e2\u2030\u00a1 Y\r\n\r\nLemma 10: Complement (r1 `Union` r2) \u00e2\u2030\u00a1 Complement r1 `Intersect` Complement r2\r\n\r\nLet X = Complement (r1 `Intersect` r2)\r\n(r1 `Intersect` r2) `Union` X\r\n\u00e2\u2030\u00a1 (r1 `Intersect` r2) `Union` Complement (r1 `Intersect` r2)\r\n\u00e2\u2030\u00a1 univ [Axiom 5]\r\n\r\nLet Y = Complement r1 `Union` Complement r2\r\n(r1 `Intersect` r2) `Union` Y\r\n\u00e2\u2030\u00a1 (r1 `Intersect` r2) `Union` (Complement r1 `Union` Complement r2)\r\n\u00e2\u2030\u00a1 (r1 `Union` (Complement r1 `Union` Complement r2)) `Intersect`\r\n  (r2 `Union` (Complement r1 `Union` Complement r2)) [Axiom 3]\r\n\u00e2\u2030\u00a1 (r1 `Union` (Complement r1 `Union` Complement r2)) `Intersect`\r\n  ((Complement r1 `Union` Complement r2) `Union` r2) [Axiom 2]\r\n\u00e2\u2030\u00a1 ((r1 `Union` Complement r1) `Union` Complement r2) `Intersect`\r\n  ((Complement r1 `Union` Complement r2) `Union` r2) [Axiom 1]\r\n\u00e2\u2030\u00a1 ((r1 `Union` Complement r1) `Union` Complement r2) `Intersect`\r\n  (Complement r1 `Union` (Complement r2 `Union` r2)) [Axiom 1]\r\n\u00e2\u2030\u00a1 (univ `Union` Complement r2) `Intersect`\r\n  (Complement r1 `Union` (Complement r2 `Union` r2)) [Axiom 5]\r\n\u00e2\u2030\u00a1 (univ `Union` Complement r2) `Intersect`\r\n  (Complement r1 `Union` (r2 `Union` Complement r2)) [Axiom 2]\r\n\u00e2\u2030\u00a1 (univ `Union` Complement r2) `Intersect` (Complement r1 `Union` univ) [Axiom 5]\r\n\u00e2\u2030\u00a1 (univ `Union` Complement r2) `Intersect` univ [Lemma 3]\r\n\u00e2\u2030\u00a1 univ `Union` Complement r2 [Axiom 4]\r\n\u00e2\u2030\u00a1 Complement r2 `Union` univ [Axiom 2]\r\n\u00e2\u2030\u00a1 univ [Lemma 3]\r\n\r\n\u00e2\u02c6\u00b4 X \u00e2\u2030\u00a1 Y\r\n\r\nLemma 11: Complement (r1 `Intersect` r2) \u00e2\u2030\u00a1  Complement r1 `Union` Complement r2<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>Proof from axioms is something that takes great care: it is all too easy to skip a step that &#8220;obviously follows&#8221; from the axioms without proving that step. I&#8217;m not convinced this is all correct&#8230; r \u00e2\u2030\u00a1 r `Intersect` univ [Axiom 4] \u00e2\u2030\u00a1 r `Intersect` (r `Union` Complement r) [Axiom 5] \u00e2\u2030\u00a1 (r `Intersect` r) [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":[],"categories":[1],"tags":[],"_links":{"self":[{"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=\/wp\/v2\/posts\/38"}],"collection":[{"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=38"}],"version-history":[{"count":0,"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=\/wp\/v2\/posts\/38\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=38"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=38"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.elbeno.com\/haskell_soe_blog\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=38"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}