Esta entrada es una recopilación de lecturas compartidas, durante agosto de 2021, en Twitter fundamentalmente sobre programación funcional y demostración asistida por ordenador.
Las lecturas están ordenadas según su fecha de publicación en Twitter.
Al final de cada artículo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.
Una recopilación de todas las lecturas compartidas se encuentra en GitHub.
Esta entrada es una recopilación de lecturas compartidas, durante julio de 2021, en Twitter fundamentalmente sobre programación funcional y demostración asistida por ordenador.
Las lecturas están ordenadas según su fecha de publicación en Twitter.
Al final de cada artículo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.
Una recopilación de todas las lecturas compartidas se encuentra en GitHub.
Esta entrada es una recopilación de lecturas compartidas, durante junio de 2021, en Twitter fundamentalmente sobre programación funcional y demostración asistida por ordenador.
Las lecturas están ordenadas según su fecha de publicación en Twitter.
Al final de cada artículo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.
Una recopilación de todas las lecturas compartidas se encuentra en GitHub.
Esta entrada es una recopilación de lecturas compartidas, durante mayo de 2021, en Twitter fundamentalmente sobre programación funcional y demostración asistida por ordenador.
Las lecturas están ordenadas según su fecha de publicación en Twitter.
Al final de cada artículo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.
Una recopilación de todas las lecturas compartidas se encuentra en GitHub.
Esta entrada es una recopilación de lecturas compartidas, durante abril de 2021, en Twitter fundamentalmente sobre programación funcional y demostración asistida por ordenador.
Las lecturas están ordenadas según su fecha de publicación en Twitter.
Al final de cada artículo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.
Una recopilación de todas las lecturas compartidas se encuentra en GitHub.
Esta entrada es una recopilación de lecturas compartidas, durante marzo de 2021, en Twitter fundamentalmente sobre programación funcional y demostración asistida por ordenador.
Las lecturas están ordenadas según su fecha de publicación en Twitter.
Al final de cada artículo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.
Una recopilación de todas las lecturas compartidas se encuentra en GitHub.
Esta entrada es una recopilación de lecturas compartidas, durante febrero de 2021, en Twitter fundamentalmente sobre programación funcional y demostración asistida por ordenador.
Las lecturas están ordenadas según su fecha de publicación en Twitter.
Al final de cada artículo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.
Una recopilación de todas las lecturas compartidas se encuentra en GitHub.
Esta entrada es una recopilación de lecturas compartidas, durante enero de 2021, en Twitter fundamentalmente sobre programación funcional y demostración asistida por ordenador.
Las lecturas están ordenadas según su fecha de publicación en Twitter.
Al final de cada artículo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.
Una recopilación de todas las lecturas compartidas se encuentra en GitHub.
He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo en el que se comentan 11 pruebas en Lean de la propiedad
La función identidad no está acotada superiormente
usando los estilos aplicativo, declarativo, y funcional.
A continuación, se muestra el vídeo
y el código de la teoría utilizada
import data.real.basic -- ---------------------------------------------------- -- Ejercicio 1. Definir la función -- acotada_superiormente : (ℝ → ℝ) → Prop -- tal que (acotada_superiormente f) expresa que la -- función f está acotada superiormente. -- ---------------------------------------------------- def acotada_superiormente : (ℝ → ℝ) → Prop | f := ∃ M, ∀ x, f x ≤ M -- ---------------------------------------------------- -- Ejercicio 2. Demostrar que la función identidad no -- está acotada superiormente. -- ---------------------------------------------------- -- 1ª demostración example : ¬acotada_superiormente id := begin unfold acotada_superiormente, unfold id, by_contradiction h, cases h with M hM, specialize hM (M+1), contrapose hM, simp only [not_le], exact lt_add_one M, end -- 2ª demostración example : ¬acotada_superiormente id := begin unfold acotada_superiormente id, push_neg, intro M, use M + 1, linarith, end -- 3ª demostración example : ¬acotada_superiormente id := begin unfold acotada_superiormente id, push_neg, exact no_top, end -- 4ª demostración example : ¬acotada_superiormente id := assume h1 : acotada_superiormente id, have h2 : ∃ M, ∀ x, id x ≤ M, from h1, show false, from exists.elim h2 ( assume M, assume hM : ∀ x, id x ≤ M, have h3 : M + 1 ≤ M, from hM (M+1), have h4 : ¬(M < M + 1), from not_lt.mpr h3, have h5 : M < M + 1, from lt_add_one M, show false, from h4 h5) -- 5ª demostración example : ¬acotada_superiormente id := assume h1 : acotada_superiormente id, have h2 : ∃ M, ∀ x, id x ≤ M, from h1, show false, from exists.elim h2 ( assume M, assume hM : ∀ x, id x ≤ M, have h3 : M + 1 ≤ M, from hM (M+1), have h4 : ¬(M < M + 1), from not_lt.mpr h3, have h5 : M < M + 1, from lt_add_one M, h4 h5) -- 6ª demostración example : ¬acotada_superiormente id := assume h1 : acotada_superiormente id, have h2 : ∃ M, ∀ x, id x ≤ M, from h1, show false, from exists.elim h2 ( assume M, assume hM : ∀ x, id x ≤ M, have h3 : M + 1 ≤ M, from hM (M+1), (not_lt.mpr h3) (lt_add_one M)) -- 7ª demostración example : ¬acotada_superiormente id := assume h1 : acotada_superiormente id, have h2 : ∃ M, ∀ x, id x ≤ M, from h1, show false, from exists.elim h2 ( assume M, assume hM : ∀ x, id x ≤ M, (not_lt.mpr (hM (M+1))) (lt_add_one M)) -- 8ª demostración example : ¬acotada_superiormente id := assume h1 : acotada_superiormente id, have h2 : ∃ M, ∀ x, id x ≤ M, from h1, show false, from exists.elim h2 (λ M hM, (not_lt.mpr (hM (M+1))) (lt_add_one M)) -- 9ª demostración example : ¬acotada_superiormente id := assume h1 : acotada_superiormente id, have h2 : ∃ M, ∀ x, id x ≤ M, from h1, exists.elim h2 (λ M hM, (not_lt.mpr (hM (M+1))) (lt_add_one M)) -- 10ª demostración example : ¬acotada_superiormente id := assume h1 : acotada_superiormente id, exists.elim h1 (λ M hM, (not_lt.mpr (hM (M+1))) (lt_add_one M)) -- 11ª demostración example : ¬acotada_superiormente id := λ h1, exists.elim h1 (λ M hM, (not_lt.mpr (hM (M+1))) (lt_add_one M)) |
He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo en el que se comentan 6 pruebas en Lean de la propiedad
¬par f ↔ ∃ x, f (-x) ≠ f x
usando los estilos declarativo, aplicativo y automático.
A continuación, se muestra el vídeo
y el código de la teoría utilizada
import data.real.basic variable (f : ℝ → ℝ) -- ---------------------------------------------------- -- Ejercicio 1. Definir la función -- par : (ℝ → ℝ) → Prop -- tal que (par f) expresa que f es par. -- ---------------------------------------------------- def par : (ℝ → ℝ) → Prop | f := ∀ x, f (-x) = f x -- ---------------------------------------------------- -- Ejercicio 2. Demostrar que -- ¬par f ↔ ∃ x, f (-x) ≠ f x -- ---------------------------------------------------- -- 1ª demostración example : ¬par f ↔ ∃ x, f (-x) ≠ f x := begin split, { contrapose, intro h1, rw not_not, unfold par, intro x, by_contradiction h2, apply h1, use x, }, { intro h1, intro h2, unfold par at h2, cases h1 with x hx, apply hx, exact h2 x, }, end -- 2ª demostración example : ¬par f ↔ ∃ x, f (-x) ≠ f x := begin split, { contrapose, intro h1, rw not_not, intro x, by_contradiction h2, apply h1, use x, }, { rintros ⟨x, hx⟩ h', exact hx (h' x) }, end -- 3ª demostración example : ¬par f ↔ ∃ x, f (-x) ≠ f x := begin unfold par, push_neg, end -- 4ª demostración example : ¬par f ↔ ∃ x, f (-x) ≠ f x := iff.intro ( have h1 : ¬(∃ x, f (-x) ≠ f x) → ¬¬par f, { assume h2 : ¬(∃ x, f (-x) ≠ f x), have h3 : par f, { assume x, have h4 : ¬(f (-x) ≠ f x), { assume h5 : f (-x) ≠ f x, have h6 : ∃ x, f (-x) ≠ f x, from exists.intro x h5, show false, from h2 h6, }, show f (-x) = f x, from not_not.mp h4}, show ¬¬par f, from not_not.mpr h3 }, show ¬par f → (∃ x, f (-x) ≠ f x), from not_imp_not.mp h1) ( assume h1 : ∃ x, f (-x) ≠ f x, show ¬par f, { assume h2 : par f, show false, from exists.elim h1 ( assume x, assume hx : f (-x) ≠ f x, have h3 : f (-x) = f x, from h2 x, show false, from hx h3)}) -- 5ª demostración example : ¬par f ↔ ∃ x, f (-x) ≠ f x := -- by suggest not_forall -- 6ª demostración example : ¬par f ↔ ∃ x, f (-x) ≠ f x := -- by hint by simp [par] |
