{"id":7448,"date":"2020-10-05T17:35:42","date_gmt":"2020-10-05T15:35:42","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7448"},"modified":"2020-12-20T17:36:21","modified_gmt":"2020-12-20T16:36:21","slug":"formatus-pruebas-en-lean-de-%e2%88%83x-px-%e2%88%a8-qx-%e2%86%94-%e2%88%83x-px-%e2%88%a8-%e2%88%83x-qx","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/formatus-pruebas-en-lean-de-%e2%88%83x-px-%e2%88%a8-qx-%e2%86%94-%e2%88%83x-px-%e2%88%a8-%e2%88%83x-qx\/","title":{"rendered":"ForMatUS: Pruebas en Lean de \u2203x (P(x) \u2228 Q(x)) \u2194 \u2203x P(x) \u2228 \u2203x Q(x)"},"content":{"rendered":"<p>He a\u00f1adido a la lista <a href=\"https:\/\/bit.ly\/2FcUrwQ\">L\u00f3gica con Lean<\/a> el <a href=\"https:\/\/youtu.be\/Ai_IUwbuBBg\">v\u00eddeo<\/a> en el que se comentan pruebas en Lean de la propiedad distributiva del existencial sobre la disyunci\u00f3n<\/p>\n<pre lang=\"lean\">\u2203x (P(x) \u2228 Q(x)) \u2194 \u2203x P(x) \u2228 \u2203x Q(x)\n<\/pre>\n<p>usando los estilos declarativos, aplicativos, funcional y autom\u00e1tico.<\/p>\n<p>A continuaci\u00f3n, se muestra el v\u00eddeo<\/p>\n<p><center><\/p>\n<p><iframe loading=\"lazy\" src=\"https:\/\/www.youtube.com\/embed\/Ai_IUwbuBBg\" width=\"560\" height=\"315\" frameborder=\"0\" allowfullscreen=\"allowfullscreen\" data-mce-fragment=\"1\"><\/iframe><\/p>\n<p><\/center>y el <a href=\"https:\/\/github.com\/jaalonso\/Logica_con_Lean\/blob\/master\/src\/2_LPO\/Pruebas_de_%E2%88%83xP(x)%E2%88%A8%E2%88%83xQ(x)%E2%86%94%E2%88%83x(P(x)%E2%88%A8Q(x)).lean\">c\u00f3digo<\/a> de la teor\u00eda utilizada<\/p>\n<pre lang=\"lean\">import tactic\n\nsection\n\nvariable  {U : Type}\nvariables {P Q : U -&gt; Prop}\n\n-- -----------------------------------------------------\n-- Ej. 1. Demostrar\n--    \u2203x (P(x) \u2228 Q(x)) \u22a2 \u2203x P(x) \u2228 \u2203x Q(x)\n-- -----------------------------------------------------\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (h1 : \u2203x, P x  \u2228 Q x)\n  : (\u2203x, P x) \u2228 (\u2203x, Q x) :=\nexists.elim h1\n  ( assume x\u2080 (h2 : P x\u2080 \u2228 Q x\u2080),\n    or.elim h2\n    ( assume h3 : P x\u2080,\n      have h4 : \u2203x, P x,          from exists.intro x\u2080 h3,\n      show (\u2203x, P x) \u2228 (\u2203x, Q x), from or.inl h4 )\n    ( assume h6 : Q x\u2080,\n      have h7 : \u2203x, Q x,          from exists.intro x\u2080 h6,\n      show (\u2203x, P x) \u2228 (\u2203x, Q x), from or.inr h7 ))\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (h1 : \u2203x, P x  \u2228 Q x)\n  : (\u2203x, P x) \u2228 (\u2203x, Q x) :=\nexists.elim h1\n  ( assume x\u2080 (h2 : P x\u2080 \u2228 Q x\u2080),\n    or.elim h2\n    ( assume h3 : P x\u2080,\n      have h4 : \u2203x, P x,          from \u27e8x\u2080, h3\u27e9,\n      show (\u2203x, P x) \u2228 (\u2203x, Q x), from or.inl h4 )\n    ( assume h6 : Q x\u2080,\n      have h7 : \u2203x, Q x,          from \u27e8x\u2080, h6\u27e9,\n      show (\u2203x, P x) \u2228 (\u2203x, Q x), from or.inr h7 ))\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  (h1 : \u2203x, P x  \u2228 Q x)\n  : (\u2203x, P x) \u2228 (\u2203x, Q x) :=\nexists.elim h1\n  ( assume x\u2080 (h2 : P x\u2080 \u2228 Q x\u2080),\n    or.elim h2\n    ( assume h3 : P x\u2080,\n      have h4 : \u2203x, P x,          from \u27e8x\u2080, h3\u27e9,\n      or.inl h4 )\n    ( assume h6 : Q x\u2080,\n      have h7 : \u2203x, Q x,          from \u27e8x\u2080, h6\u27e9,\n      or.inr h7 ))\n\n-- 4\u00aa demostraci\u00f3n\nexample\n  (h1 : \u2203x, P x  \u2228 Q x)\n  : (\u2203x, P x) \u2228 (\u2203x, Q x) :=\nexists.elim h1\n  ( assume x\u2080 (h2 : P x\u2080 \u2228 Q x\u2080),\n    or.elim h2\n    ( assume h3 : P x\u2080,\n      or.inl \u27e8x\u2080, h3\u27e9 )\n    ( assume h6 : Q x\u2080,\n      or.inr \u27e8x\u2080, h6\u27e9 ))\n\n-- 5\u00aa demostraci\u00f3n\nexample\n  (h1 : \u2203x, P x  \u2228 Q x)\n  : (\u2203x, P x) \u2228 (\u2203x, Q x) :=\nexists.elim h1\n  ( assume x\u2080 (h2 : P x\u2080 \u2228 Q x\u2080),\n    or.elim h2\n    ( \u03bb h3, or.inl \u27e8x\u2080, h3\u27e9 )\n    ( \u03bb h6, or.inr \u27e8x\u2080, h6\u27e9 ))\n\n-- 6\u00aa demostraci\u00f3n\nexample\n  (h1 : \u2203x, P x  \u2228 Q x)\n  : (\u2203x, P x) \u2228 (\u2203x, Q x) :=\nexists.elim h1\n  (\u03bb x\u2080 h2, h2.elim (\u03bb h3, or.inl \u27e8x\u2080, h3\u27e9)\n                    (\u03bb h6, or.inr \u27e8x\u2080, h6\u27e9))\n\n-- 7\u00aa demostraci\u00f3n\nexample\n  (h1 : \u2203x, P x  \u2228 Q x)\n  : (\u2203x, P x) \u2228 (\u2203x, Q x) :=\n-- by library_search\nexists_or_distrib.mp h1\n\n-- 8\u00aa demostraci\u00f3n\nexample\n  (h1 : \u2203x, P x  \u2228 Q x)\n  : (\u2203x, P x) \u2228 (\u2203x, Q x) :=\nmatch h1 with \u27e8x\u2080, (h2 : P x\u2080 \u2228 Q x\u2080)\u27e9 :=\n  ( or.elim h2\n    ( assume h3 : P x\u2080,\n      have h4 : \u2203x, P x,          from exists.intro x\u2080 h3,\n      show (\u2203x, P x) \u2228 (\u2203x, Q x), from or.inl h4 )\n    ( assume h6 : Q x\u2080,\n      have h7 : \u2203x, Q x,          from exists.intro x\u2080 h6,\n      show (\u2203x, P x) \u2228 (\u2203x, Q x), from or.inr h7 ))\nend\n\n-- 9\u00aa demostraci\u00f3n\nexample\n  (h1 : \u2203x, P x  \u2228 Q x)\n  : (\u2203x, P x) \u2228 (\u2203x, Q x) :=\nbegin\n  cases h1 with x\u2080 h3,\n  cases h3 with hp hq,\n  { left,\n    use x\u2080,\n    exact hp, },\n  { right,\n    use x\u2080,\n    exact hq, },\nend\n\n-- 10\u00aa demostraci\u00f3n\nexample\n  (h1 : \u2203x, P x  \u2228 Q x)\n  : (\u2203x, P x) \u2228 (\u2203x, Q x) :=\nbegin\n  rcases h1 with \u27e8x\u2080, hp | hq\u27e9,\n  { left,\n    use x\u2080,\n    exact hp, },\n  { right,\n    use x\u2080,\n    exact hq, },\nend\n\n-- 11\u00aa demostraci\u00f3n\nlemma aux1\n  (h1 : \u2203x, P x  \u2228 Q x)\n  : (\u2203x, P x) \u2228 (\u2203x, Q x) :=\n-- by hint\nby finish\n\n-- -----------------------------------------------------\n-- Ej. 2. Demostrar\n--    \u2203x P(x) \u2228 \u2203x Q(x) \u22a2 \u2203x (P(x) \u2228 Q(x))\n-- -----------------------------------------------------\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (h1 : (\u2203x, P x) \u2228 (\u2203x, Q x))\n  : \u2203x, P x  \u2228 Q x :=\nor.elim h1\n  ( assume h2 : \u2203x, P x,\n    exists.elim h2\n      ( assume x\u2080 (h3 : P x\u2080),\n        have h4 : P x\u2080 \u2228 Q x\u2080, from or.inl h3,\n        show \u2203x, P x  \u2228 Q x,   from exists.intro x\u2080 h4 ))\n  ( assume h2 : \u2203x, Q x,\n    exists.elim h2\n      ( assume x\u2080 (h3 : Q x\u2080),\n        have h4 : P x\u2080 \u2228 Q x\u2080, from or.inr h3,\n        show \u2203x, P x  \u2228 Q x,   from exists.intro x\u2080 h4 ))\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (h1 : (\u2203x, P x) \u2228 (\u2203x, Q x))\n  : \u2203x, P x  \u2228 Q x :=\nh1.elim\n  ( assume \u27e8x\u2080, (h3 : P x\u2080)\u27e9,\n    have h4 : P x\u2080 \u2228 Q x\u2080, from or.inl h3,\n    show \u2203x, P x  \u2228 Q x,   from \u27e8x\u2080, h4\u27e9 )\n  ( assume \u27e8x\u2080, (h3 : Q x\u2080)\u27e9,\n    have h4 : P x\u2080 \u2228 Q x\u2080, from or.inr h3,\n    show \u2203x, P x  \u2228 Q x,   from \u27e8x\u2080, h4\u27e9 )\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  (h1 : (\u2203x, P x) \u2228 (\u2203x, Q x))\n  : \u2203x, P x  \u2228 Q x :=\nh1.elim\n  ( assume \u27e8x\u2080, (h3 : P x\u2080)\u27e9,\n    have h4 : P x\u2080 \u2228 Q x\u2080, from or.inl h3,\n    \u27e8x\u2080, h4\u27e9 )\n  ( assume \u27e8x\u2080, (h3 : Q x\u2080)\u27e9,\n    have h4 : P x\u2080 \u2228 Q x\u2080, from or.inr h3,\n    \u27e8x\u2080, h4\u27e9 )\n\n-- 4\u00aa demostraci\u00f3n\nexample\n  (h1 : (\u2203x, P x) \u2228 (\u2203x, Q x))\n  : \u2203x, P x  \u2228 Q x :=\nh1.elim\n  ( assume \u27e8x\u2080, (h3 : P x\u2080)\u27e9,\n    \u27e8x\u2080, or.inl h3\u27e9 )\n  ( assume \u27e8x\u2080, (h3 : Q x\u2080)\u27e9,\n    \u27e8x\u2080, or.inr h3\u27e9 )\n\n-- 5\u00aa demostraci\u00f3n\nexample\n  (h1 : (\u2203x, P x) \u2228 (\u2203x, Q x))\n  : \u2203x, P x  \u2228 Q x :=\nh1.elim\n  (\u03bb \u27e8x\u2080, h3\u27e9, \u27e8x\u2080, or.inl h3\u27e9)\n  (\u03bb \u27e8x\u2080, h3\u27e9, \u27e8x\u2080, or.inr h3\u27e9)\n\n-- 6\u00aa demostraci\u00f3n\nexample\n  (h1 : (\u2203x, P x) \u2228 (\u2203x, Q x))\n  : \u2203x, P x  \u2228 Q x :=\n-- by library_search\nexists_or_distrib.mpr h1\n\n-- 7\u00aa demostraci\u00f3n\nexample\n  (h1 : (\u2203x, P x) \u2228 (\u2203x, Q x))\n  : \u2203x, P x  \u2228 Q x :=\nbegin\n  cases h1 with hp hq,\n  { cases hp with x\u2080 hx\u2080,\n    use x\u2080,\n    left,\n    exact hx\u2080, },\n  { cases hq with x\u2081 hx\u2081,\n    use x\u2081,\n    right,\n    exact hx\u2081, },\nend\n\n-- 8\u00aa demostraci\u00f3n\nexample\n  (h1 : (\u2203x, P x) \u2228 (\u2203x, Q x))\n  : \u2203x, P x  \u2228 Q x :=\nbegin\n  rcases h1 with \u27e8x\u2080, hx\u2080\u27e9 | \u27e8x\u2081, hx\u2081\u27e9,\n  { use x\u2080,\n    left,\n    exact hx\u2080, },\n  { use x\u2081,\n    right,\n    exact hx\u2081, },\nend\n\n-- 9\u00aa demostraci\u00f3n\nlemma aux2\n  (h1 : (\u2203x, P x) \u2228 (\u2203x, Q x))\n  : \u2203x, P x  \u2228 Q x :=\n-- by hint\nby finish\n\n-- -----------------------------------------------------\n-- Ej. 3. Demostrar\n--    \u2203x (P(x) \u2228 Q(x)) \u2194 \u2203x P(x) \u2228 \u2203x Q(x)\n-- -----------------------------------------------------\n\n-- 1\u00aa demostraci\u00f3n\nexample :\n  (\u2203x, P x  \u2228 Q x) \u2194 (\u2203x, P x) \u2228 (\u2203x, Q x) :=\niff.intro aux1 aux2\n\n-- 2\u00aa demostraci\u00f3n\nexample :\n  (\u2203x, P x  \u2228 Q x) \u2194 (\u2203x, P x) \u2228 (\u2203x, Q x) :=\n\u27e8aux1, aux2\u27e9\n\n-- 3\u00aa demostraci\u00f3n\nexample :\n  (\u2203x, P x  \u2228 Q x) \u2194 (\u2203x, P x) \u2228 (\u2203x, Q x) :=\n-- by library_search\nexists_or_distrib\n\nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"<p>He a\u00f1adido a la lista L\u00f3gica con Lean el v\u00eddeo en el que se comentan pruebas en Lean de la propiedad distributiva del existencial sobre la disyunci\u00f3n \u2203x (P(x) \u2228 Q(x)) \u2194 \u2203x P(x) \u2228 \u2203x Q(x) usando los estilos declarativos, aplicativos, funcional y autom\u00e1tico. A continuaci\u00f3n, se muestra el v\u00eddeo y el c\u00f3digo de&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[335],"tags":[336],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7448"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=7448"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7448\/revisions"}],"predecessor-version":[{"id":7449,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7448\/revisions\/7449"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7448"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7448"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7448"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}