jaalonso/Calculemus

Ejercicios de demostración con Lean e Isabelle/HOL.

Calculemus (Ejercicios de demostración asistida por ordenador)

En este repositorio se encuentran los ejercicios propuestos en Calculemus para demostrarlos con asistentes de pruebas (como Isabelle/HOL y Lean).

• Reto f (f (f b)) = f b.
• Teorema de Nicómaco.
• Praeclarum theorema.
• El problema lógico del mal.
• La dama o el tigre.
• El problema de los infectados.
• El problema del barbero.
• Las reflexivas circulares son simétricas.
• Propiedad de monotonía de la intersección (En Lean y en Isabelle).
• Propiedad semidistributiva de la intersección sobre la unión (En Lean y en Isabelle).
• Diferencia de diferencia de conjuntos (En Lean y en Isabelle).
• 2ª propiedad semidistributiva de la intersección sobre la unión (En Lean y en Isabelle).
• 2ª diferencia de diferencia de conjuntos (En Lean y en Isabelle).
• Conmutatividad de la intersección (En Lean y en Isabelle).
• Intersección con su unión (En Lean y en Isabelle).
• Unión con su intersección (En Lean y en Isabelle).
• Unión con su diferencia (En Lean y en Isabelle).
• Diferencia de unión e intersección (En Lean y en Isabelle).
• Unión de los conjuntos de los pares e impares (En Lean y en Isabelle).
• Intersección de los primos y los mayores que dos (En Lean y en Isabelle).
• Distributiva de la intersección respecto de la unión general (En Lean y en Isabelle).
• Intersección de intersecciones (En Lean y en Isabelle).
• Unión con intersección general (En Lean y en Isabelle).
• Imagen inversa de la intersección (En Lean y en Isabelle).
• Imagen de la unión (En Lean y en Isabelle).
• Imagen inversa de la imagen (En Lean y en Isabelle).
• Subconjunto de la imagen inversa (En Lean y en Isabelle).
• Imagen inversa de la imagen de aplicaciones inyectivas (En Lean y en Isabelle).
• Imagen de la imagen inversa (En Lean y en Isabelle).
• Imagen de imagen inversa de aplicaciones suprayectivas (En Lean y en Isabelle).
• Monotonía de la imagen de conjuntos (En Lean y en Isabelle).
• Monotonía de la imagen inversa (En Lean y en Isabelle).
• Imagen inversa de la unión (En Lean y en Isabelle).
• Imagen de la intersección (En Lean y en Isabelle).
• Imagen de la intersección de aplicaciones inyectivas (En Lean y en Isabelle).
• Imagen de la diferencia de conjuntos (En Lean y en Isabelle).
• Imagen inversa de la diferencia (En Lean y en Isabelle).
• Intersección con la imagen (En Lean y en Isabelle).
• Unión con la imagen (En Lean y en Isabelle).
• Intersección con la imagen inversa (En Lean y en Isabelle).
• Unión con la imagen inversa (En Lean y en Isabelle).
• Imagen de la unión general (En Lean y en Isabelle).
• Imagen de la intersección general (En Lean y en Isabelle).
• Imagen de la intersección general mediante inyectiva (En Lean y en Isabelle).
• Imagen inversa de la unión general (En Lean y en Isabelle).
• Imagen inversa de la intersección general (En Lean y en Isabelle).
• Teorema de Cantor (En Lean y en Isabelle).
• En los monoides, los inversos a la izquierda y a la derecha son iguales (En Lean y en Isabelle).
• Producto_de_potencias_de_la_misma_base_en_monoides (En Lean y en Isabelle).
• Equivalencia de inversos iguales al neutro (En Lean y en Isabelle).
• Unicidad de inversos en monoides (En Lean y en Isabelle).
• Caracterización de producto igual al primer factor (En Lean y en Isabelle).
• Unicidad del elemento neutro en los grupos (En Lean y en Isabelle).
• Unicidad de los inversos en los grupos (En Lean y en Isabelle).
• Inverso del producto (En Lean y en Isabelle).
• Inverso del inverso en grupos (En Lean y en Isabelle).
• Propiedad cancelativa en grupos (En Lean y en Isabelle).
• Potencias de potencias en monoides (En Lean y en Isabelle).
• Los monoides booleanos son conmutativos (En Lean y en Isabelle).
• Límite de sucesiones constantes (En Lean y en Isabelle).
• Unicidad del límite de las sucesiones convergentes (En Lean y en Isabelle).
• Límite cuando se suma una constante (En Lean y en Isabelle).
• Límite de la suma de sucesiones convergentes (En Lean y en Isabelle).
• Límite multiplicado por una constante (En Lean y en Isabelle).
• El límite de u es a syss el de u-a es 0 (En Lean y en Isabelle).
• Producto de sucesiones convergentes a cero (En Lean y en Isabelle).
• Teorema del emparedado (En Lean y en Isabelle).
• La composición de crecientes es creciente (En Lean y en Isabelle).
• La composición de una función creciente y una decreciente es decreciente (En Lean y en Isabelle).
• Una función creciente e involutiva es la identidad (En Lean y en Isabelle).
• Si `f x ≤ f y → x ≤ y`, entonces f es inyectiva (En Lean y en Isabelle).
• Los supremos de las sucesiones crecientes son sus límites (En Lean y en Isabelle).
• Un número es par syss lo es su cuadrado (En Lean y en Isabelle).
• Acotación de sucesiones convergentes (En Lean y en Isabelle).
• La paradoja del barbero (En Lean y en Isabelle).
• Propiedad de la densidad de los reales (En Lean y en Isabelle).
• Propiedad cancelativa del producto de números naturales (En Lean y en Isabelle).
• Límite de sucesión menor que otra sucesión (En Lean y en Isabelle).
• Las sucesiones acotadas por cero son nulas (En Lean y en Isabelle).
• Producto de una sucesión acotada por otra convergente a cero (En Lean y en Isabelle).
• La congruencia módulo 2 es una relación de equivalencia (En Lean y en Isabelle).
• Las funciones con inversa por la izquierda son inyectivas (En Lean y en Isabelle).
• Las funciones inyectivas tienen inversa por la izquierda (En Lean y en Isabelle).
• Una función tiene inversa por la izquierda si y solo si es inyectiva (En Lean y en Isabelle).
• Las funciones con inversa por la derecha son suprayectivas (En Lean y en Isabelle).
• Las funciones suprayectivas tienen inversa por la derecha (En Lean y en Isabelle).
• Una función tiene inversa por la derecha si y solo si es suprayectiva (En Lean y en Isabelle).
• Las funciones con inversa son biyectivas (En Lean y en Isabelle).
• Las funciones biyectivas tienen inversa (En Lean y en Isabelle).
• Una función tiene inversa si y solo si es biyectiva (En Lean y en Isabelle).
• La equipotencia es una relación reflexiva (En Lean y en Isabelle).
• La inversa de una función biyectiva es biyectiva (En Lean y en Isabelle).
• La equipotencia es una relación simétrica (En Lean y en Isabelle).
• La composición de funciones inyectivas es inyectiva (En Lean y en Isabelle).
• La composición de funciones suprayectivas es suprayectiva (En Lean y en Isabelle).
• La composición de funciones biyectivas es biyectiva (En Lean y en Isabelle).
• La equipotencia es una relación transitiva (En Lean y en Isabelle).
• La equipotencia es una relación de equivalencia (En Lean y en Isabelle).
• La igualdad de valores es una relación de equivalencia (En Lean y en Isabelle).
• La composición por la izquierda con una inyectiva es una operación inyectiva (En Lean y en Isabelle).
• Las sucesiones convergentes son sucesiones de Cauchy (En Lean y en Isabelle).
• Las clases de equivalencia de elementos relacionados son iguales (En Lean y en Isabelle).
• Las clases de equivalencia de elementos no relacionados son disjuntas (En Lean y en Isabelle).
• El conjunto de las clases de equivalencia es una partición (En Lean y en Isabelle).
• Las particiones definen relaciones reflexivas (En Lean y en Isabelle).
• Las familias de conjuntos definen relaciones simétricas (En Lean y en Isabelle).
• Las particiones definen relaciones transitivas (En Lean y en Isabelle).
• Las particiones definen relaciones de equivalencia (En Lean y en Isabelle).
• Relación entre los índices de las subsucesiones y de la sucesión (En Lean y en Isabelle).
• Las funciones de extracción no están acotadas (En Lean y en Isabelle).
• Si a es un punto de acumulación de u, entonces ∀ε>0, ∀ N, ∃k≥N, |u(k)−a| < ε (En Lean y en Isabelle).
• Las subsucesiones tienen el mismo límite que la sucesión (En Lean y en Isabelle).
• El punto de acumulación de las sucesiones convergente es su límite (En Lean y en Isabelle).
• La_suma_de_los_n_primeros_impares_es_n^2 (En Lean y en Isabelle).
• Si a es un punto de acumulación de la sucesión de Cauchy u, entonces a es el límite de u (En Lean y en Isabelle).
• Las sucesiones divergentes positivas no_tienen límites finitos (En Lean y en Isabelle).
• Límite de sucesiones no decrecientes (En Lean y en Isabelle).
• Pruebas de length (repeat x n) = n (En Lean y en Isabelle).
• Asociatividad de la concatenación de listas (En Lean y en Isabelle).
• Pruebas de length(xs ++ ys) =_length(xs) + length(ys) (En Lean y en Isabelle).
• Pruebas de take n xs ++ drop n xs = xs (En Lean y en Isabelle).
• Pruebas de equivalencia de definiciones de inversa (En Lean y en Isabelle).
• Pruebas de que la función espejo de los árboles binarios es involutiva (En Lean y en Isabelle).
• Razonamiento sobre árboles binarios: Aplanamiento e imagen especular (En Lean y en Isabelle).
• Si x es el supremo de A, entonces ∀ y, y < x → ∃ a ∈ A, y < a (En Lean y en Isabelle).
• (∀ ε > 0, y ≤ x + ε) → y ≤ x (En Lean y en Isabelle).
• Los límites son menores o iguales que las cotas superiores (En Lean y en Isabelle).
• Si f es continua en a y el límite de u(n) es a, entonces el límite de f(u(n)) es f(a) (En Lean y en Isabelle).
• Suma de los primeros números naturales (En Lean y en Isabelle).
• Suma de progresión aritmética (En Lean y en Isabelle).
• Suma de progresión geométrica (En Lean y en Isabelle).
• Suma de los primeros cuadrados (En Lean y en Isabelle).
• Suma de los primeros cubos (En Lean y en Isabelle).
• Prueba de (1+p)^n mayor o igual que 1+np (En Lean y en Isabelle).
• Formula_de_Gauss_de_la_suma (En Lean y en Isabelle).
• Suma de potencias de dos (En Lean y en Isabelle).
• Identidad de Brahmagupta-Fibonacci (En Lean y en Isabelle).
• Igualdad_de_bloques_de_una_particion_cuando_tienen_elementos_comunes (En Lean).
• Pertenencia a bloques de una partición con elementos comunes (En Lean).
• Pertenencia a su propia clase de equivalencia (En Lean).
• Las clases de equivalencia contienen a las clases de equivalencia de_sus elementos (En Lean).
• Las clases de equivalencia son iguales a las de sus elementos (En Lean).
• Las clases de equivalencia son no vacías (En Lean).
• Las clases de equivalencia recubren el conjunto (En Lean).
• Las clases de equivalencia son disjuntas (En Lean).
• El cociente aplica relaciones de equivalencia en particiones (En Lean).
• Las relaciones definidas por particiones son reflexivas (En Lean).
• Las relaciones definidas por particiones son simétricas (En Lean).
• Las relaciones definidas por particiones son transitivas (En Lean).
• Aplicación de particiones en relaciones de equivalencia (En Lean).
• La función relacionP es inversa por la izquierda de la función cociente (En Lean).
• La función relacionP es inversa por la derecha de la función cociente (En Lean).
• Isomorfismo entre relaciones de equivalencia y particiones (En Lean).
• Propiedad de monotonía de la intersección (En Lean y en Isabelle).
• Propiedad semidistributiva de la intersección sobre la unión (En Lean y en Isabelle).
• Diferencia de diferencia de conjuntos (En Lean y en Isabelle).
• Intersección con su unión (En Lean y en Isabelle).
• Distributiva de la intersección respecto de la unión general (En Lean y en Isabelle).
• Imagen inversa de la intersección (En Lean y en Isabelle).
• Imagen de la unión (En Lean y en Isabelle).
• Teorema de Cantor (En Lean y en Isabelle).
• Si_g·f_es_inyectiva_entonces_f_es_inyectiva (En Lean y en Isabelle).
• Si g·f es suprayectiva, entonces g es suprayectiva (En Lean y en Isabelle).
• Si f·f es biyectiva entonces f es biyectiva (En Lean y en Isabelle).
• El producto por un par es par (En Lean).
• Si a, b y c son números reales, entonces (a * b) * c = b * (a * c) (En Lean).
• Si a, b, c, d, e y f son números reales tales que a * b = c * d y e = f entonces, a * (b * e) = c * (d * f) (En Lean).
• Si a y b son números reales, entonces (a + b) * (a + b) = a * a + 2 * (a * b) + b * b (En Lean).
• Si a, b, c y d son números reales, entonces (a + b) * (c + d) = a * c + a * d + b * c + b * d (En Lean).
• Si a y b son números reales, entonces (a + b) * (a - b) = a^2 - b^2 (En Lean).
• Si R es un anillo y a, b ∈ R, entonces -a + (a + b) = b (En Lean).
• Si R es un anillo y a, b ∈ R, entonces (a + b) + -b = a (En Lean).
• Si R es un anillo y a, b, c ∈ R tales que a + b = a + c, entonces b = c. (En Lean).
• Si R es un anillo y a, b, c ∈ R tales que a + b = c + b, entonces a = c. (En Lean).
• Si R es un anillo y a ∈ R, entonces a * 0 = 0 (En Lean).
• Si R es un anillo y a ∈ R, entonces 0 * a = 0 (En Lean).
• Si R es un anillo y a,b∈R tales que a+b=0, entonces -a=b (En Lean).
• Si R es un anillo y a,b∈R tales que a+b=0, entonces a=-b (En Lean).
• Si R es un anillo, entonces -0 = 0 (En Lean)
• Si R es un anillo y a ∈ R, entonces -(-a) = a (En Lean).
• Si R es un anillo y a,b∈R, entonces a-b=a+(-b) (En Lean).
• Si R es un anillo y a ∈ R, entonces 2 * a = a + a (En Lean).
• Si G es un grupo y a ∈ G, entonces a * a⁻¹ = 1 (En Lean).
• Si G es un grupo y a ∈ G, entonces a * 1 = a (En Lean).
• Si G es un grupo y a, b ∈ G tales que b * a = 1, entonces a⁻¹ = b (En Lean).
• Si G es un grupo y a, b ∈ G, entonces (a * b)⁻¹ = b⁻¹ * a⁻¹ (En Lean).
• Si a, b, c, d, e ∈ ℝ tales que a ≤ b, b < c, c ≤ d, d < e, entonces a < e (En Lean).
• Si a, b, d ∈ ℝ tales que 1 ≤ a y b ≤ d, entonces 2 + a + eᵇ ≤ 3a + eᵈ (En Lean).
• Si a, b, c, d, f ∈ ℝ tales que a ≤ b y c < d, entonces a + eᶜ + f < b + eᵈ + f (En Lean).
• Si a, b ∈ ℝ tales que a ≤ b, entonces log(1 + eᵃ) ≤ log(1 + eᵇ) (En Lean).
• Si a, b, c ∈ ℝ tales que a ≤ b, entonces c - eᵇ ≤ c - eᵃ (En Lean]).
• Si a, b ∈ ℝ, entonces 2ab ≤ a² + b² (En Lean).
• Si a, b ∈ ℝ, entonces |ab| ≤ (a^2 + b^2)/2 (En Lean).
• Si a, b ∈ ℝ, entonces min(a,b) = min(b,a) (En Lean).
• Si a, b ∈ ℝ, entonces max(a,b) = max(b,a) (En Lean).
• Si a, b, c ∈ ℝ, entonces min(min(a,b),c) = min(a,min(b,c)) (En Lean).
• Si a, b, c ∈ ℝ, entonces min a b + c = min (a + c) (b + c) (En Lean).
• Si a, b ∈ ℝ, entonces |a| - |b| ≤ |a - b| (En Lean).
• Si x, y, z ∈ ℕ, entonces x ∣ y * x * z (En Lean).
• Si x ∈ ℕ, entonces x ∣ x^2 (En Lean).
• Si w,x,y,z ∈ ℕ tales que x ∣ w, entonces x ∣ yxz + x² + w² (En Lean).
• Si m, n ∈ ℕ, entonces gcd(m,n) = gcd(n,m) (En Lean).
• Si R es un retículo y x, y ∈ R, entonces x ⊓ y = y ⊓ x (En Lean).
• Si R es un retículo y x, y ∈ R, entonces x ⊔ y = y ⊔ x (En Lean).
• Si R es un retículo y x, y, z ∈ R, entonces (x ⊓ y) ⊓ z = x ⊓ (y ⊓ z) (En Lean).
• Si R es un retículo y x, y, z ∈ R, entonces (x ⊔ y) ⊔ z = x ⊔ (y ⊔ z) (En Lean).
• Si R es un retículo y x, y ∈ R, entonces x ⊓ (x ⊔ y) = x (En Lean).
• Si R es un retículo y x, y ∈ R, entonces x ⊔ (x ⊓ y) = x (En Lean).
• Si R es un retículo tal que x ⊓ (y ⊔ z) = (x ⊓ y) ⊔ (x ⊓ z), entonces (a ⊔ b) ⊓ c = (a ⊓ c) ⊔ (b ⊓ c) (En Lean).
• Si R es un retículo tal que x ⊔ (y ⊓ z) = (x ⊔ y) ⊓ (x ⊔ z), entonces (a ⊓ b) ⊔ c = (a ⊔ c) ⊓ (b ⊔ c) (En Lean).
• Si R es un anillo ordenado y a, b ∈ R, entonces a ≤ b → 0 ≤ b - a (En Lean).
• Si R es un anillo ordenado y a, b ∈ R, entonces 0 ≤ b - a → a ≤ b (En Lean).
• Si R es un anillo ordenado y a, b, c ∈ R tales que a ≤ b y 0 ≤ c, entonces a * c ≤ b * c (En Lean).
• Si X es un espacio métrico y x, y ∈ X, entonces dist(x,y) ≥ 0 (En Lean).
• Si x,y,ε ∈ ℝ tales que 0 < ε ≤ 1, |x| < ε y |y| < ε, entonces |x*y| < ε (En Lean).
• La suma de una cota superior de f y una cota superior de g es una cota superior de f+g (En Lean).
• La suma de una cota inferior de f y una cota inferior de g es una cota inferior de f+g (En Lean).
• El producto de dos funciones no negativas es no negativa (En Lean).
• Si a es una cota superior no negativa de f y b es es una cota superior de la función no negativa g, entonces a·b es una cota superior de f·g (En Lean).
• La suma de dos funciones monótonas es monótona (En Lean).
• Si f es monótona y c ≥ 0, entonces c·f es monótona. (En Lean).
• Composicion_de_funciones_monotonas (En Lean).
• La suma de dos funciones pares es par. (En Lean).

El producto de dos funciones impares es par (En Lean).

• El producto de una función par por una impar es impar. (En Lean).
• Si f es par y g es impar, entonces f ∘ g es par (En Lean).
• Para cualquier conjunto s, s ⊆ s (En Lean).
• Si r ⊆ s y s ⊆ t, entonces r ⊆ t (En Lean).
• Si a es una cota superior de s y a ≤ b, entonces b es una cota superior de s (En Lean).
• Para todo c ∈ ℝ, la función f(x) = x+c es inyectiva (En Lean).
• Para todo c ∈ ℝ-{0}, la función f(x) = x * c es inyectiva (En Lean).
• Composicion_de_funciones_inyectivas (En Lean).
• ∃ x ∈ ℝ, 2 < x < 3 (En Lean).
• La suma de dos funciones acotadas superiormente también lo está (En Lean).
• La suma de dos funciones acotadas inferiormente también lo está (En Lean).
• Si c ≥ 0 y f está acotada superiormente, entonces c * f también lo está (En Lean).
• Si x e y son sumas de dos cuadrados, entonces xy también lo es (En Lean).
• La relación de divisibilidad es transitiva (En Lean).
• Si a divide a b y a c, entonces tambien divide a b + c. (En Lean).