{"id":362,"date":"2021-06-01T09:12:59","date_gmt":"2021-06-01T07:12:59","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=362"},"modified":"2021-06-01T09:14:53","modified_gmt":"2021-06-01T07:14:53","slug":"interseccion-de-los-primos-y-los-mayores-que-dos","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/interseccion-de-los-primos-y-los-mayores-que-dos\/","title":{"rendered":"Intersecci\u00f3n de los primos y los mayores que dos"},"content":{"rendered":"

Los conjuntos de los n\u00fameros primos, los mayores que 2 y los impares se definen por<\/p>\n

\n   def primos      : set \u2115 := {n | prime n}\n   def mayoresQue2 : set \u2115 := {n | n > 2}\n   def impares     : set \u2115 := {n | \u00ac even n}\n<\/pre>\n
Demostrar que<\/p>\n
\n   primos \u2229 mayoresQue2 \u2286 impares\n<\/pre>\n
Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n
\nimport data.nat.parity\nimport data.nat.prime\nimport tactic\n\nopen nat\n\ndef primos      : set \u2115 := {n | prime n}\ndef mayoresQue2 : set \u2115 := {n | n > 2}\ndef impares     : set \u2115 := {n | \u00ac even n}\n\nexample : primos \u2229 mayoresQue2 \u2286 impares :=\nsorry\n<\/pre>\n
Soluciones<\/h4>\n
<\/p>\n
Soluciones con Lean<\/strong><\/p>\n
\nimport data.nat.parity\nimport data.nat.prime\nimport tactic\n\nopen nat\n\ndef primos      : set \u2115 := {n | prime n}\ndef mayoresQue2 : set \u2115 := {n | n > 2}\ndef impares     : set \u2115 := {n | \u00ac even n}\n\nexample : primos \u2229 mayoresQue2 \u2286 impares :=\nbegin\n  unfold primos mayoresQue2 impares,\n  intro n,\n  simp,\n  intro hn,\n  cases prime.eq_two_or_odd hn with h h,\n  { rw h,\n    intro,\n    linarith, },\n  { rw even_iff,\n    rw h,\n    norm_num },\nend\n<\/pre>\n
Soluciones con Isabelle\/HOL<\/strong><\/p>\n
\ntheory Interseccion_de_los_primos_y_los_mayores_que_dos\nimports Main \"HOL-Number_Theory.Number_Theory\"\nbegin\n\ndefinition primos :: \"nat set\" where\n  \"primos = {n \u2208 \u2115 . prime n}\"\n\ndefinition mayoresQue2 :: \"nat set\" where\n  \"mayoresQue2 = {n \u2208 \u2115 . n > 2}\"\n\ndefinition impares :: \"nat set\" where\n  \"impares = {n \u2208 \u2115 . \u00ac even n}\"\n\nsection \u20391\u00aa demostraci\u00f3n\u203a\n\nlemma \"primos \u2229 mayoresQue2 \u2286 impares\"\nproof\n  fix x\n  assume \"x \u2208 primos \u2229 mayoresQue2\"\n  then have \"x \u2208 \u2115 \u2227 prime x \u2227 2 < x\"\n    by (simp add: primos_def mayoresQue2_def)\n  then have \"x \u2208 \u2115 \u2227 odd x\"\n    by (simp add: prime_odd_nat)\n  then show \"x \u2208 impares\"\n    by (simp add: impares_def)\nqed\n\nsection \u20392\u00aa demostraci\u00f3n\u203a\n\nlemma \"primos \u2229 mayoresQue2 \u2286 impares\"\n  unfolding primos_def mayoresQue2_def impares_def\n  by (simp add: Collect_mono_iff Int_def prime_odd_nat)\n\nsection \u20393\u00aa demostraci\u00f3n\u203a\n\nlemma \"primos \u2229 mayoresQue2 \u2286 impares\"\n  unfolding primos_def mayoresQue2_def impares_def\n  by (auto simp add: prime_odd_nat)\n\nend\n<\/pre>\n
Nuevas soluciones<\/strong><\/p>\n
    \n
  • En los comentarios se pueden escribir nuevas soluciones.\n
  • El c\u00f3digo se debe escribir entre una l\u00ednea con <pre lang="isar"> y otra con <\/pre>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"
    Los conjuntos de los n\u00fameros primos, los mayores que 2 y los impares se definen por def primos : set \u2115 := {n | prime n} def mayoresQue2 : set \u2115 := {n | n > 2} def impares : set \u2115 := {n | \u00ac even n} Demostrar que primos \u2229 mayoresQue2 \u2286 impares Para ello, completar la siguiente teor\u00eda de Lean: import data.nat.parity import data.nat.prime import tactic open nat def primos : set \u2115 := {n | prime n} def mayoresQue2 : set \u2115 := {n | n > 2} def impares : set \u2115 := {n | \u00ac even n} example : primos \u2229 mayoresQue2 \u2286 impares := sorry Soluciones<\/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":[7],"tags":[],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/362"}],"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=362"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/362\/revisions"}],"predecessor-version":[{"id":364,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/362\/revisions\/364"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=362"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=362"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=362"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}