31 octubre 2020 – Vestigium

ForMatUS: Pruebas en Lean de que las partes simétricas son simé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 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

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

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

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

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

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

-- 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), },

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

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