mayo 2021 – Calculemus

Unión de los conjuntos de los pares e impares

PorJosé A. Alonso 31 mayo 202121 agosto 2021

Los conjuntos de los números naturales, de los pares y de los impares se definen por

   def naturales : set ℕ := {n | true}
   def pares     : set ℕ := {n | even n}
   def impares   : set ℕ := {n | ¬ even n}

def naturales : set ℕ := {n | true}

def pares : set ℕ := {n | even n}

def impares : set ℕ := {n | ¬ even n}

Demostrar que

   pares ∪ impares = naturales

1	pares ∪ impares = naturales

Para ello, completar la siguiente teoría de Lean:

import data.nat.parity
import data.set.basic
import tactic

open set

def naturales : set ℕ := {n | true}
def pares     : set ℕ := {n | even n}
def impares   : set ℕ := {n | ¬ even n}

example : pares ∪ impares = naturales :=
sorry

import data.nat.parity

import data.set.basic

import tactic

open set

def naturales : set ℕ := {n | true}

def pares : set ℕ := {n | even n}

def impares : set ℕ := {n | ¬ even n}

example : pares ∪ impares = naturales :=

sorry

Diferencia de unión e intersección

PorJosé A. Alonso 28 mayo 202127 mayo 2021

Demostrar que

(s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t)

Para ello, completar la siguiente teoría de Lean:

import data.set.basic
open set

variable {α : Type}
variables s t : set α

example : (s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t) :=
sorry

import data.set.basic

open set

variable {α : Type}

variables s t : set α

example : (s \ t) ∪ (t \ s) = (s ∪ t) \ (s ∩ t) :=

sorry

Soluciones

Unión con su diferencia

PorJosé A. Alonso 27 mayo 202126 mayo 2021

Demostrar que

(s \ t) ∪ t = s ∪ t

Para ello, completar la siguiente teoría de Lean:

import data.set.basic
open set

variable {α : Type}
variables s t : set α

example : (s \ t) ∪ t = s ∪ t :=
sorry

import data.set.basic

open set

variable {α : Type}

variables s t : set α

example : (s \ t) ∪ t = s ∪ t :=

sorry

Unión con su intersección

PorJosé A. Alonso 26 mayo 202125 mayo 2021

Demostrar que

s ∪ (s ∩ t) = s

Para ello, completar la siguiente teoría de Lean:

import data.set.basic
open set

variable {α : Type}
variables s t : set α

example : s ∪ (s ∩ t) = s :=
sorry

import data.set.basic

open set

variable {α : Type}

variables s t : set α

example : s ∪ (s ∩ t) = s :=

sorry

Read More «Unión con su intersección»

Conmutatividad de la intersección

PorJosé A. Alonso 24 mayo 202124 mayo 2021

Demostrar que

s ∩ t = t ∩ s

Para ello, completar la siguiente teoría de Lean:

import data.set.basic
open set

variable {α : Type}
variables s t u : set α

example : s ∩ t = t ∩ s :=
sorry

import data.set.basic

open set

variable {α : Type}

variables s t u : set α

example : s ∩ t = t ∩ s :=

sorry

Notas

En este enlace se puede escribir las soluciones en Lean.
A continuación se muestran algunas soluciones (que se pueden probar en este enlace).
En los comentarios se pueden publicar otras soluciones, en Lean o en otros sistemas de razonamiento.
- Para publicar las demostraciones en Lean se deben de escribir entre una línea con <pre lang="lean"> y otra con </pre>
- Para publicar las demostraciones en Isabelle/HOL se deben de escribir entre una línea con <pre lang="isar"> y otra con </pre>

2ª diferencia de diferencia de conjuntos

PorJosé A. Alonso 21 mayo 202124 mayo 2021

Demostrar que

s \ (t ∪ u) ⊆ (s \ t) \ u

Para ello, completar la siguiente teoría de Lean:

import data.set.basic
open set

variable {α : Type}
variables s t u : set α

example : s \ (t ∪ u) ⊆ (s \ t) \ u :=
sorry

import data.set.basic

open set

variable {α : Type}

variables s t u : set α

example : s \ (t ∪ u) ⊆ (s \ t) \ u :=

sorry

Notas

En este enlace se puede escribir las soluciones en Lean.
A continuación se muestran algunas soluciones (que se pueden probar en este enlace).
En los comentarios se pueden publicar otras soluciones, en Lean o en otros sistemas de razonamiento.
- Para publicar las demostraciones en Lean se deben de escribir entre una línea con <pre lang="lean"> y otra con </pre>
- Para publicar las demostraciones en Isabelle/HOL se deben de escribir entre una línea con <pre lang="isar"> y otra con </pre>

2ª propiedad semidistributiva de la intersección sobre la unión

PorJosé A. Alonso 20 mayo 202124 mayo 2021

Demostrar que

(s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u)

Para ello, completar la siguiente teoría de Lean:

import data.set.basic
open set

variable {α : Type}
variables s t u : set α

example : (s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u):=
sorry

import data.set.basic

open set

variable {α : Type}

variables s t u : set α

example : (s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u):=

sorry

Notas

En este enlace se puede escribir las soluciones en Lean.
A continuación se muestran algunas soluciones (que se pueden probar en este enlace).
En los comentarios se pueden publicar otras soluciones, en Lean o en otros sistemas de razonamiento.
- Para publicar las demostraciones en Lean se deben de escribir entre una línea con <pre lang="lean"> y otra con </pre>
- Para publicar las demostraciones en Isabelle/HOL se deben de escribir entre una línea con <pre lang="isar"> y otra con </pre>

Propiedad semidistributiva de la intersección sobre la unión

PorJosé A. Alonso 18 mayo 202121 abril 2022

Demostrar que

s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u)

Para ello, completar la siguiente teoría de Lean:

import data.set.basic
open set

variable {α : Type}
variables s t u : set α

example :
  s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) :=
sorry

import data.set.basic

open set

variable {α : Type}

variables s t u : set α

example :

s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) :=

sorry

Notas

En este enlace se puede escribir las soluciones en Lean.
A continuación se muestran algunas soluciones (que se pueden probar en este enlace).
En los comentarios se pueden publicar otras soluciones, en Lean o en otros sistemas de razonamiento.
- Para publicar las demostraciones en Lean se deben de escribir entre una línea con <pre lang="lean"> y otra con </pre>
- Para publicar las demostraciones en Isabelle/HOL se deben de escribir entre una línea con <pre lang="isar"> y otra con </pre>

Propiedad de monotonía de la intersección

PorJosé A. Alonso 17 mayo 202118 abril 2022

Demostrar que la intersección es monótona por la izquierda; es decir, si

s ⊆ t,

entonces

s ∩ u ⊆ t ∩ u.

Para ello, completar la siguiente teoría de Lean:

import data.set.basic
open set

variable {α : Type}
variables s t u : set α

example
  (h : s ⊆ t)
  : s ∩ u ⊆ t ∩ u :=
sorry

import data.set.basic

open set

variable {α : Type}

variables s t u : set α

example

(h : s ⊆ t)

: s ∩ u ⊆ t ∩ u :=

sorry

Notas

En este enlace se puede escribir las soluciones en Lean.
A continuación se muestran algunas soluciones (que se pueden probar en este enlace).
En los comentarios se pueden publicar otras soluciones, en Lean o en otros sistemas de razonamiento.
- Para publicar las demostraciones en Lean se deben de escribir entre una línea con <pre lang="lean"> y otra con </pre>
- Para publicar las demostraciones en Isabelle/HOL se deben de escribir entre una línea con <pre lang="isar"> y otra con </pre>

Sobre Calculemus

PorJosé A. Alonso 16 mayo 202121 agosto 2021

El objetivo principal de Calculemus es proponer ejercicios de demostración de resultados matemáticos usando sistemas de demostración interactiva, fundamentalmente Lean e Isabelle/HOL.

En los enunciados de los ejercicios se da la plantilla para Lean.

Las soluciones propuestas están en la versión 3.30.0 de Lean y en la versión 2021 de Isabelle/HOL. Las distintas soluciones están ordenadas desde las más detalladas a las más automáticas. Además, las soluciones están en este repositorio de GitHub.

Es recomendable, antes de leer las soluciones propuestas, intentar escribir demostraciones propias (en el caso de Lean se pueden probar en el navegador a través de este enlace).

En los comentarios se pueden publicar demostraciones distintas de las propuestas en Lean, Isabelle/HOL u otros sistemas (como Coq, Agda o PVS.