Lean_Prover – Página 5

ForMatUS: Pruebas en Lean de que las relaciones reflexivas y euclídeas son de equivalencia

PorJosé A. Alonso 2 noviembre 202021 diciembre 2020

He añadido a la lista Lógica con Lean el vídeo en el que se comentan pruebas en Lean de que si una relación es reflexiva y euclídea, entonces es de equivalencia. Se usan los estilos declarativos, aplicativos y funcional.

A continuación, se muestra el vídeo

y el código de la teoría utilizada

-- ----------------------------------------------------
-- Una relación binaria (≈) es euclídea si
--    ∀ {a b c}, a ≈ b → c ≈ b → a ≈ c
--
-- El objetivo de esta teoría es demostrar que si una
-- relación es reflexiva y euclídea, entonces es de
-- equivalencia.
-- ----------------------------------------------------

import tactic

section

parameter {A : Type}
parameter (R : A → A → Prop)

local infix ≈ := R

parameter reflexivaR : reflexive (≈)
parameter euclideaR : ∀ {a b c}, a ≈ b → c ≈ b → a ≈ c

include reflexivaR euclideaR

-- ----------------------------------------------------
-- Ej. 1. Demostrar que las relaciones reflexivas y
-- y euclídeas son simétricas.
-- ----------------------------------------------------

-- 1ª demostración
example : symmetric (≈) :=
begin
  intros a b h,
  exact euclideaR (reflexivaR b) h,
end

-- 2ª demostración
example : symmetric (≈) :=
λ a b h, euclideaR (reflexivaR b) h

-- 3ª demostración
lemma simetricaR : symmetric (≈) :=
assume a b (h1 : a ≈ b),
have h2 : b ≈ b, from (reflexivaR b),
show b ≈ a, from euclideaR h2 h1

-- ----------------------------------------------------
-- Ej. 2. Demostrar que las relaciones reflexivas y
-- y euclídeas son transitivas.
-- ----------------------------------------------------

-- 1ª demostración
example : transitive (≈) :=
begin
  rintros a b c h1 h2,
  apply euclideaR h1,
  exact euclideaR (reflexivaR c) h2,
end

-- 2ª demostración
lemma transitivaR : transitive (≈) :=
λ a b c h1 h2, (euclideaR h1) (euclideaR (reflexivaR c) h2)

-- 3ª demostración
example : transitive (≈) :=
assume a b c (h1 : a ≈ b) (h2 : b ≈ c),
have h3 : c ≈ b, from euclideaR (reflexivaR c) h2,
show a ≈ c, from euclideaR h1 h3

-- ----------------------------------------------------
-- Ej. 3. Demostrar que las relaciones reflexivas y
-- y euclídeas son de equivalencia.
-- ----------------------------------------------------

-- 1ª demostración
example : equivalence (≈) :=
begin
  unfold equivalence,
  exact ⟨reflexivaR, simetricaR, transitivaR⟩,
end

-- 2ª demostración
example : equivalence (≈) :=
⟨reflexivaR, simetricaR, transitivaR⟩

end

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

-- Una relación binaria (≈) es euclídea si

-- ∀ {a b c}, a ≈ b → c ≈ b → a ≈ c

-- El objetivo de esta teoría es demostrar que si una

-- relación es reflexiva y euclídea, entonces es de

-- equivalencia.

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

import tactic

section

parameter {A : Type}

parameter (R : A → A → Prop)

local infix ≈ := R

parameter reflexivaR : reflexive (≈)

parameter euclideaR : ∀ {a b c}, a ≈ b → c ≈ b → a ≈ c

include reflexivaR euclideaR

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

-- Ej. 1. Demostrar que las relaciones reflexivas y

-- y euclídeas son simétricas.

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

-- 1ª demostración

example : symmetric (≈) :=

begin

intros a b h,

exact euclideaR (reflexivaR b) h,

end

-- 2ª demostración

example : symmetric (≈) :=

λ a b h, euclideaR (reflexivaR b) h

-- 3ª demostración

lemma simetricaR : symmetric (≈) :=

assume a b (h1 : a ≈ b),

have h2 : b ≈ b, from (reflexivaR b),

show b ≈ a, from euclideaR h2 h1

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

-- Ej. 2. Demostrar que las relaciones reflexivas y

-- y euclídeas son transitivas.

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

-- 1ª demostración

example : transitive (≈) :=

begin

rintros a b c h1 h2,

apply euclideaR h1,

exact euclideaR (reflexivaR c) h2,

end

-- 2ª demostración

lemma transitivaR : transitive (≈) :=

λ a b c h1 h2, (euclideaR h1) (euclideaR (reflexivaR c) h2)

-- 3ª demostración

example : transitive (≈) :=

assume a b c (h1 : a ≈ b) (h2 : b ≈ c),

have h3 : c ≈ b, from euclideaR (reflexivaR c) h2,

show a ≈ c, from euclideaR h1 h3

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

-- Ej. 3. Demostrar que las relaciones reflexivas y

-- y euclídeas son de equivalencia.

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

-- 1ª demostración

example : equivalence (≈) :=

begin

unfold equivalence,

exact ⟨reflexivaR, simetricaR, transitivaR⟩,

end

-- 2ª demostración

example : equivalence (≈) :=

⟨reflexivaR, simetricaR, transitivaR⟩

end

ForMatUS: Pruebas en Lean de que las equivalencias son los preórdenes simétricos

PorJosé A. Alonso 2 noviembre 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 equivalencias son los preórdenes simétricos, 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. Un preorden es una relación reflexiva y
-- transitiva.
--
-- Demostrar que las relaciones de equivalencias son
-- los prórdenes simétricos.
-- ----------------------------------------------------

import tactic

variable {A : Type}
variable R : A → A → Prop

def preorden (R : A → A → Prop) : Prop :=
  reflexive R ∧ transitive R

-- #print equivalence
-- #print symmetric

-- 1ª demostración
example :
  equivalence R ↔ preorden R ∧ symmetric R :=
begin
  split,
  { rintros ⟨h1, h2, h3⟩,
    exact ⟨⟨h1, h3⟩, h2⟩, },
  { rintros ⟨⟨h1, h3⟩, h2⟩,
    exact ⟨h1, h2, h3⟩, },
end

-- 2ª demostración
example :
  equivalence R ↔ preorden R ∧ symmetric R :=
⟨λ ⟨h1, h2, h3⟩, ⟨⟨h1, h3⟩, h2⟩,
 λ ⟨⟨h1, h3⟩, h2⟩, ⟨h1, h2, h3⟩⟩

-- 3ª demostración
example :
  equivalence R ↔ preorden R ∧ symmetric R :=
iff.intro
  ( assume h1 : equivalence R,
    have h2 : reflexive R, from and.left h1,
    have h3 : symmetric R, from and.left (and.right h1),
    have h4 : transitive R, from and.right (and.right h1),
    show preorden R ∧ symmetric R,
      from and.intro (and.intro h2 h4) h3)
  ( assume h1 : preorden R ∧ symmetric R,
    have h2 : preorden R, from and.left h1,
    show equivalence R,
      from and.intro (and.left h2)
             (and.intro (and.right h1) (and.right h2)))

-- 4ª demostración
example :
  equivalence R ↔ preorden R ∧ symmetric R :=
begin
  unfold equivalence preorden,
  tauto,
end

-- 5ª demostración
example :
  equivalence R ↔ preorden R ∧ symmetric R :=
by finish [preorden]

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

-- Ej. 1. Un preorden es una relación reflexiva y

-- transitiva.

-- Demostrar que las relaciones de equivalencias son

-- los prórdenes simétricos.

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

import tactic

variable {A : Type}

variable R : A → A → Prop

def preorden (R : A → A → Prop) : Prop :=

reflexive R ∧ transitive R

-- #print equivalence

-- #print symmetric

-- 1ª demostración

example :

equivalence R ↔ preorden R ∧ symmetric R :=

begin

split,

{ rintros ⟨h1, h2, h3⟩,

exact ⟨⟨h1, h3⟩, h2⟩, },

{ rintros ⟨⟨h1, h3⟩, h2⟩,

exact ⟨h1, h2, h3⟩, },

end

-- 2ª demostración

example :

equivalence R ↔ preorden R ∧ symmetric R :=

⟨λ ⟨h1, h2, h3⟩, ⟨⟨h1, h3⟩, h2⟩,

λ ⟨⟨h1, h3⟩, h2⟩, ⟨h1, h2, h3⟩⟩

-- 3ª demostración

example :

equivalence R ↔ preorden R ∧ symmetric R :=

iff.intro

( assume h1 : equivalence R,

have h2 : reflexive R, from and.left h1,

have h3 : symmetric R, from and.left (and.right h1),

have h4 : transitive R, from and.right (and.right h1),

show preorden R ∧ symmetric R,

from and.intro (and.intro h2 h4) h3)

( assume h1 : preorden R ∧ symmetric R,

have h2 : preorden R, from and.left h1,

show equivalence R,

from and.intro (and.left h2)

(and.intro (and.right h1) (and.right h2)))

-- 4ª demostración

example :

equivalence R ↔ preorden R ∧ symmetric R :=

begin

unfold equivalence preorden,

tauto,

end

-- 5ª demostración

example :

equivalence R ↔ preorden R ∧ symmetric R :=

by finish [preorden]

ForMatUS: Pruebas en Lean de una desigualdad entre números naturales

PorJosé A. Alonso 1 noviembre 202021 diciembre 2020

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 8 pruebas en Lean de una desigualdad entre números naturales, 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 si n y m son números naturales
-- tales que n + 1 ≤ m, entonces n &lt; m + 1.
-- ----------------------------------------------------

import tactic

variables n m : ℕ

-- 1ª demostración
example
  (h : n + 1 ≤ m)
  : n &lt; m + 1 :=
calc
  n   &lt; n + 1 : lt_add_one n
  ... ≤ m     : h
  ... &lt; m + 1 : lt_add_one m

-- 2ª demostración
example
  (h : n + 1 ≤ m)
  : n &lt; m + 1 :=
have h1 : n &lt; n + 1, from lt_add_one n,
have h2 : n &lt; m,     from lt_of_lt_of_le h1 h,
have h3 : m &lt; m + 1, from lt_add_one m,
show n &lt; m + 1,      from lt.trans h2 h3

-- 3ª demostración
example
  (h : n + 1 ≤ m)
  : n &lt; m + 1 :=
begin
  apply lt_trans (lt_add_one n),
  apply lt_of_le_of_lt h (lt_add_one m),
end

-- 4ª demostración
example
  (h : n + 1 ≤ m)
  : n &lt; m + 1 :=
lt_trans (lt_add_one n) (lt_of_le_of_lt h (lt_add_one m))

-- 5ª demostración
example
  (h : n + 1 ≤ m)
  : n &lt; m + 1 :=
-- by suggest
nat.lt.step h

-- 6ª demostración
example
  (h : n + 1 ≤ m)
  : n &lt; m + 1 :=
-- by hint
by omega

-- 7ª demostración
example
  (h : n + 1 ≤ m)
  : n &lt; m + 1 :=
by linarith

-- 8ª demostración
example
  (h : n + 1 ≤ m)
  : n &lt; m + 1 :=
by nlinarith

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

-- Ej. 1. Demostrar que si n y m son números naturales

-- tales que n + 1 ≤ m, entonces n < m + 1.

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

import tactic

variables n m : ℕ

-- 1ª demostración

example

(h : n + 1 ≤ m)

: n < m + 1 :=

calc

n < n + 1 : lt_add_one n

... ≤ m : h

... < m + 1 : lt_add_one m

-- 2ª demostración

example

(h : n + 1 ≤ m)

: n < m + 1 :=

have h1 : n < n + 1, from lt_add_one n,

have h2 : n < m, from lt_of_lt_of_le h1 h,

have h3 : m < m + 1, from lt_add_one m,

show n < m + 1, from lt.trans h2 h3

-- 3ª demostración

example

(h : n + 1 ≤ m)

: n < m + 1 :=

begin

apply lt_trans (lt_add_one n),

apply lt_of_le_of_lt h (lt_add_one m),

end

-- 4ª demostración

example

(h : n + 1 ≤ m)

: n < m + 1 :=

lt_trans (lt_add_one n) (lt_of_le_of_lt h (lt_add_one m))

-- 5ª demostración

example

(h : n + 1 ≤ m)

: n < m + 1 :=

-- by suggest

nat.lt.step h

-- 6ª demostración

example

(h : n + 1 ≤ m)

: n < m + 1 :=

-- by hint

by omega

-- 7ª demostración

example

(h : n + 1 ≤ m)

: n < m + 1 :=

by linarith

-- 8ª demostración

example

(h : n + 1 ≤ m)

: n < m + 1 :=

by nlinarith

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