{"id":7960,"date":"2023-07-15T12:04:10","date_gmt":"2023-07-15T10:04:10","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7960"},"modified":"2023-07-16T12:05:25","modified_gmt":"2023-07-16T10:05:25","slug":"15-jul-23","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/15-jul-23\/","title":{"rendered":"La semana en Calculemus (15 de julio de 2023)"},"content":{"rendered":"<p>Esta semana he publicado en <a href=\"https:\/\/www.glc.us.es\/~jalonso\/calculemus\/\">Calculemus<\/a> las demostraciones con Lean4 de las siguientes propiedades:<\/p>\n<ul>\n<li><a href=\"#ej1\">1. \u2200 m n : \u2115, Even n \u2192 Even (m * n)<\/a><\/li>\n<li><a href=\"#ej2\">2. \u2200 a b c \u2208 \u211d, (a * b) * c = b * (a * c)<\/a><\/li>\n<li><a href=\"#ej3\">3. \u2200 a b c \u2208 \u211d, (c * b) * a = b * (a * c)<\/a><\/li>\n<li><a href=\"#ej4\">4. \u2200 a b c \u2208 \u211d, a * (b * c) = b * (a * c)<\/a><\/li>\n<li><a href=\"#ej5\">5. Si ab = cd y e = f, entonces a(be) = c(df)<\/a><\/li>\n<\/ul>\n<p>A continuaci\u00f3n se muestran las soluciones.<br \/>\n<!--more--><br \/>\n<a name=\"ej1\"><\/a><\/p>\n<h3>1. \u2200 m n : \u2115, Even n \u2192 Even (m * n)<\/h3>\n<p>Demostrar que los productos de los n\u00fameros naturales por n\u00fameros pares son pares.<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n<pre lang=\"lean\">import Mathlib.Data.Nat.Basic\nimport Mathlib.Data.Nat.Parity\nimport Mathlib.Tactic\n\nopen Nat\n\nexample : \u2200 m n : \u2115, Even n \u2192 Even (m * n) := by\n  sorry\n<\/pre>\n<p><!-- more--><\/p>\n<p><b>Soluciones con Lean<\/b><\/p>\n<pre lang=\"lean\">import Mathlib.Data.Nat.Basic\nimport Mathlib.Data.Nat.Parity\nimport Mathlib.Tactic\n\nopen Nat\n\n-- 1\u00aa demostraci\u00f3n\nexample : \u2200 m n : \u2115, Even n \u2192 Even (m * n) := by\n  rintro m n \u27e8k, hk\u27e9\n  use m * k\n  rw [hk]\n  ring\n\n-- 2\u00aa demostraci\u00f3n\nexample : \u2200 m n : \u2115, Even n \u2192 Even (m * n) := by\n  rintro m n \u27e8k, hk\u27e9\n  use m * k\n  rw [hk]\n  rw [mul_add]\n\n-- 3\u00aa demostraci\u00f3n\nexample : \u2200 m n : \u2115, Even n \u2192 Even (m * n) := by\n  rintro m n \u27e8k, hk\u27e9\n  use m * k\n  rw [hk, mul_add]\n\n-- 4\u00aa demostraci\u00f3n\nexample : \u2200 m n : Nat, Even n \u2192 Even (m * n) := by\n  rintro m n \u27e8k, hk\u27e9; use m * k; rw [hk, mul_add]\n\n-- 5\u00aa demostraci\u00f3n\nexample : \u2200 m n : \u2115, Even n \u2192 Even (m * n) := by\n  rintro m n \u27e8k, hk\u27e9\n  exact \u27e8m * k, by rw [hk, mul_add]\u27e9\n\n-- 6\u00aa demostraci\u00f3n\nexample : \u2200 m n : Nat, Even n \u2192 Even (m * n) :=\nfun m n \u27e8k, hk\u27e9 \u21a6 \u27e8m * k, by rw [hk, mul_add]\u27e9\n\n-- 7\u00aa demostraci\u00f3n\nexample : \u2200 m n : \u2115, Even n \u2192 Even (m * n) := by\n  rintro m n \u27e8k, hk\u27e9\n  use m * k\n  rw [hk]\n  exact mul_add m k k\n\n-- 8\u00aa demostraci\u00f3n\nexample : \u2200 m n : \u2115, Even n \u2192 Even (m * n) := by\n  intros m n hn\n  unfold Even at *\n  cases hn with\n  | intro k hk =&gt;\n    use m * k\n    rw [hk, mul_add]\n\n-- 9\u00aa demostraci\u00f3n\nexample : \u2200 m n : \u2115, Even n \u2192 Even (m * n) := by\n  intros m n hn\n  unfold Even at *\n  cases hn with\n  | intro k hk =&gt;\n    use m * k\n    calc m * n\n       = m * (k + k)   := by exact congrArg (HMul.hMul m) hk\n     _ = m * k + m * k := by exact mul_add m k k\n\n-- 10\u00aa demostraci\u00f3n\nexample : \u2200 m n : Nat, Even n \u2192 Even (m * n) := by\n  intros; simp [*, parity_simps]\n<\/pre>\n<p><b>Comentarios (con ChatGPT)<\/b><\/p>\n<div id=\"content\" class=\"content\">\n<p>Las demostraciones presentadas tienen como objetivo demostrar la proposici\u00f3n de que, para cualquier n\u00famero natural <code>m<\/code> y <code>n<\/code>, si <code>n<\/code> es par (<code>Even<\/code>), entonces el producto de <code>m<\/code> y <code>n<\/code> tambi\u00e9n es par. A continuaci\u00f3n, analizaremos cada demostraci\u00f3n en detalle:<\/p>\n<p>La <b>1\u00aa demostraci\u00f3n<\/b> comienza con el comando <code>example<\/code>, que establece la meta que se desea demostrar. Luego, se introducen las variables <code>m<\/code> y <code>n<\/code> utilizando el comando <code>rintro<\/code>, lo que permite utilizarlas en la prueba. A continuaci\u00f3n, se introduce la hip\u00f3tesis de que <code>n<\/code> es par utilizando <code>\u27e8k, hk\u27e9<\/code>, donde <code>k<\/code> es un n\u00famero natural y <code>hk<\/code> es una prueba de que <code>n = k + k<\/code>.<\/p>\n<p>Para demostrar que <code>m * n<\/code> es par, se utiliza el comando <code>use m * k<\/code>, que establece <code>m * k<\/code> como el n\u00famero natural que demostrar\u00e1 que <code>m * n<\/code> es par. Luego, se utiliza el comando <code>rw [hk]<\/code> para reemplazar <code>n<\/code> en la meta con <code>k + k<\/code>, utilizando la prueba <code>hk<\/code>.<\/p>\n<p>Finalmente, se utiliza el comando <code>ring<\/code> para simplificar la expresi\u00f3n <code>m * (k + k)<\/code> a <code>m * k + m * k<\/code> utilizando las propiedades algebraicas de los n\u00fameros naturales.<\/p>\n<p>En resumen, la demostraci\u00f3n establece que si <code>n<\/code> es par, entonces <code>m * n<\/code> tambi\u00e9n es par, utilizando la propiedad de la paridad de los n\u00fameros naturales.<\/p>\n<p>La <b>2\u00aa demostraci\u00f3n<\/b> es similar a la primera, pero incluye un paso adicional utilizando el comando <code>rw [mul_add]<\/code>.<\/p>\n<p>Al igual que en la primera demostraci\u00f3n, se comienza con el comando <code>example<\/code>, se introducen las variables <code>m<\/code> y <code>n<\/code> con <code>rintro<\/code>, y se establece la hip\u00f3tesis de que <code>n<\/code> es par utilizando <code>\u27e8k, hk\u27e9<\/code>. A continuaci\u00f3n, se utiliza el comando <code>use m * k<\/code> para establecer <code>m * k<\/code> como el n\u00famero natural que demostrar\u00e1 que <code>m * n<\/code> es par.<\/p>\n<p>Despu\u00e9s de eso, se utiliza el comando <code>rw [hk]<\/code> para reemplazar <code>n<\/code> en la meta por <code>k *+ k<\/code>, utilizando la prueba <code>hk<\/code>. Esto es similar a la primera demostraci\u00f3n.<\/p>\n<p>Sin embargo, en la segunda demostraci\u00f3n se agrega el comando <code>rw [mul_add]<\/code> adicionalmente. Este comando utiliza la propiedad distributiva de la multiplicaci\u00f3n respecto a la adici\u00f3n en los n\u00fameros naturales. Al aplicar <code>rw [mul_add]<\/code>, se expande la expresi\u00f3n <code>m * (k + k)<\/code> en la meta a <code>m * k + m * k<\/code>.<\/p>\n<p>En resumen, la segunda demostraci\u00f3n es una extensi\u00f3n de la primera, donde se agrega el paso adicional <code>rw [mul_add]<\/code> para aplicar la propiedad distributiva de la multiplicaci\u00f3n respecto a la adici\u00f3n en los n\u00fameros naturales. Esto permite expandir la expresi\u00f3n <code>m * (k + k)<\/code> a <code>m * k + m * k<\/code> en la meta de la demostraci\u00f3n.<\/p>\n<p>La <b>3\u00aa demostraci\u00f3n<\/b> comienza con el comando <code>rintro<\/code> seguido de <code>m n \u27e8k, hk\u27e9<\/code>. Esto introduce las variables <code>m<\/code> y <code>n<\/code>, as\u00ed como una hip\u00f3tesis <code>hk<\/code> de la forma <code>\u27e8k, hk\u27e9<\/code> que establece que <code>n<\/code> es par.<\/p>\n<p>Luego se utiliza <code>use m * k<\/code> para establecer <code>m * k<\/code> como el n\u00famero demostrar\u00e1 que <code>m * n<\/code> es par. Esto se logra al utilizar el comando <code>rw<\/code> (reemplazo) con <code>[hk, mul_add]<\/code>. El reemplazo se realiza en dos pasos. Primero, se reemplaza <code>hk<\/code>, lo que resulta en la sustituci\u00f3n de <code>n<\/code> por <code>k + k<\/code> en la meta. Luego, se aplica la propiedad distributiva de la multiplicaci\u00f3n respecto a la adici\u00f3n en los n\u00fameros naturales, expandiendo la expresi\u00f3n <code>m * (k + k)<\/code> a <code>m * k + m * k<\/code>.<\/p>\n<p>En resumen, la tercera demostraci\u00f3n utiliza la introducci\u00f3n de variables, la asignaci\u00f3n de un n\u00famero espec\u00edfico (<code>m * k<\/code>) para demostrar la paridad de <code>m * n<\/code>, y luego realiza reemplazos para simplificar la expresi\u00f3n y llegar al resultado deseado.<\/p>\n<p>La <b>4\u00aa demostraci\u00f3n<\/b> utiliza una notaci\u00f3n m\u00e1s compacta en comparaci\u00f3n con las demostraciones anteriores. Comienza con el comando <code>rintro m n \u27e8k, hk\u27e9<\/code>, que introduce las variables <code>m<\/code> y <code>n<\/code>, as\u00ed como una hip\u00f3tesis <code>hk<\/code> de la forma <code>\u27e8k, hk\u27e9<\/code> que establece que <code>n<\/code> es par.<\/p>\n<p>Luego se utiliza <code>use m * k<\/code> para establecer <code>m * k<\/code> como el n\u00famero que demostrar\u00e1 que <code>m * n<\/code> es par. Esta es una abreviatura de <code>use (m * k)<\/code>.<\/p>\n<p>A continuaci\u00f3n, se utiliza el comando <code>rw [hk, mul_add]<\/code> para realizar dos reemplazos en un solo paso. Primero, se reemplaza <code>hk<\/code>, lo que sustituye <code>n<\/code> por <code>k + k<\/code> en la meta. Luego, se aplica la propiedad distributiva de la multiplicaci\u00f3n respecto a la adici\u00f3n en los n\u00fameros naturales, expandiendo la expresi\u00f3n <code>m * (k + k)<\/code> a <code>m * k + m * k<\/code>.<\/p>\n<p>En resumen, la cuarta demostraci\u00f3n utiliza una notaci\u00f3n m\u00e1s compacta para introducir variables y establecer el n\u00famero que demuestra la paridad de <code>m * n<\/code>, y luego realiza los reemplazos necesarios para simplificar la expresi\u00f3n y alcanzar el resultado deseado.<\/p>\n<p>La <b>5\u00aa demostraci\u00f3n<\/b> comienza con el comando <code>rintro<\/code> para introducir las variables <code>m<\/code> y <code>n<\/code>, y luego <code>\u27e8k, hk\u27e9<\/code> se utiliza para establecer la hip\u00f3tesis de paridad <code>n = k + k<\/code>, donde <code>k<\/code> es un n\u00famero natural y <code>hk<\/code> es una prueba de esta igualdad.<\/p>\n<p>Luego se utiliza el comando <code>exact \u27e8m * k, by rw [hk, mul_add]\u27e9<\/code> para establecer directamente <code>\u27e8m * k, \u2026\u27e9<\/code> como la prueba requerida de que <code>m * n<\/code> es par. Aqu\u00ed, <code>\u27e8m * k, \u2026\u27e9<\/code> representa el n\u00famero <code>m * k<\/code> como testigo de la paridad, y <code>by rw [hk, mul_add]<\/code> proporciona una prueba que muestra que ese n\u00famero es par.<\/p>\n<p>Dentro de <code>by rw [hk, mul_add]<\/code>, se realiza el reemplazo utilizando <code>rw<\/code>. Primero, se reemplaza <code>hk<\/code>, lo que sustituye <code>n<\/code> por <code>k + k<\/code> en la meta. Luego, se aplica la propiedad distributiva de la multiplicaci\u00f3n respecto a la adici\u00f3n en los n\u00fameros naturales, expandiendo la expresi\u00f3n <code>m * (k + k)<\/code> a <code>m * k + m * k<\/code>.<\/p>\n<p>En resumen, la quinta demostraci\u00f3n utiliza el comando <code>rintro<\/code> para introducir las variables y la hip\u00f3tesis de paridad, y luego utiliza <code>exact<\/code> para establecer directamente el n\u00famero y la prueba requeridos para demostrar la paridad de <code>m * n<\/code>. Proporciona una soluci\u00f3n directa y concisa al problema planteado.<\/p>\n<p>La <b>6\u00aa demostraci\u00f3n<\/b> utiliza una notaci\u00f3n de funci\u00f3n lambda para definir directamente la prueba requerida. Comienza con <code>fun m n \u27e8k, hk\u27e9 \u21a6<\/code>, donde se introducen las variables <code>m<\/code> y <code>n<\/code>, y se establece una hip\u00f3tesis <code>\u27e8k, hk\u27e9<\/code> que afirma que <code>n<\/code> es par.<\/p>\n<p>Luego, se utiliza <code>\u27e8m * k, by rw [hk, mul_add]\u27e9<\/code> para establecer directamente <code>m * k<\/code> como el n\u00famero que demostrar\u00e1 que <code>m * n<\/code> es par. Esto se hace mediante el uso de la notaci\u00f3n <code>\u27e8valor, prueba\u27e9<\/code>, donde <code>valor<\/code> representa el n\u00famero que se utilizar\u00e1 como testigo de la paridad y <code>prueba<\/code> es una prueba que muestra que ese valor es par.<\/p>\n<p>En este caso, se establece <code>m * k<\/code> como el valor y se proporciona prueba utilizando by <code>rw [hk, mul_add]<\/code>. Aqu\u00ed, <code>rw [hk, mul_add]<\/code> realiza dos reemplazos en un solo paso. Primero, se reemplaza <code>hk<\/code>, lo que sustituye <code>n<\/code> por <code>k + k<\/code> en la meta. Luego, se aplica la propiedad distributiva de la multiplicaci\u00f3n respecto a la adici\u00f3n en los n\u00fameros naturales, expandiendo la expresi\u00f3n <code>m * (k + k)<\/code> a <code>m * k + m * k<\/code>.<\/p>\n<p>En resumen, la sexta demostraci\u00f3n utiliza una funci\u00f3n lambda para definir directamente el valor y la prueba necesarios para demostrar la paridad de <code>m * n<\/code>. Proporciona una soluci\u00f3n concisa y directa al problema planteado, al igual que la quinta demostraci\u00f3n.<\/p>\n<p>La <b>7\u00aa demostraci\u00f3n<\/b> comienza con el comando <code>rintro<\/code> para introducir las variables <code>m<\/code> y <code>n<\/code>, y luego <code>\u27e8k, hk\u27e9<\/code> se utiliza para establecer la hip\u00f3tesis de paridad <code>n = k + k<\/code>, donde <code>k<\/code> es un n\u00famero natural y <code>hk<\/code> es una prueba de esta igualdad.<\/p>\n<p>A continuaci\u00f3n, se utiliza <code>use m * k<\/code> para establecer <code>m * k<\/code> como el n\u00famero que demostrar\u00e1 que <code>m * n<\/code> es par.<\/p>\n<p>Luego se utiliza <code>rw [hk]<\/code> para reemplazar <code>n<\/code> en la meta por <code>k + k<\/code>, utilizando la prueba <code>hk<\/code>.<\/p>\n<p>Finalmente, se utiliza <code>exact mul_add m k k<\/code> para establecer que <code>m * (k + k)<\/code> es igual a <code>m * k + m * k<\/code>. Esto se logra utilizando la propiedad distributiva de la multiplicaci\u00f3n respecto a la adici\u00f3n en los n\u00fameros naturales.<\/p>\n<p>En resumen, la s\u00e9ptima demostraci\u00f3n utiliza los comandos <code>rintro<\/code>, <code>use<\/code>, <code>rw<\/code> y <code>exact<\/code> para introducir variables, establecer el n\u00famero testigo, realizar reemplazos y proporcionar una prueba final que demuestra la paridad de <code>m * n<\/code>.<\/p>\n<p>La <b>8\u00aa demostraci\u00f3n<\/b> comienza con el comando <code>intros m n hn<\/code> para introducir las variables <code>m<\/code> y <code>n<\/code>, as\u00ed como la hip\u00f3tesis de paridad <code>hn<\/code>. Luego se utiliza <code>unfold Even at *<\/code> para desplegar la definici\u00f3n de paridad en todos los lugares relevantes.<\/p>\n<p>A continuaci\u00f3n, se utiliza <code>cases hn with | intro k hk =&gt;<\/code> para realizar un an\u00e1lisis de casos sobre la hip\u00f3tesis de paridad <code>hn<\/code>. En el caso en que <code>hn<\/code> se cumple y se puede demostrar que <code>n = k + k<\/code>, se introduce una nueva variable <code>k<\/code> y una prueba <code>hk<\/code> que establece esa igualdad.<\/p>\n<p>Dentro de este caso, se utiliza <code>use m * k<\/code> para establecer <code>m * k<\/code> como el n\u00famero que demostrar\u00e1 que <code>m * n<\/code> es par. Luego se utiliza <code>rw [hk, mul_add]<\/code> para realizar los reemplazos correspondientes.<\/p>\n<p>En resumen, la octava demostraci\u00f3n utiliza <code>intros<\/code> para introducir las variables <code>m<\/code>, <code>n<\/code> y la hip\u00f3tesis de paridad <code>hn<\/code>. Luego se utiliza <code>unfold Even at *<\/code> para desplegar la definici\u00f3n de paridad en todos los lugares relevantes. A continuaci\u00f3n, se realiza un an\u00e1lisis de casos sobre la hip\u00f3tesis de paridad utilizando <code>cases<\/code>, y se introduce el n\u00famero testigo utilizando <code>use<\/code>. Finalmente, se realiza el reemplazo utilizando <code>rw<\/code> para simplificar la expresi\u00f3n y demostrar la paridad de <code>m * n<\/code>.<\/p>\n<p>La <b>9\u00aa demostraci\u00f3n<\/b> comienza con el comando <code>intros m n hn<\/code> para introducir las variables <code>m<\/code> y <code>n<\/code>, as\u00ed como la hip\u00f3tesis de paridad <code>hn<\/code>. Luego se utiliza <code>unfold Even at *<\/code> para desplegar la definici\u00f3n de paridad en todos los lugares relevantes.<\/p>\n<p>A continuaci\u00f3n, se utiliza <code>cases hn with | intro k hk =&gt;<\/code> para realizar un an\u00e1lisis de casos sobre la hip\u00f3tesis de paridad <code>hn<\/code>. En el caso en que hn se cumple y se puede demostrar que <code>n = k + k<\/code>, se introduce una nueva variable <code>k<\/code> y una prueba <code>hk<\/code> que establece esa igualdad.<\/p>\n<p>Dentro de este caso, se utiliza <code>use m * k<\/code> para establecer <code>m * k<\/code> como el n\u00famero que demostrar\u00e1 que <code>m * n<\/code> es par.<\/p>\n<p>Luego, se utiliza <code>calc m * n = m * (k + k) := by exact congrArg (HMul.hMul m) hk<\/code> para realizar un razonamiento algebraico paso a paso. La igualdad se deriva aplicando el lema <code>congrArg<\/code> al valor <code>m<\/code> y la prueba <code>hk<\/code> para mostrar que la multiplicaci\u00f3n preserva la igualdad. Esto establece que <code>m * n<\/code> es igual a <code>m * (k + k)<\/code>.<\/p>\n<p>Finalmente, se utiliza <code>_ = m * k + m * k := by exact mul_add m k k<\/code> para aplicar el lema <code>mul_add<\/code> y establecer que <code>m * k + m * k<\/code> es igual a <code>m * (k + k)<\/code>. Esto se logra utilizando la propiedad distributiva de la multiplicaci\u00f3n respecto a la adici\u00f3n en los n\u00fameros naturales.<\/p>\n<p>En resumen, la novena demostraci\u00f3n utiliza <code>intros<\/code> para introducir las variables <code>m<\/code>, <code>n<\/code> y la hip\u00f3tesis de paridad <code>hn<\/code>. Luego se utiliza <code>unfold Even at *<\/code> para desplegar la definici\u00f3n de paridad en todos los lugares relevantes. A continuaci\u00f3n, se realiza un an\u00e1lisis de casos sobre la hip\u00f3tesis de paridad utilizando <code>cases<\/code>, se introduce el n\u00famero testigo utilizando <code>use<\/code>, y se utiliza <code>calc<\/code> y <code>by<\/code> para realizar razonamientos algebraicos paso a paso y establecer la igualdad necesaria.<\/p>\n<p>La <b>*10\u00aa demostraci\u00f3n<\/b> utiliza una estrategia de simplificaci\u00f3n (<code>simp<\/code>) con las expresiones <code>*<\/code>, <code>parity_simps<\/code>. El comando <code>intros<\/code> se utiliza para introducir las variables y se utiliza <code>;<\/code> para combinar m\u00faltiples comandos en una sola l\u00ednea.<\/p>\n<p>El <code>simp<\/code> se aplica a las expresiones <code>*<\/code> y <code>parity_simps<\/code>. La expresi\u00f3n <code>*<\/code> indica que se deben aplicar simplificaciones con el contexto y la meta, mientras que <code>parity_simps<\/code> indica que se deben aplicar simplificaciones espec\u00edficas relacionadas con la paridad de los n\u00fameros naturales.<\/p>\n<p>En resumen, la d\u00e9cima demostraci\u00f3n utiliza <code>intros<\/code> para introducir las variablesy luego aplica el comando <code>simp<\/code> con <code>*<\/code>, <code>parity_simps<\/code> para realizar las simplificaciones necesarias en la expresi\u00f3n <code>m * n<\/code> y demostrar su paridad. Esta estrategia simplificada permite una demostraci\u00f3n concisa y autom\u00e1tica del resultado deseado.<\/p>\n<p>En <b>resumen<\/b>, todas las demostraciones presentadas son v\u00e1lidas y demuestran la misma proposici\u00f3n. Algunas utilizan t\u00e1cticas m\u00e1s directas y simples, mientras que otras exploran diferentes enfoques y estilos de escritura en Lean.<\/p>\n<\/div>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li>J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/44d6BMo\">Mathematics in Lean<\/a>, p. 3.<\/li>\n<\/ul>\n<p><a name=\"ej2\"><\/a><\/p>\n<h3>2. \u2200 a b c \u2208 \u211d, (a * b) * c = b * (a * c)<\/h3>\n<p>Demostrar con Lean4 que los n\u00fameros reales tienen la siguiente propiedad<\/p>\n<pre lang=\"text\">(a * b) * c = b * (a * c)\n<\/pre>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">import Mathlib.Tactic\nimport Mathlib.Data.Real.Basic\n\nexample (a b c : \u211d) : (a * b) * c = b * (a * c) := by\nsorry\n<\/pre>\n<p><b>Soluciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">import Mathlib.Tactic\nimport Mathlib.Data.Real.Basic\n\n-- 1\u00aa demostraci\u00f3n\nexample (a b c : \u211d) : (a * b) * c = b * (a * c) := by\n  rw [mul_comm a b]\n  rw [mul_assoc b a c]\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (a b c : \u211d)\n  : (a * b) * c = b * (a * c) :=\ncalc\n  (a * b) * c = (b * a) * c := by rw [mul_comm a b]\n            _ = b * (a * c) := by rw [mul_assoc b a c]\n\n-- 3\u00aa demostraci\u00f3n\nexample (a b c : \u211d) : (a * b) * c = b * (a * c) :=\nby ring\n<\/pre>\n<p><b>Comentarios (de ChatGPT)<\/b><\/p>\n<div id=\"content\" class=\"content\">\n<p>En estas demostraciones, se muestra que para cualquier n\u00famero real <code>a<\/code>, <code>b<\/code> y <code>c<\/code>, se cumple la igualdad <code>(a * b) * c = b * (a * c)<\/code>. A continuaci\u00f3n, se explica cada demostraci\u00f3n en detalle:<\/p>\n<p>En la <b>1\u00aa demostraci\u00f3n<\/b> se utiliza la t\u00e1ctica <code>by<\/code> junto con la t\u00e1ctica <code>rw<\/code> (<code>rewrite<\/code>) para reescribir la expresi\u00f3n y llegar a la igualdad deseada.<\/p>\n<p>La t\u00e1ctica <code>rw [mul_comm a b]<\/code> se utiliza para aplicar la conmutatividad de la multiplicaci\u00f3n y cambiar el orden de <code>a<\/code> y <code>b<\/code> en la expresi\u00f3n <code>(a * b)<\/code>. Despu\u00e9s, la t\u00e1ctica <code>rw [mul_assoc b a c]<\/code> se utiliza para aplicar la asociatividad de la multiplicaci\u00f3n y reagrupar los t\u00e9rminos de la expresi\u00f3n <code>((b * a) * c)<\/code> en <code>(b * (a * c))<\/code>.<\/p>\n<p>Al combinar estas dos t\u00e1cticas, se reescribe la expresi\u00f3n original hasta llegar a la igualdad deseada.<\/p>\n<p>En <b>2\u00aa demostraci\u00f3n<\/b> se utiliza la t\u00e1ctica <code>calc<\/code> para realizar una cadena de igualdades y llegar a la igualdad deseada.<\/p>\n<p>La cadena de igualdades comienza con <code>(a * b) * c<\/code> y se utiliza la t\u00e1ctica <code>rw [mul_comm a b]<\/code> para reescribir <code>(a * b)<\/code> como <code>(b * a)<\/code>. Luego, se utiliza la t\u00e1ctica <code>rw [mul_assoc b a c]<\/code> para reescribir <code>(b * a) * c<\/code> como <code>b * (a * c)<\/code>.<\/p>\n<p>Al utilizar la t\u00e1ctica calc de esta manera, se muestra paso a paso c\u00f3mo se llega a la igualdad deseada a trav\u00e9s de una cadena de reescrituras.<\/p>\n<p>En la <b>3\u00aa demostraci\u00f3n<\/b> se utiliza la t\u00e1ctica <code>by ring<\/code> para demostrar la igualdad directamente utilizando propiedades algebraicas conocidas.<\/p>\n<p>La t\u00e1ctica <code>by ring<\/code> se utiliza cuando se trabaja con anillos, como en este caso con los n\u00fameros reales. Esta t\u00e1ctica aplica autom\u00e1ticamente las reglas algebraicas b\u00e1sicas, como la conmutatividad y la asociatividad de la multiplicaci\u00f3n, para simplificar y demostrar la igualdad.<\/p>\n<p>En este caso, la t\u00e1ctica <code>by ring<\/code> reorganiza autom\u00e1ticamente los t\u00e9rminos en la expresi\u00f3n <code>(a * b) * c<\/code> y llega a la forma <code>b * (a * c)<\/code>, demostrando as\u00ed la igualdad.<\/p>\n<p>En <b>resumen<\/b>, estas demostraciones muestran diferentes enfoques para demostrar la igualdad <code>(a * b) * c = b * (a * c)<\/code> utilizando t\u00e1cticas de reescritura y propiedades algebraicas b\u00e1sicas. Cada demostraci\u00f3n presenta un enfoque distinto, pero todos llegan al mismo resultado.<\/p>\n<\/div>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li>J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 5.<\/li>\n<\/ul>\n<p><a name=\"ej3\"><\/a><\/p>\n<h3>3. \u2200 a b c \u2208 \u211d, (c * b) * a = b * (a * c)<\/h3>\n<p>Demostrar con Lean4 que los n\u00fameros reales tienen la siguiente propiedad<\/p>\n<pre lang=\"text\">(c * b) * a = b * (a * c)\n<\/pre>\n<p>Para ello, completar la siguiente teor\u00eda de Lean:<\/p>\n<pre lang=\"lean\">import Mathlib.Tactic\nimport Mathlib.Data.Real.Basic\n\nexample (a b c : \u211d) : (c * b) * a = b * (a * c) :=\nby sorry\n<\/pre>\n<p><b>Soluciones con Lean4<\/b><\/p>\n<pre lang=\"lean\">import Mathlib.Tactic\nimport Mathlib.Data.Real.Basic\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (a b c : \u211d)\n  : (c * b) * a = b * (a * c) :=\nby\n  rw [mul_comm c b]\n  rw [mul_assoc]\n  rw [mul_comm c a]\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (a b c : \u211d)\n  : (c * b) * a = b * (a * c) :=\ncalc\n  (c * b) * a\n    = (b * c) * a := by rw [mul_comm c b]\n  _ = b * (c * a) := by rw [mul_assoc]\n  _ = b * (a * c) := by rw [mul_comm c a]\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  (a b c : \u211d)\n  : (c * b) * a = b * (a * c) :=\nby ring\n<\/pre>\n<p><b>Comentarios (obtenidos con ChatGPT)<\/b><\/p>\n<div id=\"content\" class=\"content\">\n<p>Las tres demostraciones son variantes equivalentes para demostrar la misma igualdad, utilizando t\u00e1cticas diferentes. Voy a explicar cada una de ellas en detalle:<\/p>\n<p>En la <b>1\u00aa demostraci\u00f3n<\/b> se utiliza la t\u00e1ctica <code>rw<\/code> para realizar reescrituras. La igualdad que se quiere demostrar es <code>(c * b) * a = b *<br \/>\n(a * c)<\/code>. La demostraci\u00f3n comienza con <code>by<\/code>, que indica que se utilizar\u00e1n t\u00e1cticas para completar la prueba.<\/p>\n<p>Luego, se utiliza <code>rw [mul_comm c b]<\/code>, que aplica la regla de reescritura para intercambiar <code>c<\/code> y <code>b<\/code> en la expresi\u00f3n <code>(c * b) * a<\/code>, obteniendo as\u00ed <code>(b *<br \/>\nc) * a<\/code>.<\/p>\n<p>A continuaci\u00f3n, se utiliza <code>rw [mul_assoc]<\/code>, que aplica la regla de asociatividad de la multiplicaci\u00f3n para reagrupar los t\u00e9rminos, obteniendo <code>b * (c * a)<\/code>.<\/p>\n<p>Finalmente, se utiliza <code>rw [mul_comm c a]<\/code>, que aplica la regla de reescritura para intercambiar <code>c<\/code> y <code>a<\/code> en la expresi\u00f3n <code>b * (c * a)<\/code>, obteniendo as\u00ed <code>b * (a * c)<\/code>. La prueba se considera completada y se ha demostrado la igualdad deseada.<\/p>\n<p>En la <b>2\u00aa demostraci\u00f3n<\/b> se utiliza la t\u00e1ctica <code>calc<\/code> para realizar c\u00e1lculos sucesivos. La igualdad que se quiere demostrar es <code>(c * b) * a = b * (a * c)<\/code>.<\/p>\n<p>La prueba comienza con <code>(c * b) * a<\/code>, y utilizando <code>:=<\/code> se establece que es igual a <code>(b * c) * a<\/code>. Esto se logra mediante <code>by rw [mul_comm c b]<\/code>, que aplica la regla de reescritura para intercambiar <code>c<\/code> y <code>b<\/code>.<\/p>\n<p>A continuaci\u00f3n, se utiliza <code>_ =<\/code> para indicar que el resultado actual es igual a <code>b * (c * a)<\/code>. Esto se logra mediante <code>by rw [mul_assoc]<\/code>, que aplica la regla de asociatividad de la multiplicaci\u00f3n.<\/p>\n<p>Finalmente, se utiliza <code>_ =<\/code> nuevamente para indicar que el resultado actual es igual a <code>b * (a * c)<\/code>. Esto se logra mediante <code>by rw [mul_comm c a]<\/code>, que aplica la regla de reescritura para intercambiar <code>c<\/code> y <code>a<\/code>. La prueba se considera completada y se ha demostrado la igualdad deseada.<\/p>\n<p>En la <b>3\u00aa demostraci\u00f3n<\/b> se utiliza la t\u00e1ctica <code>ring<\/code> para demostrar la igualdad autom\u00e1ticamente. La t\u00e1ctica <code>ring<\/code> es capaz de manejar expresiones algebraicas y aplicar reglas de simplificaci\u00f3n y reescritura para demostrar igualdades.<\/p>\n<p>La prueba comienza con <code>by ring<\/code>, que indica que se utilizar\u00e1 la t\u00e1ctica ring para completar la prueba. Esta t\u00e1ctica analiza la expresi\u00f3n <code>(c * b) * a<\/code> y la iguala autom\u00e1ticamente a <code>b * (a * c)<\/code> aplicando las reglas algebraicas necesarias.<\/p>\n<p>La t\u00e1ctica <code>ring<\/code> es muy \u00fatil para demostrar igualdades algebraicas simples de forma autom\u00e1tica, sin necesidad de especificar pasos intermedios. En este caso, la igualdad se demuestra de manera autom\u00e1tica y la prueba se considera completada.<\/p>\n<p>En <b>resumen<\/b>, las tres demostraciones son equivalentes y demuestran la igualdad <code>(c * b) * a = b * (a * c)<\/code> utilizando t\u00e1cticas diferentes: reescrituras (<code>rw<\/code>), c\u00e1lculos sucesivos (<code>calc<\/code>), y la t\u00e1ctica autom\u00e1tica <code>ring<\/code>.<\/p>\n<\/div>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li>J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 5.<\/li>\n<\/ul>\n<p><a name=\"ej4\"><\/a><\/p>\n<h3>4. \u2200 a b c \u2208 \u211d, a * (b * c) = b * (a * c)<\/h3>\n<p>Demostrar con Lean4 que \u2200 a b c \u2208 \u211d, a * (b * c) = b * (a * c)<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">\nimport Mathlib.Tactic\nimport Mathlib.Data.Real.Basic\n\nexample\n  (a b c : \u211d) : a * (b * c) = b * (a * c) :=\nby sorry\n<\/pre>\n<p><b>Soluciones con Lean<\/b><\/p>\n<pre lang=\"lean\">\nimport Mathlib.Tactic\nimport Mathlib.Data.Real.Basic\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (a b c : \u211d) : a * (b * c) = b * (a * c) :=\nby\n  rw [\u2190mul_assoc]\n  rw [mul_comm a b]\n  rw [mul_assoc]\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (a b c : \u211d) : a * (b * c) = b * (a * c) :=\ncalc\n  a * (b * c)\n    = (a * b) * c := by rw [\u2190mul_assoc]\n  _ = (b * a) * c := by rw [mul_comm a b]\n  _ = b * (a * c) := by rw [mul_assoc]\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  (a b c : \u211d) : a * (b * c) = b * (a * c) :=\nby ring\n<\/pre>\n<p><b>Comentarios (con ChatGPT)<\/b><\/p>\n<p>Las tres demostraciones son formas diferentes de demostrar la igualdad <code>a * (b * c) = b * (a * c)<\/code>, donde <code>a<\/code>, <code>b<\/code> y <code>c<\/code> son n\u00fameros reales.<\/p>\n<p>En la <strong>1\u00aa demostraci\u00f3n<\/strong>, se utilizan las t\u00e1cticas de reescritura (<code>rw<\/code>) para manipular la expresi\u00f3n y llegar al resultado deseado. La demostraci\u00f3n se realiza en un bloque <code>by<\/code>, lo que significa que todas las t\u00e1cticas se aplican secuencialmente. Aqu\u00ed se muestra el paso a paso:<\/p>\n<ol>\n<li>Se utiliza la t\u00e1ctica <code>rw [\u2190mul_assoc]<\/code> para reescribir la expresi\u00f3n <code>a * (b * c)<\/code> como <code>(a * b) * c<\/code>. Esto se hace utilizando la asociatividad de la multiplicaci\u00f3n.<\/li>\n<li>Luego, se utiliza <code>rw [mul_comm a b]<\/code> para reescribir la expresi\u00f3n <code>a * b<\/code> como <code>b * a<\/code>. Esto se hace utilizando la conmutatividad de la multiplicaci\u00f3n.<\/li>\n<li>Finalmente, se utiliza <code>rw [mul_assoc]<\/code> para reescribir la expresi\u00f3n <code>(b * a) * c<\/code> como <code>b * (a * c)<\/code>. Nuevamente, se aplica la asociatividad de la multiplicaci\u00f3n.<\/li>\n<\/ol>\n<p>Al seguir estos pasos, se llega a la igualdad deseada: <code>a * (b * c) = b * (a * c)<\/code>.<\/p>\n<p>En la <strong>2\u00aa demostraci\u00f3n<\/strong>, se utiliza la t\u00e1ctica <code>calc<\/code> para realizar la demostraci\u00f3n utilizando un estilo m\u00e1s conciso y estructurado. Aqu\u00ed se muestra el paso a paso:<\/p>\n<ol>\n<li>Se inicia con la expresi\u00f3n <code>a * (b * c)<\/code>.<\/li>\n<li>Luego, se utiliza la t\u00e1ctica <code>by rw [\u2190mul_assoc]<\/code> para reescribir la expresi\u00f3n como <code>(a * b) * c<\/code>. Esto se hace utilizando la asociatividad de la multiplicaci\u00f3n.<\/li>\n<li>A continuaci\u00f3n, se utiliza la t\u00e1ctica <code>by rw [mul_comm a b]<\/code> para reescribir la expresi\u00f3n como <code>(b * a) * c<\/code>. Esto se hace utilizando la conmutatividad de la multiplicaci\u00f3n.<\/li>\n<li>Por \u00faltimo, se utiliza la t\u00e1ctica <code>by rw [mul_assoc]<\/code> para reescribir la expresi\u00f3n como <code>b * (a * c)<\/code>. Se aplica la asociatividad de la multiplicaci\u00f3n nuevamente.<\/li>\n<\/ol>\n<p>Al seguir estos pasos, se llega a la igualdad deseada: <code>a * (b * c) = b * (a * c)<\/code>.<\/p>\n<p>En la <strong>3\u00aa demostraci\u00f3n<\/strong>, se utiliza la t\u00e1ctica <code>ring<\/code> para demostrar la igualdad. La t\u00e1ctica <code>ring<\/code> es una t\u00e1ctica poderosa que puede demostrar autom\u00e1ticamente muchas identidades algebraicas.<\/p>\n<p>Al utilizar <code>by ring<\/code>, se le indica al sistema de demostraci\u00f3n autom\u00e1tica que pruebe la igualdad utilizando propiedades algebraicas. En este caso, el sistema reconoce autom\u00e1ticamente que se puede aplicar la conmutatividad y la asociatividad de la multiplicaci\u00f3n para llegar al resultado deseado.<\/p>\n<p>En resumen, las tres demostraciones utilizan diferentes t\u00e1cticas y estilos para llegar a la igualdad <code>a * (b * c) = b * (a * c)<\/code>. La primera y segunda demostraci\u00f3n utilizan las t\u00e1cticas <code>rw<\/code> y <code>calc<\/code>, respectivamente, para reescribir la expresi\u00f3n paso a paso. La tercera demostraci\u00f3n utiliza la t\u00e1ctica <code>ring<\/code> para demostrar autom\u00e1ticamente la igualdad utilizando propiedades algebraicas.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li>J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 6.<\/li>\n<\/ul>\n<p><a name=\"ej5\"><\/a><\/p>\n<h3>5. Si ab = cd y e = f, entonces a(be) = c(df)<\/h3>\n<p>Demostrar con Lean4 que si a, b, c, d, e y f son n\u00fameros reales tales que ab = cd y e = f, entonces a(be) = c(df)<\/p>\n<p>Para ello, completar la siguiente teor\u00eda de Lean4:<\/p>\n<pre lang=\"lean\">import Mathlib.Tactic\nimport Mathlib.Data.Real.Basic\n\nexample\n  (a b c d e f : \u211d)\n  (h1 : a * b = c * d)\n  (h2 : e = f)\n  : a * (b * e) = c * (d * f) :=\nby sorry\n<\/pre>\n<p><b>Soluciones con Lean<\/b><\/p>\n<pre lang=\"lean\">import Mathlib.Tactic\nimport Mathlib.Data.Real.Basic\n\n-- 1\u00aa demostraci\u00f3n\nexample\n  (a b c d e f : \u211d)\n  (h1 : a * b = c * d)\n  (h2 : e = f)\n  : a * (b * e) = c * (d * f) :=\nby\n  rw [h2]\n  rw [\u2190mul_assoc]\n  rw [h1]\n  rw [mul_assoc]\n\n-- 2\u00aa demostraci\u00f3n\nexample\n  (a b c d e f : \u211d)\n  (h1 : a * b = c * d)\n  (h2 : e = f)\n  : a * (b * e) = c * (d * f) :=\ncalc\n  a * (b * e)\n    = a * (b * f) := by rw [h2]\n  _ = (a * b) * f := by rw [\u2190mul_assoc]\n  _ = (c * d) * f := by rw [h1]\n  _ = c * (d * f) := by rw [mul_assoc]\n\n-- 3\u00aa demostraci\u00f3n\nexample\n  (a b c d e f : \u211d)\n  (h1 : a * b = c * d)\n  (h2 : e = f)\n  : a * (b * e) = c * (d * f) :=\nby\n  simp [*, \u2190mul_assoc]\n<\/pre>\n<p><b>Comentarios (a partir de los generados por ChatGPT)<\/b><\/p>\n<p>Las tres demostraciones presentadas tienen como objetivo demostrar la igualdad: <code>a * (b * e) = c * (d * f)<\/code>, utilizando las hip\u00f3tesis <code>h1: a * b = c * d<\/code> y <code>h2: e = f<\/code>. A continuaci\u00f3n, comentar\u00e9 cada una de las demostraciones:<\/p>\n<p>En la <strong>1\u00aa demostraci\u00f3n<\/strong> se utiliza el enfoque de reescribir (<code>rw<\/code>) expresiones utilizando las igualdades dadas. El primer paso reemplazar <code>e<\/code> por <code>f<\/code> usando la hip\u00f3tesis <code>h2<\/code> (<code>rw [h2]<\/code>). Luego, se utiliza el lema de asociatividad de la multiplicaci\u00f3n en sentido inverso (<code>\u2190mul_assoc<\/code>) para reorganizar los t\u00e9rminos y obtener <code>(a * b) * f = (c * d) * f<\/code>. Por \u00faltimo, se utiliza la hip\u00f3tesis <code>h1<\/code> (<code>rw [h1]<\/code>) para reemplazar <code>a * b<\/code> por <code>c * d<\/code> y, finalmente, usando la asociatividad se llega a la igualdad deseada.<\/p>\n<p>En la <strong>2\u00aa demostraci\u00f3n<\/strong> se utiliza el enfoque de c\u00e1lculo (<code>calc<\/code>) para realizar una secuencia de pasos de igualdad. Comienza con <code>a * (b * e)<\/code> y se utiliza la hip\u00f3tesis <code>h2<\/code> para reemplazar <code>e<\/code> por <code>f<\/code> (<code>by rw [h2]<\/code>). Luego, se utiliza el lema de asociatividad de la multiplicaci\u00f3n en sentido inverso (<code>\u2190mul_assoc<\/code>) para reorganizar los t\u00e9rminos y obtener <code>a * (b * f) = (a * b) * f<\/code>. A continuaci\u00f3n, se utiliza la hip\u00f3tesis <code>h1<\/code> para reemplazar <code>a * b<\/code> por <code>c * d<\/code> (<code>by rw [h1]<\/code>) y se obtiene <code>(c * d) * f<\/code>. Finalmente, se utiliza nuevamente el lema de asociatividad de la multiplicaci\u00f3n en sentido directo (<code>mul_assoc<\/code>) para reorganizar los t\u00e9rminos y obtener <code>c * (d * f)<\/code>, llegando as\u00ed a la igualdad deseada.<\/p>\n<p>En la <strong>3\u00aa demostraci\u00f3n<\/strong> se utiliza el enfoque de simplificaci\u00f3n (<code>simp<\/code>). Se utiliza el modificador <code>*<\/code> para indicar que se deben utilizar todas las hip\u00f3tesis y lemas disponibles. En este caso, se utiliza <code>*<\/code> y <code>\u2190mul_assoc<\/code> para aplicar el lema de asociatividad de la multiplicaci\u00f3n en sentido inverso. El objetivo es simplificar <code>a * (b * e)<\/code> a <code>c * (d * f)<\/code> directamente, aprovechando las igualdades <code>h1<\/code> y <code>h2<\/code>. Este enfoque permite simplificar la demostraci\u00f3n a una sola l\u00ednea.<\/p>\n<p>En resumen, las tres demostraciones logran el mismo objetivo de demostrar la igualdad <code>a * (b * e) = c * (d * f)<\/code> utilizando diferentes enfoques. La primera utiliza reescrituras expl\u00edcitas (<code>rw<\/code>), la segunda utiliza el enfoque de c\u00e1lculo (<code>calc<\/code>) y la tercera utiliza la simplificaci\u00f3n autom\u00e1tica (<code>simp<\/code>). Cada enfoque tiene sus propias ventajas y puede ser preferido dependiendo del contexto y de la experiencia del desarrollador.<\/p>\n<p><b>Referencias<\/b><\/p>\n<ul>\n<li>J. Avigad y P. Massot. <a href=\"https:\/\/bit.ly\/3U4UjBk\">Mathematics in Lean<\/a>, p. 6.<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>Esta semana he publicado en Calculemus las demostraciones con Lean4 de las siguientes propiedades: 1. \u2200 m n : \u2115, Even n \u2192 Even (m * n) 2. \u2200 a b c \u2208 \u211d, (a * b) * c = b * (a * c) 3. \u2200 a b c \u2208 \u211d, (c * b)&#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":[1],"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\/7960"}],"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=7960"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7960\/revisions"}],"predecessor-version":[{"id":7961,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7960\/revisions\/7961"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7960"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7960"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7960"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}