{"id":7446,"date":"2020-10-03T17:29:38","date_gmt":"2020-10-03T15:29:38","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7446"},"modified":"2020-12-20T17:30:23","modified_gmt":"2020-12-20T16:30:23","slug":"formatus-pruebas-en-lean-de-%e2%88%80x-px-%e2%88%a7-qx-%e2%86%94-%e2%88%80x-px-%e2%88%a7-%e2%88%80x-qx","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/formatus-pruebas-en-lean-de-%e2%88%80x-px-%e2%88%a7-qx-%e2%86%94-%e2%88%80x-px-%e2%88%a7-%e2%88%80x-qx\/","title":{"rendered":"ForMatUS: Pruebas en Lean de \u2200x (P(x) \u2227 Q(x)) \u2194 \u2200x P(x) \u2227 \u2200x 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\/buEuarWb7QU\">v\u00eddeo<\/a> en el que se comentan pruebas en Lean de la propiedad<\/p>\n<pre lang=\"lean\">\u2200x (P(x) \u2227 Q(x)) \u2194 \u2200x P(x) \u2227 \u2200x 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\/buEuarWb7QU\" 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%80x(P(x)%E2%88%A7Q(x))%E2%86%94%E2%88%80xP(x)%E2%88%A7%E2%88%80xQ(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--    \u2200x (P(x) \u2227 Q(x)) \u22a2 \u2200x P(x) \u2227 \u2200x Q(x)\n-- ------------------------------------------------------\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (h1 : \u2200x, P x \u2227 Q x)\n  : (\u2200x, P x) \u2227 (\u2200x, Q x) :=\nhave h5 : \u2200x, P x, from\n    assume x\u2080,\n    have h3 : P x\u2080 \u2227 Q x\u2080,  from h1 x\u2080,\n    show P x\u2080,              from and.elim_left h3,\nhave h9 : \u2200x, Q x, from\n    assume x\u2081,\n    have h7 : P x\u2081 \u2227 Q x\u2081,  from h1 x\u2081,\n    show Q x\u2081,              from and.elim_right h7,\nshow (\u2200x, P x) \u2227 (\u2200x, Q x), from and.intro h5 h9\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (h1 : \u2200x, P x \u2227 Q x)\n  : (\u2200x, P x) \u2227 (\u2200x, Q x) :=\nhave h5 : \u2200x, P x, from\n    assume x\u2080,\n    have h3 : P x\u2080 \u2227 Q x\u2080,  from h1 x\u2080,\n    show P x\u2080,              from h3.left,\nhave h9 : \u2200x, Q x, from\n    assume x\u2081,\n    have h7 : P x\u2081 \u2227 Q x\u2081,  from h1 x\u2081,\n    show Q x\u2081,              from h7.right,\nshow (\u2200x, P x) \u2227 (\u2200x, Q x), from \u27e8h5, h9\u27e9\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  (h1 : \u2200x, P x \u2227 Q x)\n  : (\u2200x, P x) \u2227 (\u2200x, Q x) :=\nhave h5 : \u2200x, P x, from\n    assume x\u2080,\n    have h3 : P x\u2080 \u2227 Q x\u2080,  from h1 x\u2080,\n    h3.left,\nhave h9 : \u2200x, Q x, from\n    assume x\u2081,\n    have h7 : P x\u2081 \u2227 Q x\u2081,  from h1 x\u2081,\n    h7.right,\nshow (\u2200x, P x) \u2227 (\u2200x, Q x), from \u27e8h5, h9\u27e9\n\n-- 4\u00aa demostraci\u00f3n\nexample\n  (h1 : \u2200x, P x \u2227 Q x)\n  : (\u2200x, P x) \u2227 (\u2200x, Q x) :=\nhave h5 : \u2200x, P x, from\n    assume x\u2080,\n    (h1 x\u2080).left,\nhave h9 : \u2200x, Q x, from\n    assume x\u2081,\n    (h1 x\u2081).right,\nshow (\u2200x, P x) \u2227 (\u2200x, Q x), from \u27e8h5, h9\u27e9\n\n-- 5\u00aa demostraci\u00f3n\nexample\n  (h1 : \u2200x, P x \u2227 Q x)\n  : (\u2200x, P x) \u2227 (\u2200x, Q x) :=\nhave h5 : \u2200x, P x, from\n    \u03bb x\u2080, (h1 x\u2080).left,\nhave h9 : \u2200x, Q x, from\n    \u03bb x\u2081, (h1 x\u2081).right,\nshow (\u2200x, P x) \u2227 (\u2200x, Q x), from \u27e8h5, h9\u27e9\n\n-- 6\u00aa demostraci\u00f3n\nexample\n  (h1 : \u2200x, P x \u2227 Q x)\n  : (\u2200x, P x) \u2227 (\u2200x, Q x) :=\nhave h5 : \u2200x, P x, from\n    \u03bb x\u2080, (h1 x\u2080).left,\nhave h9 : \u2200x, Q x, from\n    \u03bb x\u2081, (h1 x\u2081).right,\n\u27e8h5, h9\u27e9\n\n-- 7\u00aa demostraci\u00f3n\nexample\n  (h1 : \u2200x, P x \u2227 Q x)\n  : (\u2200x, P x) \u2227 (\u2200x, Q x) :=\n\u27e8\u03bb x\u2080, (h1 x\u2080).left, \u03bb x\u2081, (h1 x\u2081).right\u27e9\n\n-- 8\u00aa demostraci\u00f3n\nexample\n  (h1 : \u2200x, P x \u2227 Q x)\n  : (\u2200x, P x) \u2227 (\u2200x, Q x) :=\n-- by library_search\nforall_and_distrib.mp h1\n\n-- 9\u00aa demostraci\u00f3n\nexample\n  (h1 : \u2200x, P x \u2227 Q x)\n  : (\u2200x, P x) \u2227 (\u2200x, Q x) :=\nbegin\n  split,\n  { intro x\u2080,\n    specialize h1 x\u2080,\n    exact h1.left, },\n  { intro x\u2081,\n    specialize h1 x\u2081,\n    exact h1.right, },\nend\n\n-- 9\u00aa demostraci\u00f3n\nlemma aux1\n  (h1 : \u2200x, P x \u2227 Q x)\n  : (\u2200x, P x) \u2227 (\u2200x, Q x) :=\n-- by hint\nby finish\n\n-- ------------------------------------------------------\n-- Ej. 2. Demostrar\n--    \u2200x P(x) \u2227 \u2200x Q(x) \u22a2 \u2200x (P(x) \u2227 Q(x))\n-- ------------------------------------------------------\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (h1 : (\u2200x, P x) \u2227 (\u2200x, Q x))\n  : \u2200x, P x \u2227 Q x :=\nassume x\u2080,\nhave h3 : \u2200x, P x, from and.elim_left h1,\nhave h4 : P x\u2080,    from h3 x\u2080,\nhave h5 : \u2200x, Q x, from and.elim_right h1,\nhave h6 : Q x\u2080,    from h5 x\u2080,\nshow P x\u2080 \u2227 Q x\u2080,  from and.intro h4 h6\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (h1 : (\u2200x, P x) \u2227 (\u2200x, Q x))\n  : \u2200x, P x \u2227 Q x :=\nassume x\u2080,\nhave h3 : \u2200x, P x, from h1.left,\nhave h4 : P x\u2080,    from h3 x\u2080,\nhave h5 : \u2200x, Q x, from h1.right,\nhave h6 : Q x\u2080,    from h5 x\u2080,\nshow P x\u2080 \u2227 Q x\u2080,  from \u27e8h4, h6\u27e9\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  (h1 : (\u2200x, P x) \u2227 (\u2200x, Q x))\n  : \u2200x, P x \u2227 Q x :=\nassume x\u2080,\nhave h3 : \u2200x, P x, from h1.left,\nhave h4 : P x\u2080,    from h3 x\u2080,\nhave h5 : \u2200x, Q x, from h1.right,\nhave h6 : Q x\u2080,    from h5 x\u2080,\n\u27e8h4, h6\u27e9\n\n-- 4\u00aa demostraci\u00f3n\nexample\n  (h1 : (\u2200x, P x) \u2227 (\u2200x, Q x))\n  : \u2200x, P x \u2227 Q x :=\nassume x\u2080,\nhave h3 : \u2200x, P x, from h1.left,\nhave h4 : P x\u2080,    from h3 x\u2080,\nhave h5 : \u2200x, Q x, from h1.right,\n\u27e8h4, h5 x\u2080\u27e9\n\n-- 5\u00aa demostraci\u00f3n\nexample\n  (h1 : (\u2200x, P x) \u2227 (\u2200x, Q x))\n  : \u2200x, P x \u2227 Q x :=\nassume x\u2080,\nhave h3 : \u2200x, P x, from h1.left,\nhave h4 : P x\u2080,    from h3 x\u2080,\n\u27e8h4, h1.right x\u2080\u27e9\n\n-- 6\u00aa demostraci\u00f3n\nexample\n  (h1 : (\u2200x, P x) \u2227 (\u2200x, Q x))\n  : \u2200x, P x \u2227 Q x :=\nassume x\u2080,\nhave h3 : \u2200x, P x, from h1.left,\n\u27e8h3 x\u2080, h1.right x\u2080\u27e9\n\n-- 7\u00aa demostraci\u00f3n\nexample\n  (h1 : (\u2200x, P x) \u2227 (\u2200x, Q x))\n  : \u2200x, P x \u2227 Q x :=\nassume x\u2080,\n\u27e8h1.left x\u2080, h1.right x\u2080\u27e9\n\n-- 8\u00aa demostraci\u00f3n\nexample\n  (h1 : (\u2200x, P x) \u2227 (\u2200x, Q x))\n  : \u2200x, P x \u2227 Q x :=\n\u03bb x\u2080, \u27e8h1.left x\u2080, h1.right x\u2080\u27e9\n\n-- 9\u00aa demostraci\u00f3n\nexample\n  (h1 : (\u2200x, P x) \u2227 (\u2200x, Q x))\n  : \u2200x, P x \u2227 Q x :=\n-- by library_search\nforall_and_distrib.mpr h1\n\n-- 10\u00aa demostraci\u00f3n\nexample\n  (h1 : (\u2200x, P x) \u2227 (\u2200x, Q x))\n  : \u2200x, P x \u2227 Q x :=\nbegin\n  cases h1 with h2 h3,\n  intro x\u2080,\n  split,\n  { apply h2, },\n  { apply h3, },\nend\n\n-- 11\u00aa demostraci\u00f3n\nexample\n  (h1 : (\u2200x, P x) \u2227 (\u2200x, Q x))\n  : \u2200x, P x \u2227 Q x :=\n-- by hint\nby tauto\n\n-- 12\u00aa demostraci\u00f3n\nlemma aux2\n  (h1 : (\u2200x, P x) \u2227 (\u2200x, Q x))\n  : \u2200x, P x \u2227 Q x :=\nby finish\n\n-- ------------------------------------------------------\n-- Ej. 3. Demostrar\n--    \u2200x (P(x) \u2227 Q(x)) \u2194 \u2200x P(x) \u2227 \u2200x Q(x)\n-- ------------------------------------------------------\n\n-- 1\u00aa demostraci\u00f3n\nexample :\n  (\u2200x, P x \u2227 Q x) \u2194 (\u2200x, P x) \u2227 (\u2200x, Q x) :=\niff.intro aux1 aux2\n\n-- 2\u00aa demostraci\u00f3n\nexample :\n  (\u2200x, P x \u2227 Q x) \u2194 (\u2200x, P x) \u2227 (\u2200x, Q x) :=\n-- by library_search\nforall_and_distrib\n\n-- 3\u00aa demostraci\u00f3n\nexample :\n  (\u2200x, P x \u2227 Q x) \u2194 (\u2200x, P x) \u2227 (\u2200x, Q x) :=\n-- by hint\nby finish\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 \u2200x (P(x) \u2227 Q(x)) \u2194 \u2200x P(x) \u2227 \u2200x Q(x) usando los estilos declarativos, aplicativos, funcional y autom\u00e1tico. A continuaci\u00f3n, se muestra el v\u00eddeo y el c\u00f3digo de la teor\u00eda utilizada import tactic section&#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\/7446"}],"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=7446"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7446\/revisions"}],"predecessor-version":[{"id":7447,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7446\/revisions\/7447"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7446"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7446"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7446"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}