{"id":7394,"date":"2020-09-20T12:09:16","date_gmt":"2020-09-20T10:09:16","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7394"},"modified":"2020-12-20T12:10:40","modified_gmt":"2020-12-20T11:10:40","slug":"formatus-reglas-de-introduccion-de-la-disyuncion-en-lean","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/formatus-reglas-de-introduccion-de-la-disyuncion-en-lean\/","title":{"rendered":"ForMatUS: Reglas de introducci\u00f3n de la disyunci\u00f3n 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\/vJzydeiWvOc\">v\u00eddeo<\/a> en el que se comentan el uso en Lean de las reglas de introducci\u00f3n de la disyunci\u00f3n con ejemplos de pruebas en 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\/vJzydeiWvOc\" width=\"560\" height=\"315\" frameborder=\"0\" allowfullscreen=\"allowfullscreen\" data-mce-fragment=\"1\"><\/iframe><\/p>\n<p><\/center>y el c\u00f3digo de la teor\u00eda utilizada<\/p>\n<pre lang=\"lean\">import tactic\n\nvariables (P Q R : Prop)\n\n-- ----------------------------------------------------\n-- Ej. 1. (p. 11) Demostrar\n--    P \u22a2 P \u2228 Q\n-- ----------------------------------------------------\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (h : P)\n  : P \u2228 Q :=\nor.intro_left Q h\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (h : P)\n  : P \u2228 Q :=\n-- by library_search\nor.inl h\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  (h : P)\n  : P \u2228 Q :=\n-- by hint\nby tauto\n\n-- 4\u00aa demostraci\u00f3n\nexample\n  (h : P)\n  : P \u2228 Q :=\nby finish\n\n-- ----------------------------------------------------\n-- Ej. 2. Demostrar\n--    P \u2227 Q \u22a2 P \u2228 R\n-- ----------------------------------------------------\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (h1 : P \u2227 Q)\n  : P \u2228 R :=\nhave h2 : P,\n  from and.elim_left h1,\nshow P \u2228 R,\n  from or.inl h2\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (h1 : P \u2227 Q)\n  : P \u2228 R :=\nhave h2 : P,\n  from h1.1,\nshow P \u2228 R,\n  from or.inl h2\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  (h1 : P \u2227 Q)\n  : P \u2228 R :=\nhave h2 : P := h1.1,\nshow P \u2228 R,\n  from or.inl h2\n\n-- 4\u00aa demostraci\u00f3n\nexample\n  (h1 : P \u2227 Q)\n  : P \u2228 R :=\nshow P \u2228 R,\n  from or.inl h1.1\n\n-- 5\u00aa demostraci\u00f3n\nexample\n  (h1 : P \u2227 Q)\n  : P \u2228 R :=\n-- by suggest\nor.inl h1.1\n\n-- 6\u00aa demostraci\u00f3n\nexample\n  (h1 : P \u2227 Q)\n  : P \u2228 R :=\n-- by hint\nby tauto\n\n-- 7\u00aa demostraci\u00f3n\nexample\n  (h1 : P \u2227 Q)\n  : P \u2228 R :=\nby finish\n\n-- ----------------------------------------------------\n-- Ej. 3. Demostrar\n--    Q \u22a2 P \u2228 Q\n-- ----------------------------------------------------\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (h : Q)\n  : P \u2228 Q :=\nor.intro_right P h\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (h : Q)\n  : P \u2228 Q :=\n-- by suggest\nor.inr h\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  (h : Q)\n  : P \u2228 Q :=\n-- by hint\nby tauto\n\n-- 4\u00aa demostraci\u00f3n\nexample\n  (h : Q)\n  : P \u2228 Q :=\nby finish\n\n-- ----------------------------------------------------\n-- Ej. 4. Demostrar\n--    P \u2227 Q \u22a2 R \u2228 Q\n-- ----------------------------------------------------\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (h1 : P \u2227 Q)\n  : R \u2228 Q :=\nhave h2 : Q,\n  from and.elim_right h1,\nshow R \u2228 Q,\n  from or.inr h2\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (h1 : P \u2227 Q)\n  : R \u2228 Q :=\nhave h2 : Q,\n  from h1.2,\nshow R \u2228 Q,\n  from or.inr h2\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  (h1 : P \u2227 Q)\n  : R \u2228 Q :=\nhave h2 : Q := h1.2,\nshow R \u2228 Q,\n  from or.inr h2\n\n-- 4\u00aa demostraci\u00f3n\nexample\n  (h1 : P \u2227 Q)\n  : R \u2228 Q :=\nshow R \u2228 Q,\n  from or.inr h1.2\n\n-- 5\u00aa demostraci\u00f3n\nexample\n  (h1 : P \u2227 Q)\n  : R \u2228 Q :=\n-- by suggest\nor.inr h1.2\n\n-- 6\u00aa demostraci\u00f3n\nexample\n  (h1 : P \u2227 Q)\n  : R \u2228 Q :=\n-- by hint\nby tauto\n\n-- 7\u00aa demostraci\u00f3n\nexample\n  (h1 : P \u2227 Q)\n  : R \u2228 Q :=\nby finish\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 el uso en Lean de las reglas de introducci\u00f3n de la disyunci\u00f3n con ejemplos de pruebas en 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 variables&#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":[],"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\/7394"}],"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=7394"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7394\/revisions"}],"predecessor-version":[{"id":7395,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7394\/revisions\/7395"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7394"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7394"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7394"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}