{"id":608,"date":"2021-07-28T12:54:50","date_gmt":"2021-07-28T10:54:50","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=608"},"modified":"2021-07-28T12:54:50","modified_gmt":"2021-07-28T10:54:50","slug":"propiedad-cancelativa-del-producto-de-numeros-naturales","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/propiedad-cancelativa-del-producto-de-numeros-naturales\/","title":{"rendered":"Propiedad cancelativa del producto de n\u00fameros naturales"},"content":{"rendered":"<p>Sean k, m, n n\u00fameros naturales. Demostrar que<\/p>\n<pre lang=\"text\">\n   k * m = k * n \u2194 m = n \u2228 k = 0\n<\/pre>\n<p>Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n<pre lang=\"lean\">\nimport data.nat.basic\nopen nat\n\nvariables {k m n : \u2115}\n\nexample :\n  k * m = k * n \u2194 m = n \u2228 k = 0 :=\nsorry\n<\/pre>\n<p>[expand title=\u00bbSoluciones con Lean\u00bb]<\/p>\n<pre lang=\"lean\">\r\nimport data.nat.basic\r\nopen nat\r\n\r\nvariables {k m n : \u2115}\r\n\r\n-- Para que no use la notaci\u00f3n con puntos\r\nset_option pp.structure_projections false\r\n\r\n-- 1\u00aa demostraci\u00f3n\r\nexample :\r\n  k * m = k * n \u2194 m = n \u2228 k = 0 :=\r\nbegin\r\n  have h1: k \u2260 0 \u2192 k * m = k * n \u2192 m = n,\r\n    { induction n with n HI generalizing m,\r\n      { by finish, },\r\n      { cases m,\r\n        { by finish, },\r\n        { intros hk hS,\r\n          congr,\r\n          apply HI hk,\r\n          rw mul_succ at hS,\r\n          rw mul_succ at hS,\r\n          exact add_right_cancel hS, }}},\r\n  by finish,\r\nend\r\n\r\n-- 2\u00aa demostraci\u00f3n\r\nexample :\r\n  k * m = k * n \u2194 m = n \u2228 k = 0 :=\r\nbegin\r\n  have h1: k \u2260 0 \u2192 k * m = k * n \u2192 m = n,\r\n    { induction n with n HI generalizing m,\r\n      { by finish, },\r\n      { cases m,\r\n        { by finish, },\r\n        { intros hk hS,\r\n          congr,\r\n          apply HI hk,\r\n          simp only [mul_succ] at hS,\r\n          exact add_right_cancel hS, }}},\r\n  by finish,\r\nend\r\n\r\n-- 3\u00aa demostraci\u00f3n\r\nexample :\r\n  k * m = k * n \u2194 m = n \u2228 k = 0 :=\r\nbegin\r\n  have h1: k \u2260 0 \u2192 k * m = k * n \u2192 m = n,\r\n    { induction n with n HI generalizing m,\r\n      { by finish, },\r\n      { cases m,\r\n        { by finish, },\r\n        { by finish, }}},\r\n  by finish,\r\nend\r\n\r\n-- 4\u00aa demostraci\u00f3n\r\nexample :\r\n  k * m = k * n \u2194 m = n \u2228 k = 0 :=\r\nbegin\r\n  have h1: k \u2260 0 \u2192 k * m = k * n \u2192 m = n,\r\n    { induction n with n HI generalizing m,\r\n      { by finish, },\r\n      { cases m; by finish }},\r\n  by finish,\r\nend\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\nexample :\r\n  k * m = k * n \u2194 m = n \u2228 k = 0 :=\r\nbegin\r\n  have h1: k \u2260 0 \u2192 k * m = k * n \u2192 m = n,\r\n    { induction n with n HI generalizing m ; by finish },\r\n  by finish,\r\nend\r\n\r\n-- 5\u00aa demostraci\u00f3n\r\nexample :\r\n  k * m = k * n \u2194 m = n \u2228 k = 0 :=\r\nbegin\r\n  by_cases hk : k = 0,\r\n  { by simp, },\r\n  { rw mul_right_inj' hk,\r\n    by tauto, },\r\nend\r\n\r\n-- 6\u00aa demostraci\u00f3n\r\nexample :\r\n  k * m = k * n \u2194 m = n \u2228 k = 0 :=\r\nmul_eq_mul_left_iff\r\n\r\n-- 7\u00aa demostraci\u00f3n\r\nexample :\r\n  k * m = k * n \u2194 m = n \u2228 k = 0 :=\r\nby simp\r\n<\/pre>\n<p>Se puede interactuar con la prueba anterior en <a href=\"https:\/\/leanprover-community.github.io\/lean-web-editor\/#url=https:\/\/raw.githubusercontent.com\/jaalonso\/Calculemus\/main\/src\/Propiedad_cancelativa_del_producto_de_numeros_naturales.lean\" rel=\"noopener noreferrer\" target=\"_blank\">esta sesi\u00f3n con Lean<\/a>.<\/p>\n<p>En los comentarios se pueden escribir otras soluciones, escribiendo el c\u00f3digo entre una l\u00ednea con &#60;pre lang=&quot;lean&quot;&#62; y otra con &#60;\/pre&#62;<br \/>\n[\/expand]<\/p>\n<p>[expand title=\u00bbSoluciones con Isabelle\/HOL\u00bb]<\/p>\n<pre lang=\"isar\">\r\ntheory Propiedad_cancelativa_del_producto_de_numeros_naturales\r\nimports Main\r\nbegin\r\n\r\n(* 1\u00aa demostraci\u00f3n *)\r\nlemma\r\n  fixes k m n :: nat\r\n  shows \"k * m = k * n \u27f7 m = n \u2228 k = 0\"\r\nproof -\r\n  have \"k \u2260 0 \u27f9 k * m = k * n \u27f9 m = n\"\r\n  proof (induct n arbitrary: m)\r\n    fix m\r\n    assume \"k \u2260 0\" and \"k * m = k * 0\"\r\n    show \"m = 0\"\r\n      using \u2039k * m = k * 0\u203a\r\n      by (simp only: mult_left_cancel[OF \u2039k \u2260 0\u203a])\r\n  next\r\n    fix n m\r\n    assume HI : \"\u22c0m. \u27e6k \u2260 0; k * m = k * n\u27e7 \u27f9 m = n\"\r\n       and hk : \"k \u2260 0\"\r\n       and \"k * m = k * Suc n\"\r\n    then show \"m = Suc n\"\r\n    proof (cases m)\r\n      assume \"m = 0\"\r\n      then show \"m = Suc n\"\r\n        using \u2039k * m = k * Suc n\u203a\r\n        by (simp only: mult_left_cancel[OF \u2039k \u2260 0\u203a])\r\n    next\r\n      fix m'\r\n      assume \"m = Suc m'\"\r\n      then have \"k * Suc m' = k * Suc n\"\r\n        using \u2039k * m = k * Suc n\u203a by (rule subst)\r\n      then have \"k * m' + k = k * n + k\"\r\n        by (simp only: mult_Suc_right)\r\n      then have \"k * m' = k * n\"\r\n        by (simp only: add_right_imp_eq)\r\n      then have \"m' = n\"\r\n        by (simp only: HI[OF hk])\r\n      then show \"m = Suc n\"\r\n        by (simp only: \u2039m = Suc m'\u203a)\r\n    qed\r\n  qed\r\n  then show \"k * m = k * n \u27f7 m = n \u2228 k = 0\"\r\n    by auto\r\nqed\r\n\r\n(* 2\u00aa demostraci\u00f3n *)\r\nlemma\r\n  fixes k m n :: nat\r\n  shows \"k * m = k * n \u27f7 m = n \u2228 k = 0\"\r\nproof -\r\n  have \"k \u2260 0 \u27f9 k * m = k * n \u27f9 m = n\"\r\n  proof (induct n arbitrary: m)\r\n    fix m\r\n    assume \"k \u2260 0\" and \"k * m = k * 0\"\r\n    then show \"m = 0\" by simp\r\n  next\r\n    fix n m\r\n    assume \"\u22c0m. \u27e6k \u2260 0; k * m = k * n\u27e7 \u27f9 m = n\"\r\n       and \"k \u2260 0\"\r\n       and \"k * m = k * Suc n\"\r\n    then show \"m = Suc n\"\r\n    proof (cases m)\r\n      assume \"m = 0\"\r\n      then show \"m = Suc n\"\r\n        using \u2039k * m = k * Suc n\u203a \u2039k \u2260 0\u203a by auto\r\n    next\r\n      fix m'\r\n      assume \"m = Suc m'\"\r\n      then show \"m = Suc n\"\r\n        using \u2039k * m = k * Suc n\u203a \u2039k \u2260 0\u203a by force\r\n    qed\r\n  qed\r\n  then show \"k * m = k * n \u27f7 m = n \u2228 k = 0\" by auto\r\nqed\r\n\r\n(* 3\u00aa demostraci\u00f3n *)\r\nlemma\r\n  fixes k m n :: nat\r\n  shows \"k * m = k * n \u27f7 m = n \u2228 k = 0\"\r\nproof -\r\n  have \"k \u2260 0 \u27f9 k * m = k * n \u27f9 m = n\"\r\n  proof (induct n arbitrary: m)\r\n    case 0\r\n    then show ?case\r\n      by simp\r\n  next\r\n    case (Suc n)\r\n    then show ?case\r\n    proof (cases m)\r\n      case 0\r\n      then show ?thesis\r\n        using Suc.prems by auto\r\n    next\r\n      case (Suc nat)\r\n      then show ?thesis\r\n        using Suc.prems by auto\r\n    qed\r\n  qed\r\n  then show ?thesis\r\n    by auto\r\nqed\r\n\r\n(* 4\u00aa demostraci\u00f3n *)\r\nlemma\r\n  fixes k m n :: nat\r\n  shows \"k * m = k * n \u27f7 m = n \u2228 k = 0\"\r\nproof -\r\n  have \"k \u2260 0 \u27f9 k * m = k * n \u27f9 m = n\"\r\n  proof (induct n arbitrary: m)\r\n    case 0\r\n    then show \"m = 0\" by simp\r\n  next\r\n    case (Suc n)\r\n    then show \"m = Suc n\"\r\n      by (cases m) (simp_all add: eq_commute [of 0])\r\n  qed\r\n  then show ?thesis by auto\r\nqed\r\n\r\n(* 5\u00aa demostraci\u00f3n *)\r\nlemma\r\n  fixes k m n :: nat\r\n  shows \"k * m = k * n \u27f7 m = n \u2228 k = 0\"\r\nby (simp only: mult_cancel1)\r\n\r\n(* 6\u00aa demostraci\u00f3n *)\r\nlemma\r\n  fixes k m n :: nat\r\n  shows \"k * m = k * n \u27f7 m = n \u2228 k = 0\"\r\nby simp\r\n\r\nend\r\n<\/pre>\n<p>En los comentarios se pueden escribir otras soluciones, escribiendo el c\u00f3digo entre una l\u00ednea con &#60;pre lang=&quot;isar&quot;&#62; y otra con &#60;\/pre&#62;<br \/>\n[\/expand]<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Sean k, m, n n\u00fameros naturales. Demostrar que k * m = k * n \u2194 m = n \u2228 k = 0 Para ello, completar la siguiente teor\u00eda de Lean: import data.nat.basic open nat variables {k m n : \u2115} example : k * m = k * n \u2194 m = n \u2228 k = 0 := sorry [expand title=\u00bbSoluciones con Lean\u00bb] import data.nat.basic open nat variables {k m n : \u2115} &#8212; Para que no use la notaci\u00f3n con puntos set_option pp.structure_projections false &#8212; 1\u00aa demostraci\u00f3n example : k * m = k * n \u2194 m = n \u2228 k = 0 := begin have h1: k \u2260 0 \u2192 k * m = k * n \u2192 m = n,&#8230;<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","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,"_jetpack_memberships_contains_paid_content":false,"footnotes":""},"categories":[25],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/608"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/comments?post=608"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/608\/revisions"}],"predecessor-version":[{"id":609,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/608\/revisions\/609"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=608"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=608"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=608"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}