{"id":7435,"date":"2020-10-01T17:06:44","date_gmt":"2020-10-01T15:06:44","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7435"},"modified":"2020-12-20T17:08:10","modified_gmt":"2020-12-20T16:08:10","slug":"formatus-regla-de-eliminacion-del-cuantificador-universal-en-lean","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/formatus-regla-de-eliminacion-del-cuantificador-universal-en-lean\/","title":{"rendered":"ForMatUS: Regla de eliminaci\u00f3n del cuantificador universal en Lean"},"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\/fy_2FThFvyo\">v\u00eddeo<\/a> en el que se comentan ??? pruebas en Lean de la propiedad<\/p>\n<pre lang=\"lean\">P(c), \u2200x (P(x) \u2192 \u00acQ(x)) \u22a2 \u00acQ(c)\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\/fy_2FThFvyo\" 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\/Regla_de_eliminacion_del_cuantificador_universal.lean\">c\u00f3digo<\/a> de la teor\u00eda utilizada<\/p>\n<pre lang=\"lean\">-- Ej. 1. Demostrar\n--    P(c), \u2200x (P(x) \u2192 \u00acQ(x)) \u22a2 \u00acQ(c)\n\nimport tactic\n\nvariable  U : Type\nvariable  c : U\nvariables P Q : U \u2192 Prop\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (h1 : P c)\n  (h2 : \u2200x, P x \u2192 \u00acQ x)\n  : \u00acQ c :=\nhave h3 : P c \u2192 \u00acQ c, from h2 c,\nshow \u00acQ c,            from h3 h1\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (h1 : P c)\n  (h2 : \u2200x, P x \u2192 \u00acQ x)\n  : \u00acQ c :=\nhave h3 : P c \u2192 \u00acQ c, from h2 c,\nh3 h1\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  (h1 : P c)\n  (h2 : \u2200x, P x \u2192 \u00acQ x)\n  : \u00acQ c :=\n(h2 c) h1\n\n-- 4\u00aa demostraci\u00f3n\nexample\n  (h1 : P c)\n  (h2 : \u2200x, P x \u2192 \u00acQ x)\n  : \u00acQ c :=\n-- by library_search\nh2 c h1\n\n-- 5\u00aa demostraci\u00f3n\nexample\n  (h1 : P c)\n  (h2 : \u2200x, P x \u2192 \u00acQ x)\n  : \u00acQ c :=\n-- by hint\nby tauto\n\n-- 6\u00aa demostraci\u00f3n\nexample\n  (h1 : P c)\n  (h2 : \u2200x, P x \u2192 \u00acQ x)\n  : \u00acQ c :=\nby finish\n\n-- 7\u00aa demostraci\u00f3n\nexample\n  (h1 : P c)\n  (h2 : \u2200x, P x \u2192 \u00acQ x)\n  : \u00acQ c :=\nbegin\n  apply h2,\n  exact h1,\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 P(c), \u2200x (P(x) \u2192 \u00acQ(x)) \u22a2 \u00acQ(c) 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 &#8212; Ej. 1. Demostrar &#8211;&#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\/7435"}],"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=7435"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7435\/revisions"}],"predecessor-version":[{"id":7436,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7435\/revisions\/7436"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7435"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7435"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7435"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}