{"id":2278,"date":"2024-02-23T06:00:40","date_gmt":"2024-02-23T04:00:40","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/?p=2278"},"modified":"2024-02-22T19:03:29","modified_gmt":"2024-02-22T17:03:29","slug":"23-feb-24","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/23-feb-24\/","title":{"rendered":"(s \u2229 t) \u222a (s \u2229 u) \u2286 s \u2229 (t \u222a u)"},"content":{"rendered":"\n

Demostrar con Lean4 que
\n\[ (s \u2229 t) \u222a (s \u2229 u) \u2286 s \u2229 (t \u222a u) \]<\/p>\n

Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n

\nimport Mathlib.Data.Set.Basic\nopen Set\nvariable {\u03b1 : Type}\nvariable (s t u : Set \u03b1)\n\nexample : (s \u2229 t) \u222a (s \u2229 u) \u2286 s \u2229 (t \u222a u):=\nby sorry\n<\/pre>\n
<\/p>\n
1. Demostraci\u00f3n en lenguaje natural<\/h2>\n
Sea \(x \u2208 (s \u2229 t) \u222a (s \u2229 u)\). Entonces son posibles dos casos.<\/p>\n
1\u00ba caso: Supongamos que \(x \u2208 s \u2229 t\). Entonces, \(x \u2208 s\) y \(x \u2208 t\) (y, por tanto, \(x \u2208 t \u222a u\)). Luego, \(x \u2208 s \u2229 (t \u222a u)\).<\/p>\n
2\u00ba caso: Supongamos que \(x \u2208 s \u2229 u\). Entonces, \(x \u2208 s\) y \(x \u2208 u\) (y, por tanto, \(x \u2208 t \u222a u\)). Luego, \(x \u2208 s \u2229 (t \u222a u)\).<\/p>\n
2. Demostraciones con Lean4<\/h2>\n
\nimport Mathlib.Data.Set.Basic\nopen Set\n\nvariable {\u03b1 : Type}\nvariable (s t u : Set \u03b1)\n\n-- 1\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (s \u2229 t) \u222a (s \u2229 u) \u2286 s \u2229 (t \u222a u):=\nby\n  intros x hx\n  -- x : \u03b1\n  -- hx : x \u2208 s \u2229 t \u222a s \u2229 u\n  -- \u22a2 x \u2208 s \u2229 (t \u222a u)\n  rcases hx with (xst | xsu)\n  . -- xst : x \u2208 s \u2229 t\n    constructor\n    . -- \u22a2 x \u2208 s\n      exact xst.1\n    . -- \u22a2 x \u2208 t \u222a u\n      left\n      -- \u22a2 x \u2208 t\n      exact xst.2\n  . -- xsu : x \u2208 s \u2229 u\n    constructor\n    . -- \u22a2 x \u2208 s\n      exact xsu.1\n    . -- \u22a2 x \u2208 t \u222a u\n      right\n      -- \u22a2 x \u2208 u\n      exact xsu.2\n\n-- 2\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (s \u2229 t) \u222a (s \u2229 u) \u2286 s \u2229 (t \u222a u):=\nby\n  rintro x (\u27e8xs, xt\u27e9 | \u27e8xs, xu\u27e9)\n  . -- x : \u03b1\n    -- xs : x \u2208 s\n    -- xt : x \u2208 t\n    -- \u22a2 x \u2208 s \u2229 (t \u222a u)\n    use xs\n    -- \u22a2 x \u2208 t \u222a u\n    left\n    -- \u22a2 x \u2208 t\n    exact xt\n  . -- x : \u03b1\n    -- xs : x \u2208 s\n    -- xu : x \u2208 u\n    -- \u22a2 x \u2208 s \u2229 (t \u222a u)\n    use xs\n    -- \u22a2 x \u2208 t \u222a u\n    right\n    -- \u22a2 x \u2208 u\n    exact xu\n\n-- 3\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (s \u2229 t) \u222a (s \u2229 u) \u2286 s \u2229 (t \u222a u):=\nby rw [inter_distrib_left s t u]\n\n-- 4\u00aa demostraci\u00f3n\n-- ===============\n\nexample : (s \u2229 t) \u222a (s \u2229 u) \u2286 s \u2229 (t \u222a u):=\nby\n  intros x hx\n  -- x : \u03b1\n  -- hx : x \u2208 s \u2229 t \u222a s \u2229 u\n  -- \u22a2 x \u2208 s \u2229 (t \u222a u)\n  aesop\n<\/pre>\n
Se puede interactuar con las demostraciones anteriores en Lean 4 Web<\/a>.<\/p>\n
3. Demostraciones con Isabelle\/HOL<\/h2>\n
\ntheory Propiedad_semidistributiva_de_la_interseccion_sobre_la_union_2\nimports Main\nbegin\n\n(* 1\u00aa demostraci\u00f3n *)\nlemma \"(s \u2229 t) \u222a (s \u2229 u) \u2286 s \u2229 (t \u222a u)\"\nproof (rule subsetI)\n  fix x\n  assume \"x \u2208 (s \u2229 t) \u222a (s \u2229 u)\"\n  then show \"x \u2208 s \u2229 (t \u222a u)\"\n  proof (rule UnE)\n    assume xst : \"x \u2208 s \u2229 t\"\n    then have xs : \"x \u2208 s\"\n      by (simp only: IntD1)\n    have xt : \"x \u2208 t\"\n      using xst by (simp only: IntD2)\n    then have xtu : \"x \u2208 t \u222a u\"\n      by (simp only: UnI1)\n    show \"x \u2208 s \u2229 (t \u222a u)\"\n      using xs xtu by (simp only: IntI)\n  next\n    assume xsu : \"x \u2208 s \u2229 u\"\n    then have xs : \"x \u2208 s\"\n      by (simp only: IntD1)\n    have xt : \"x \u2208 u\"\n      using xsu by (simp only: IntD2)\n    then have xtu : \"x \u2208 t \u222a u\"\n      by (simp only: UnI2)\n    show \"x \u2208 s \u2229 (t \u222a u)\"\n      using xs xtu by (simp only: IntI)\n  qed\nqed\n\n(* 2\u00aa demostraci\u00f3n *)\nlemma \"(s \u2229 t) \u222a (s \u2229 u) \u2286 s \u2229 (t \u222a u)\"\nproof\n  fix x\n  assume \"x \u2208 (s \u2229 t) \u222a (s \u2229 u)\"\n  then show \"x \u2208 s \u2229 (t \u222a u)\"\n  proof\n    assume xst : \"x \u2208 s \u2229 t\"\n    then have xs : \"x \u2208 s\"\n      by simp\n    have xt : \"x \u2208 t\"\n      using xst by simp\n    then have xtu : \"x \u2208 t \u222a u\"\n      by simp\n    show \"x \u2208 s \u2229 (t \u222a u)\"\n      using xs xtu by simp\n  next\n    assume xsu : \"x \u2208 s \u2229 u\"\n    then have xs : \"x \u2208 s\"\n      by (simp only: IntD1)\n    have xt : \"x \u2208 u\"\n      using xsu by simp\n    then have xtu : \"x \u2208 t \u222a u\"\n      by simp\n    show \"x \u2208 s \u2229 (t \u222a u)\"\n      using xs xtu by simp\n  qed\nqed\n\n(* 3\u00aa demostraci\u00f3n *)\nlemma \"(s \u2229 t) \u222a (s \u2229 u) \u2286 s \u2229 (t \u222a u)\"\nproof\n  fix x\n  assume \"x \u2208 (s \u2229 t) \u222a (s \u2229 u)\"\n  then show \"x \u2208 s \u2229 (t \u222a u)\"\n  proof\n    assume \"x \u2208 s \u2229 t\"\n    then show \"x \u2208 s \u2229 (t \u222a u)\"\n      by simp\n  next\n    assume \"x \u2208 s \u2229 u\"\n    then show \"x \u2208 s \u2229 (t \u222a u)\"\n      by simp\n  qed\nqed\n\n(* 4\u00aa demostraci\u00f3n *)\nlemma \"(s \u2229 t) \u222a (s \u2229 u) \u2286 s \u2229 (t \u222a u)\"\nproof\n  fix x\n  assume \"x \u2208 (s \u2229 t) \u222a (s \u2229 u)\"\n  then show \"x \u2208 s \u2229 (t \u222a u)\"\n    by auto\nqed\n\n(* 5\u00aa demostraci\u00f3n *)\nlemma \"(s \u2229 t) \u222a (s \u2229 u) \u2286 s \u2229 (t \u222a u)\"\nby auto\n\n(* 6\u00aa demostraci\u00f3n *)\nlemma \"(s \u2229 t) \u222a (s \u2229 u) \u2286 s \u2229 (t \u222a u)\"\nby (simp only: distrib_inf_le)\n\nend\n<\/pre>\n","protected":false},"excerpt":{"rendered":"
Demostrar con Lean4 que \[ (s \u2229 t) \u222a (s \u2229 u) \u2286 s \u2229 (t \u222a u) \] Para ello, completar la siguiente teor\u00eda de Lean4: import Mathlib.Data.Set.Basic open Set variable {\u03b1 : Type} variable (s t u : Set \u03b1) example : (s \u2229 t) \u222a (s \u2229 u) \u2286 s \u2229 (t \u222a u):= by sorry<\/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":"default","_kad_post_title":"default","_kad_post_layout":"default","_kad_post_sidebar_id":"","_kad_post_content_style":"default","_kad_post_vertical_padding":"default","_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\/2278"}],"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=2278"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/2278\/revisions"}],"predecessor-version":[{"id":2279,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/posts\/2278\/revisions\/2279"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/media?parent=2278"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/categories?post=2278"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/wp-json\/wp\/v2\/tags?post=2278"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}