Lean_Prover – Página 6

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

PorJosé A. Alonso 31 octubre 202021 diciembre 2020

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 &lt; := R'

example : transitive (&lt;) :=
assume a b c,
assume h₁ : a &lt; b,
assume h₂ : b &lt; 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 &lt; c, from and.intro ‹a ≤ c› ‹a ≠ c›

end

-- ----------------------------------------------------

-- 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

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

PorJosé A. Alonso 31 octubre 202021 diciembre 2020

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

-- ----------------------------------------------------

-- 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

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

PorJosé A. Alonso 31 octubre 202021 diciembre 2020

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

-- ----------------------------------------------------

-- 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

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

PorJosé A. Alonso 30 octubre 202021 diciembre 2020

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

1	𝒫 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

100

101

102

103

104

105

106

107

108

109

110

111

112

113

114

115

116

117

118

119

120

121

122

123

124

125

126

127

128

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

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

PorJosé A. Alonso 30 octubre 202021 diciembre 2020

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)

1	(⋃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

-- ----------------------------------------------------

-- 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