Menu Close

Mes: octubre 2020

ForMatUS: Pruebas en Lean de que las partes simétricas son simétricas

José A. Alonso--

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 6 pruebas en Lean de la siguiente propiedad: “Si R es una relación, entonces su parte simétrica (es decir, la relación S definida por S x y := R x y ∧ R y x) es simétrica”, usando los estilos declarativos, aplicativos, funcional y automático.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

-- ----------------------------------------------------
-- Ej. 1. La parte simétrica de una relación R es la
-- relación S definida por
--    S x y := R x y ∧ R y x
--
-- Demostrar que la parte simétrica de cualquier
-- relación es simétrica.
-- ----------------------------------------------------
 
section
parameter A : Type
parameter R : A → A → Prop
 
def S (x y : A) := R x y ∧ R y x
 
-- 1ª demostración
example : symmetric S :=
begin
  intros x y h,
  split,
  { exact h.right, },
  { exact h.left, },
end
 
-- 2ª demostración
example : symmetric S :=
begin
  intros x y h,
  exact ⟨h.right, h.left⟩,
end
 
-- 3ª demostración
example : symmetric S :=
λ x y h, ⟨h.right, h.left⟩
 
-- 4ª demostración
example : symmetric S :=
assume x y,
assume h : S x y,
have h1 : R x y, from h.left,
have h2 : R y x, from h.right,
show S y x, from ⟨h2, h1⟩
 
-- 5ª demostración
example : symmetric S :=
assume x y,
assume h : S x y,
show S y x, from ⟨h.right, h.left⟩
 
-- 6ª demostración
example : symmetric S :=
λ x y h, ⟨h.right, h.left⟩
 
end
Seguir leyendo →

ForMatUS: Pruebas en Lean de que las partes simétricas de las relaciones reflexivas son reflexivas

José A. Alonso--

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 5 pruebas en Lean de que las partes simétricas de las relaciones reflexivas son reflexivas usando los estilos aplicativos, declarativos y funcional.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

-- ----------------------------------------------------
-- Ej. 1. La parte simétrica de una relación R es la
-- relación S definida por
--    S x y := R x y ∧ R y x
--
-- Demostrar que la parte simétrica de una relación
-- reflexiva es reflexiva.
-- ----------------------------------------------------
 
section
 
parameter A : Type
parameter R : A → A → Prop
parameter reflR : reflexive R
 
include reflR
 
def S (x y : A) := R x y ∧ R y x
 
-- 1ª demostración
example : reflexive S :=
begin
  intro x,
  split,
  { exact (reflR x), },
  { exact (reflR x), },
end
 
-- 2ª demostración
example : reflexive S :=
assume x,
have R x x, from reflR x,
show S x x, from and.intro this this
 
-- 3ª demostración
example : reflexive S :=
assume x,
show S x x, from and.intro (reflR x) (reflR x)
 
-- 4ª demostración
example : reflexive S :=
assume x,
and.intro (reflR x) (reflR x)
 
-- 5ª demostración
example : reflexive S :=
λ x, ⟨reflR x, reflR x⟩
 
end
Seguir leyendo →

ForMatUS: Pruebas en Lean de que las partes estrictas de los órdenes parciales son transitivas

José A. Alonso--

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 2 pruebas en Lean de que las partes estrictas de los órdenes parciales son transitivas usando los estilos aplicativos y declarativos.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

-- ----------------------------------------------------
-- Ej. 1. La parte estricta de una relación R es la
-- relación R' definida por
--    R' a b := R a b ∧ a ≠ b
--
-- Demostrar que si R es un orden parcial, entonces su
-- parte estricta es transitiva.
-- ----------------------------------------------------
 
import tactic
 
section
 
parameter {A : Type}
parameter (R : A → A → Prop)
parameter (reflR    : reflexive R)
parameter (transR   : transitive R)
parameter (antisimR : anti_symmetric R)
variables {a b c : A}
 
definition R' (a b : A) : Prop :=
  R a b ∧ a ≠ b
 
include transR
include antisimR
 
-- 1ª demostración
example : transitive R' :=
begin
  rintros a b c ⟨h1,h2⟩ ⟨h3,h4⟩,
  split,
  { apply (transR h1 h3), },
  { intro h5,
    apply h4,
    apply (antisimR h3),
    rw ←h5,
    exact h1, },
end
 
-- 2ª demostración
-- ===============
 
local infix ≤ := R
local infix < := R'
 
example : transitive (<) :=
assume a b c,
assume h₁ : a < b,
assume h₂ : b < c,
have a ≤ b, from and.left h₁,
have a ≠ b, from and.right h₁,
have b ≤ c, from and.left h₂,
have b ≠ c, from and.right h₂,
have a ≤ c, from transR ‹a ≤ b› ‹b ≤ c›,
have a ≠ c, from
    assume : a = c,
    have c ≤ b, from eq.subst ‹a = c› ‹a ≤ b›,
    have b = c, from antisimR ‹b ≤ c› ‹c ≤ b›,
    show false, from ‹b ≠ c› ‹b = c›,
show a < c, from and.intro ‹a ≤ c› ‹a ≠ c›
 
end
Seguir leyendo →

ForMatUS: Pruebas en Lean de que las partes estrictas son irreflexivas

José A. Alonso--

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 2 pruebas en Lean de que las partes estrictas son irreflexivas usando los estilos aplicativos y declarativos.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

-- ----------------------------------------------------
-- Ej. 1. La parte estricta de una relación R es la
-- relación R' definida por
--    R' a b := R a b ∧ a ≠ b
--
-- Demostrar que la parte estricta de cualquier
-- relación es irreflexiva.
-- ----------------------------------------------------
 
import tactic
 
section
 
parameter {A : Type}
parameter (R : A → A → Prop)
 
definition R' (a b : A) : Prop :=
  R a b ∧ a ≠ b
 
#reduce irreflexive R
 
-- 1ª demostración
example :
  irreflexive R' :=
begin
  intros a h,
  cases h with h1 h2,
  apply h2,
  refl,
end
 
-- 2ª demostración
example :
  irreflexive R' :=
assume a,
assume : R' a a,
have a ≠ a, from and.right this,
have a = a, from rfl,
show false, from ‹a ≠ a› ‹a = a›
 
end
Seguir leyendo →

ForMatUS: Pruebas en Lean de que las relaciones irreflexivas y transitivas son asimétricas

José A. Alonso--

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 4 pruebas en Lean de que las relaciones irreflexivas y transitivas son asimétricas usando los estilos declarativos, aplicativos, funcional y automático.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

-- ----------------------------------------------------
-- Ej. 1. Demostrar que las relaciones irreflexivas y
-- transitivas son asimétricas.
-- ----------------------------------------------------
 
variable A : Type
variable R : A → A → Prop
 
-- #reduce irreflexive R
-- #reduce transitive R
 
-- 1ª demostración
example
  (h1 : irreflexive R)
  (h2 : transitive R)
  : ∀ x y, R x y → ¬ R y x :=
begin
  intros x y h3 h4,
  apply h1 x,
  apply h2 h3 h4,
end
 
-- 2ª demostración
example
  (h1 : irreflexive R)
  (h2 : transitive R)
  : ∀ x y, R x y → ¬ R y x :=
begin
  intros x y h3 h4,
  apply (h1 x) (h2 h3 h4),
end
 
-- 3ª demostración
example
  (h1 : irreflexive R)
  (h2 : transitive R)
  : ∀ x y, R x y → ¬ R y x :=
λ x y h3 h4, (h1 x) (h2 h3 h4)
 
-- 4ª demostración
example
  (h1 : irreflexive R)
  (h2 : transitive R)
  : ∀ x y, R x y → ¬ R y x :=
assume x y,
assume h3 : R x y,
assume h4 : R y x,
have h5 : R x x, from h2 h3 h4,
have h6 : ¬ R x x, from h1 x,
show false, from h6 h5
Seguir leyendo →

ForMatUS: Pruebas en Lean de 𝒫 A ⊆ 𝒫 B ↔ A ⊆ B

José A. Alonso--

He añadido a la lista Lógica con Lean el vídeo en el que se comentan pruebas de la monotonía del conjunto potencia:

𝒫 A ⊆ 𝒫 B ↔ A ⊆ B

usando los estilos declarativos, aplicativos, funcional y automático.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import data.set
open set
 
variable  {U : Type}
variables {A B C : set U}
 
-- #reduce 𝒫 A
-- #reduce B ∈ 𝒫 A
 
-- ----------------------------------------------------
-- Ej. 1. Demostrar
--    𝒫 A ⊆ 𝒫 B → A ⊆ B
-- ----------------------------------------------------
 
-- 1ª demostración
example : 𝒫 A ⊆ 𝒫 B → A ⊆ B :=
begin
  intro h,
  apply subset_of_mem_powerset,
  apply h,
  apply mem_powerset,
  exact subset.rfl,
end
 
-- 2ª demostración
example : 𝒫 A ⊆ 𝒫 B → A ⊆ B :=
begin
  intro h,
  apply h,
  exact subset.rfl,
end
 
-- 3ª demostración
example : 𝒫 A ⊆ 𝒫 B → A ⊆ B :=
begin
  intro h,
  exact (h subset.rfl),
end
 
-- 4ª demostración
example : 𝒫 A ⊆ 𝒫 B → A ⊆ B :=
λ h, h subset.rfl
 
-- 5ª demostración
example : 𝒫 A ⊆ 𝒫 B → A ⊆ B :=
assume h1 : 𝒫 A ⊆ 𝒫 B,
have h2 : A ⊆ A, from subset.rfl,
have h3 : A ∈ 𝒫 A, from h2,
have h4 : A ∈ 𝒫 B, from h1 h3,
show A ⊆ B, from h4
 
-- 6ª demostración
example : 𝒫 A ⊆ 𝒫 B → A ⊆ B :=
assume h1 : 𝒫 A ⊆ 𝒫 B,
have h2 : A ⊆ A, from subset.rfl,
have h3 : A ∈ 𝒫 A, from h2,
h1 h3
 
-- 7ª demostración
example : 𝒫 A ⊆ 𝒫 B → A ⊆ B :=
assume h1 : 𝒫 A ⊆ 𝒫 B,
have h2 : A ⊆ A, from subset.rfl,
h1 h2
 
-- 8ª demostración
example : 𝒫 A ⊆ 𝒫 B → A ⊆ B :=
assume h1 : 𝒫 A ⊆ 𝒫 B,
h1 subset.rfl
 
-- 9ª demostración
lemma aux1 : 𝒫 A ⊆ 𝒫 B → A ⊆ B :=
λ h, h subset.rfl
 
-- 10ª demostración
example : 𝒫 A ⊆ 𝒫 B → A ⊆ B :=
powerset_mono.mp
 
-- ----------------------------------------------------
-- Ej. 2. Demostrar
--    A ⊆ B → 𝒫 A ⊆ 𝒫 B
-- ----------------------------------------------------
 
-- 1ª demostración
example : A ⊆ B → 𝒫 A ⊆ 𝒫 B :=
begin
  intro h,
  intros C hCA,
  apply mem_powerset,
  apply subset.trans hCA h,
end
 
-- 2ª demostración
example : A ⊆ B → 𝒫 A ⊆ 𝒫 B :=
begin
  intros h C hCA,
  apply subset.trans hCA h,
end
 
-- 3ª demostración
lemma aux2 : A ⊆ B → 𝒫 A ⊆ 𝒫 B :=
λ h C hCA, subset.trans hCA h
 
-- 4ª demostración
example : A ⊆ B → 𝒫 A ⊆ 𝒫 B :=
powerset_mono.mpr
 
-- ----------------------------------------------------
-- Ej. 3. Demostrar
--    𝒫 A ⊆ 𝒫 B ↔ A ⊆ B
-- ----------------------------------------------------
 
-- 1ª demostración
example : 𝒫 A ⊆ 𝒫 B ↔ A ⊆ B :=
iff.intro aux1 aux2
 
-- 2ª demostración
example : 𝒫 A ⊆ 𝒫 B ↔ A ⊆ B :=
-- by library_search
powerset_mono
 
-- 3ª demostración
example : 𝒫 A ⊆ 𝒫 B ↔ A ⊆ B :=
-- by hint
by finish
 
-- 4ª demostración
example : 𝒫 A ⊆ 𝒫 B ↔ A ⊆ B :=
by simp
Seguir leyendo →

ForMatUS: Pruebas en Lean de (⋃i, ⋂j, A i j) ⊆ (⋂j, ⋃i, A i j)

José A. Alonso--

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 2 pruebas en Lean de la propiedad

(⋃i, ⋂j, A i j) ⊆ (⋂j, ⋃i, A i j)

usando los estilos declarativos, aplicativos, funcional y automático.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

-- ----------------------------------------------------
-- Ej. 1. Demostrar
--    (⋃i, ⋂j, A i j) ⊆ (⋂j, ⋃i, A i j)
-- ----------------------------------------------------
 
import data.set
 
open set
 
variables {I J U : Type}
variables (A : I → J → set U)
 
-- 1ª demostración
example : (⋃i, ⋂j, A i j) ⊆ (⋂j, ⋃i, A i j) :=
begin
  intros x h,
  rw mem_Union at h,
  cases h with i hi,
  rw mem_Inter at hi,
  apply mem_Inter.mpr,
  intro j,
  apply mem_Union.mpr,
  use i,
  exact (hi j),
end
 
-- 2ª demostración
example : (⋃i, ⋂j, A i j) ⊆ (⋂j, ⋃i, A i j) :=
begin
  intros x h,
  simp * at *,
  cases h with i hi,
  intro j,
  use i,
  exact (hi j),
end
Seguir leyendo →

ForMatUS: Pruebas en Lean de la intersección sobre unión general: C ∩ (⋃i, A i) = (⋃ i, C ∩ A i)

José A. Alonso--

He añadido a la lista Lógica con Lean el vídeo en el que se comentan pruebas en Lean de la propiedad

C ∩ (⋃i, A i) = (⋃ i, C ∩ A i)

usando los estilos declarativos, aplicativos, funcional y automático.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import data.set
 
open set
 
variables {I U : Type}
variables {A : I → set U}
variable  {C : set U}
 
-- ----------------------------------------------------
-- Ej. 1. Demostrar
--    C ∩ (⋃i, A i) ⊆ (⋃ i, C ∩ A i)
-- ----------------------------------------------------
 
-- 1ª demostración
example :
  C ∩ (⋃i, A i) ⊆ (⋃ i, C ∩ A i)  :=
begin
  rintros x ⟨hC, hU⟩,
  rw mem_Union at hU,
  cases hU with i hA,
  apply mem_Union.mpr,
  use i,
  split,
  assumption',
end
 
-- 2ª demostración
example :
  C ∩ (⋃i, A i) ⊆ (⋃ i, C ∩ A i)  :=
begin
  intros x h,
  simp * at *,
end
 
-- 3ª demostración
lemma inter_Uni_l1 :
  C ∩ (⋃i, A i) ⊆ (⋃ i, C ∩ A i)  :=
by {intros x h, simp * at *}
 
-- ----------------------------------------------------
-- Ej. 2. Demostrar
--    (⋃ i, C ∩ A i) ⊆ C ∩ (⋃i, A i)
-- ----------------------------------------------------
 
-- 1ª demostración
example :
  (⋃ i, C ∩ A i) ⊆ C ∩ (⋃i, A i) :=
begin
  intros x h,
  rw mem_Union at h,
  cases h with i hi,
  cases hi with hC hA,
  split,
  { exact hC, },
  { apply mem_Union.mpr,
    use i,
    exact hA, },
end
 
-- 2ª demostración
example : (⋃ i, C ∩ A i) ⊆ C ∩ (⋃i, A i) :=
begin
  intros x h,
  rw mem_Union at h,
  rcases h with ⟨i, hC, hA⟩,
  split,
  { exact hC, },
  { apply mem_Union.mpr,
    use i,
    exact hA, },
end
 
-- 3ª demostración
example :
  (⋃ i, C ∩ A i) ⊆ C ∩ (⋃i, A i) :=
begin
  intros x h,
  simp * at *,
end
 
-- 4ª demostración
lemma inter_Uni_l2 :
  (⋃ i, C ∩ A i) ⊆ C ∩ (⋃i, A i) :=
by {intros x h, simp * at *}
 
-- ----------------------------------------------------
-- Ej. 3. Demostrar
--    C ∩ (⋃i, A i) = (⋃ i, C ∩ A i)
-- ----------------------------------------------------
 
-- 1ª demostración
example :
  C ∩ (⋃i, A i) = (⋃ i, C ∩ A i) :=
eq_of_subset_of_subset inter_Uni_l1 inter_Uni_l2
 
-- 2ª demostración
example :
  C ∩ (⋃i, A i) = (⋃ i, C ∩ A i) :=
-- by library_search
inter_Union C A
 
-- 3ª demostración
example :
  C ∩ (⋃i, A i) = (⋃ i, C ∩ A i) :=
ext $ by simp
 
-- 4ª demostración
example :
  C ∩ (⋃i, A i) = (⋃ i, C ∩ A i) :=
by {ext, simp}
Seguir leyendo →

ForMatUS: Pruebas en Lean de la distributiva de la intersección general sobre la intersección

José A. Alonso--

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 4 pruebas en Lean de la propiedad distributiva de la intersección general sobre la intersección :

(⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i)

usando los estilos declarativos, aplicativos, funcional y automático.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

-- ----------------------------------------------------
-- Ej. 1. Demostrar
--    (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i)
-- ----------------------------------------------------
 
import data.set
import tactic
 
open set
 
variables {I U : Type}
variables {A B : I → set U}
 
-- 1ª demostración
example :
  (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i) :=
begin
  ext,
  split,
  { intro h,
    rw mem_Inter at h,
    split,
    { rw mem_Inter,
      intro i,
      exact (h i).left, },
    { rw mem_Inter,
      intro i,
      exact (h i).right, }},
  { rintro ⟨h1, h2⟩,
    rw mem_Inter at *,
    intro i,
    exact ⟨h1 i, h2 i⟩, },
end
 
-- 2ª demostración
example :
  (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i) :=
ext $
assume x : U,
iff.intro
( assume h : x ∈ ⋂ i, A i ∩ B i,
  have h1 : ∀ i, x ∈ A i ∩ B i,
    from mem_Inter.mp h,
  have h2 : ∀ i, x ∈ A i,
    from assume i, and.left (h1 i),
  have h3 : ∀ i, x ∈ B i,
    from assume i, and.right (h1 i),
  have h4 : x ∈ ⋂ i, A i,
    from mem_Inter.mpr h2,
  have h5 : x ∈ ⋂ i, B i,
    from mem_Inter.mpr h3,
  show x ∈ (⋂ i, A i) ∩ (⋂ i, B i),
    from and.intro h4 h5)
( assume h : x ∈ (⋂ i, A i) ∩ (⋂ i, B i),
  have h1 : ∀ i, x ∈ A i,
    from mem_Inter.mp (and.left h),
  have h2 : ∀ i, x ∈ B i,
    from mem_Inter.mp (and.right h),
  have h3 : ∀ i, x ∈ A i ∩ B i,
    from assume i, and.intro (h1 i) (h2 i),
  show x ∈ ⋂ i, A i ∩ B i,
    from mem_Inter.mpr h3)
 
-- 3ª demostración
example :
  (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i) :=
-- by library_search
Inter_inter_distrib A B
 
-- 4ª demostración
example :
  (⋂ i, A i ∩ B i) = (⋂ i, A i) ∩ (⋂ i, B i) :=
ext (by finish)
Seguir leyendo →

ForMatUS: Pertenencia a uniones e intersecciones de familias en Lean

José A. Alonso--

He añadido a la lista Lógica con Lean el vídeo en el que se comentan pruebas en Lean de la caracterización de la pertenencia a uniones o intersecciones de familias de conjuntos.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

import data.set
 
open set
 
variables {I U : Type}
variables {A : I → set U}
variable  {x : U}
 
-- ----------------------------------------------------
-- Ej. 1. Demostrar que
--    (x ∈ ⋃ i, A i) ↔ (∃ i, x ∈ A i)
-- ----------------------------------------------------
 
-- 1ª demostración
example :
  (x ∈ ⋃ i, A i) ↔ (∃ i, x ∈ A i) :=
-- by library_search
mem_Union
 
-- 2ª demostración
example :
  (x ∈ ⋃ i, A i) ↔ (∃ i, x ∈ A i) :=
by simp
 
-- ----------------------------------------------------
-- Ej. 2. Demostrar que
--    (x ∈ ⋂ i, A i) ↔ (∀ i, x ∈ A i)
-- ----------------------------------------------------
 
-- 1ª demostración
example :
  (x ∈ ⋂ i, A i) ↔ (∀ i, x ∈ A i) :=
-- by library_search
mem_Inter
 
-- 2ª demostración
example :
  (x ∈ ⋂ i, A i) ↔ (∀ i, x ∈ A i) :=
by simp
Seguir leyendo →