Lean_Prover – Página 9

ForMatUS: Regla de introducción de la unión en Lean

PorJosé A. Alonso 25 octubre 202021 diciembre 2020

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 11 pruebas en Lean de la regla de introducción de la unión 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
--    A ⊆ A ∪ B
-- ----------------------------------------------------

import data.set

variable  U : Type
variables A B : set U
variable  x : U

open set

-- #reduce x ∈ A ∪ B

-- 1ª demostración
example : A ⊆ A ∪ B :=
begin
  intros x h,
  simp,
  left,
  exact h,
end

-- 2ª demostración
example : A ⊆ A ∪ B :=
begin
  intros x h,
  left,
  exact h,
end

-- 3ª demostración
example : A ⊆ A ∪ B :=
assume x,
assume h : x ∈ A,
show x ∈ A ∪ B, from or.inl h

-- 4ª demostración
example : A ⊆ A ∪ B :=
assume x,
assume h : x ∈ A,
or.inl h

-- 5ª demostración
example : A ⊆ A ∪ B :=
assume x,
λ h : x ∈ A, or.inl h

-- 6ª demostración
example : A ⊆ A ∪ B :=
assume x, or.inl

-- 7ª demostración
example : A ⊆ A ∪ B :=
λ x, or.inl

-- 8ª demostración
example : A ⊆ A ∪ B :=
-- by library_search
subset_union_left A B

-- 9ª demostración
example : A ⊆ A ∪ B :=
λ x, mem_union_left B

-- 10ª demostración
example : A ⊆ A ∪ B :=
-- by hint
by finish

-- 11ª demostración
example : A ⊆ A ∪ B :=
by simp

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

-- Ej. 1. Demostrar

-- A ⊆ A ∪ B

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

import data.set

variable U : Type

variables A B : set U

variable x : U

open set

-- #reduce x ∈ A ∪ B

-- 1ª demostración

example : A ⊆ A ∪ B :=

begin

intros x h,

simp,

left,

exact h,

end

-- 2ª demostración

example : A ⊆ A ∪ B :=

begin

intros x h,

left,

exact h,

end

-- 3ª demostración

example : A ⊆ A ∪ B :=

assume x,

assume h : x ∈ A,

show x ∈ A ∪ B, from or.inl h

-- 4ª demostración

example : A ⊆ A ∪ B :=

assume x,

assume h : x ∈ A,

or.inl h

-- 5ª demostración

example : A ⊆ A ∪ B :=

assume x,

λ h : x ∈ A, or.inl h

-- 6ª demostración

example : A ⊆ A ∪ B :=

assume x, or.inl

-- 7ª demostración

example : A ⊆ A ∪ B :=

λ x, or.inl

-- 8ª demostración

example : A ⊆ A ∪ B :=

-- by library_search

subset_union_left A B

-- 9ª demostración

example : A ⊆ A ∪ B :=

λ x, mem_union_left B

-- 10ª demostración

example : A ⊆ A ∪ B :=

-- by hint

by finish

-- 11ª demostración

example : A ⊆ A ∪ B :=

by simp

ForMatUS: Regla de introducción de la intersección en Lean

PorJosé A. Alonso 24 octubre 202021 diciembre 2020

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 7 pruebas en Lean de la regla de introducción de la intersección 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
--    x ∈ A → x ∈ B → x ∈ A ∩ B
-- ----------------------------------------------------

import data.set

variable  U : Type
variables A B : set U
variable  x : U

open set

-- #reduce x ∈ A ∩ B

-- 1ª demostración
example : x ∈ A → x ∈ B → x ∈ A ∩ B :=
begin
  intros h1 h2,
  simp,
  split,
  { exact h1, },
  { exact h2, },
end

-- 2ª demostración
example : x ∈ A → x ∈ B → x ∈ A ∩ B :=
begin
  intros h1 h2,
  split,
  { exact h1, },
  { exact h2, },
end

-- 3ª demostración
example : x ∈ A → x ∈ B → x ∈ A ∩ B :=
assume h1 : x ∈ A,
assume h2 : x ∈ B,
show x ∈ A ∩ B, from and.intro h1 h2

-- 4ª demostración
example : x ∈ A → x ∈ B → x ∈ A ∩ B :=
assume h1 : x ∈ A,
assume h2 : x ∈ B,
show x ∈ A ∩ B, from ⟨h1, h2⟩

-- 5ª demostración
example : x ∈ A → x ∈ B → x ∈ A ∩ B :=
assume h1 : x ∈ A,
assume h2 : x ∈ B,
⟨h1, h2⟩

-- 6ª demostración
example : x ∈ A → x ∈ B → x ∈ A ∩ B :=
λ h1 h2, ⟨h1, h2⟩

-- 7ª demostración
example : x ∈ A → x ∈ B → x ∈ A ∩ B :=
-- by library_search
mem_inter

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

-- Ej. 1. Demostrar

-- x ∈ A → x ∈ B → x ∈ A ∩ B

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

import data.set

variable U : Type

variables A B : set U

variable x : U

open set

-- #reduce x ∈ A ∩ B

-- 1ª demostración

example : x ∈ A → x ∈ B → x ∈ A ∩ B :=

begin

intros h1 h2,

simp,

split,

{ exact h1, },

{ exact h2, },

end

-- 2ª demostración

example : x ∈ A → x ∈ B → x ∈ A ∩ B :=

begin

intros h1 h2,

split,

{ exact h1, },

{ exact h2, },

end

-- 3ª demostración

example : x ∈ A → x ∈ B → x ∈ A ∩ B :=

assume h1 : x ∈ A,

assume h2 : x ∈ B,

show x ∈ A ∩ B, from and.intro h1 h2

-- 4ª demostración

example : x ∈ A → x ∈ B → x ∈ A ∩ B :=

assume h1 : x ∈ A,

assume h2 : x ∈ B,

show x ∈ A ∩ B, from ⟨h1, h2⟩

-- 5ª demostración

example : x ∈ A → x ∈ B → x ∈ A ∩ B :=

assume h1 : x ∈ A,

assume h2 : x ∈ B,

⟨h1, h2⟩

-- 6ª demostración

example : x ∈ A → x ∈ B → x ∈ A ∩ B :=

λ h1 h2, ⟨h1, h2⟩

-- 7ª demostración

example : x ∈ A → x ∈ B → x ∈ A ∩ B :=

-- by library_search

mem_inter

ForMatUS: Pruebas en Lean de la antisimetría de la inclusión de conjuntos

PorJosé A. Alonso 22 octubre 202021 diciembre 2020

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 7 pruebas en Lean de la propiedad antisimétrica de la inclusión de conjuntos 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
--    A ⊆ B, B ⊆ A ⊢ A = B
-- ----------------------------------------------------

import data.set

variable  U : Type
variables A B : set U

open set

-- 1ª demostración
example
  (h1 : A ⊆ B)
  (h2 : B ⊆ A)
  : A = B :=
begin
  ext,
  split,
  { intro h,
    exact h1 h, },
  { intro h,
    exact h2 h, },
end

-- 2ª demostración
example
  (h1 : A ⊆ B)
  (h2 : B ⊆ A)
  : A = B :=
ext
( assume x,
  iff.intro
  ( assume h : x ∈ A,
    show x ∈ B, from h1 h)
  ( assume h : x ∈ B,
    show x ∈ A, from h2 h))

-- 3ª demostración
example
  (h1 : A ⊆ B)
  (h2 : B ⊆ A)
  : A = B :=
ext
(λ x,
 iff.intro
 (λ h, h1 h)
 (λ h, h2 h))

-- 4ª demostración
example
  (h1 : A ⊆ B)
  (h2 : B ⊆ A)
  : A = B :=
eq_of_subset_of_subset
  ( assume x,
    assume h : x ∈ A,
    show x ∈ B, from h1 h)
  ( assume x,
    assume h : x ∈ B,
    show x ∈ A, from h2 h)

-- 5ª demostración
example
  (h1 : A ⊆ B)
  (h2 : B ⊆ A)
  : A = B :=
eq_of_subset_of_subset h1 h2

-- 6ª demostración
example
  (h1 : A ⊆ B)
  (h2 : B ⊆ A)
  : A = B :=
-- by library_search
subset.antisymm h1 h2

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

-- Ej. 1. Demostrar

-- A ⊆ B, B ⊆ A ⊢ A = B

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

import data.set

variable U : Type

variables A B : set U

open set

-- 1ª demostración

example

(h1 : A ⊆ B)

(h2 : B ⊆ A)

: A = B :=

begin

ext,

split,

{ intro h,

exact h1 h, },

{ intro h,

exact h2 h, },

end

-- 2ª demostración

example

(h1 : A ⊆ B)

(h2 : B ⊆ A)

: A = B :=

ext

( assume x,

iff.intro

( assume h : x ∈ A,

show x ∈ B, from h1 h)

( assume h : x ∈ B,

show x ∈ A, from h2 h))

-- 3ª demostración

example

(h1 : A ⊆ B)

(h2 : B ⊆ A)

: A = B :=

ext

(λ x,

iff.intro

(λ h, h1 h)

(λ h, h2 h))

-- 4ª demostración

example

(h1 : A ⊆ B)

(h2 : B ⊆ A)

: A = B :=

eq_of_subset_of_subset

( assume x,

assume h : x ∈ A,

show x ∈ B, from h1 h)

( assume x,

assume h : x ∈ B,

show x ∈ A, from h2 h)

-- 5ª demostración

example

(h1 : A ⊆ B)

(h2 : B ⊆ A)

: A = B :=

eq_of_subset_of_subset h1 h2

-- 6ª demostración

example

(h1 : A ⊆ B)

(h2 : B ⊆ A)

: A = B :=

-- by library_search

subset.antisymm h1 h2

ForMatUS: Pruebas en Lean de la reflexividad de la inclusión de conjuntos

PorJosé A. Alonso 22 octubre 202021 diciembre 2020

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 11 pruebas en Lean de la propiedad reflexiva de de la inclusión de conjuntos 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
--    A ⊆ A
-- ----------------------------------------------------

import data.set
variable  U : Type
variable  x : U
variables A B C : set U

-- #reduce x ∈ A
-- #reduce B ⊆ C

-- 1ª demostración
example : A ⊆ A :=
begin
  intros x h,
  exact h,
end

-- 2ª demostración
example : A ⊆ A :=
assume x,
assume h : x ∈ A,
show x ∈ A, from h

-- 3ª demostración
example : A ⊆ A :=
assume x,
assume h : x ∈ A,
h

-- 4ª demostración
example : A ⊆ A :=
assume x,
λ h : x ∈ A, h

-- 5ª demostración
example : A ⊆ A :=
assume x,
id

-- 6ª demostración
example : A ⊆ A :=
λ x, id

-- 7ª demostración
example : A ⊆ A :=
-- by library_search
set.subset.rfl

open set

-- 8ª demostración
example : A ⊆ A :=
subset.rfl

-- 9ª demostración
example : A ⊆ A :=
-- by hint
by tauto

-- 10ª demostración
example : A ⊆ A :=
by finish

-- 11ª demostración
example : A ⊆ A :=
by refl

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

-- Ej. 1. Demostrar

-- A ⊆ A

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

import data.set

variable U : Type

variable x : U

variables A B C : set U

-- #reduce x ∈ A

-- #reduce B ⊆ C

-- 1ª demostración

example : A ⊆ A :=

begin

intros x h,

exact h,

end

-- 2ª demostración

example : A ⊆ A :=

assume x,

assume h : x ∈ A,

show x ∈ A, from h

-- 3ª demostración

example : A ⊆ A :=

assume x,

assume h : x ∈ A,

-- 4ª demostración

example : A ⊆ A :=

assume x,

λ h : x ∈ A, h

-- 5ª demostración

example : A ⊆ A :=

assume x,

-- 6ª demostración

example : A ⊆ A :=

λ x, id

-- 7ª demostración

example : A ⊆ A :=

-- by library_search

set.subset.rfl

open set

-- 8ª demostración

example : A ⊆ A :=

subset.rfl

-- 9ª demostración

example : A ⊆ A :=

-- by hint

by tauto

-- 10ª demostración

example : A ⊆ A :=

by finish

-- 11ª demostración

example : A ⊆ A :=

by refl

ForMatUS: Pruebas en Lean del desarrollo de un producto de dos sumas

PorJosé A. Alonso 21 octubre 202020 diciembre 2020

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

(a + b) * (c + d) = a * c + b * c + a * d + b * d

1	(a + b) * (c + d) = a * c + b * c + a * d + b * d

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. Sean a, b, c y d números enteros. Demostrar que
--    (a + b) * (c + d) = a * c + b * c + a * d + b * d
-- ------------------------------------------------------

import tactic
import data.int.basic

variables a b c d : ℤ

-- 1ª demostración
example : (a + b) * (c + d) = a * c + b * c + a * d + b * d :=
calc
  (a + b) * (c + d)
      = (a + b) * c + (a + b) * d         : by rw left_distrib
  ... = (a * c + b * c) + (a + b) * d     : by rw right_distrib
  ... = (a * c + b * c) + (a * d + b * d) : by rw right_distrib
  ... = a * c + b * c + a * d + b * d     : by rw ←add_assoc

-- 2ª demostración
example : (a + b) * (c + d) = a * c + b * c + a * d + b * d :=
by rw [left_distrib, right_distrib, right_distrib, ←add_assoc]

-- 3ª demostración
example : (a + b) * (c + d) = a * c + b * c + a * d + b * d :=
begin
  rw left_distrib,
  rw right_distrib,
  rw right_distrib,
  rw ←add_assoc,
end

-- 4ª demostración
example : (a + b) * (c + d) = a * c + b * c + a * d + b * d :=
calc
  (a + b) * (c + d)
      = (a + b) * c + (a + b) * d         : by rw mul_add
  ... = (a * c + b * c) + (a + b) * d     : by rw add_mul
  ... = (a * c + b * c) + (a * d + b * d) : by rw add_mul
  ... = a * c + b * c + a * d + b * d     : by rw ←add_assoc

-- 5ª demostración
example : (a + b) * (c + d) = a * c + b * c + a * d + b * d :=
-- by hint
by linarith

-- 6ª demostración
example : (a + b) * (c + d) = a * c + b * c + a * d + b * d :=
by nlinarith

-- 7ª demostración
example : (a + b) * (c + d) = a * c + b * c + a * d + b * d :=
by ring

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

-- Ej. 1. Sean a, b, c y d números enteros. Demostrar que

-- (a + b) * (c + d) = a * c + b * c + a * d + b * d

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

import tactic

import data.int.basic

variables a b c d : ℤ

-- 1ª demostración

example : (a + b) * (c + d) = a * c + b * c + a * d + b * d :=

calc

(a + b) * (c + d)

= (a + b) * c + (a + b) * d : by rw left_distrib

... = (a * c + b * c) + (a + b) * d : by rw right_distrib

... = (a * c + b * c) + (a * d + b * d) : by rw right_distrib

... = a * c + b * c + a * d + b * d : by rw ←add_assoc

-- 2ª demostración

example : (a + b) * (c + d) = a * c + b * c + a * d + b * d :=

by rw [left_distrib, right_distrib, right_distrib, ←add_assoc]

-- 3ª demostración

example : (a + b) * (c + d) = a * c + b * c + a * d + b * d :=

begin

rw left_distrib,

rw right_distrib,

rw ←add_assoc,

end

-- 4ª demostración

example : (a + b) * (c + d) = a * c + b * c + a * d + b * d :=

calc

(a + b) * (c + d)

= (a + b) * c + (a + b) * d : by rw mul_add

... = (a * c + b * c) + (a + b) * d : by rw add_mul

... = (a * c + b * c) + (a * d + b * d) : by rw add_mul

... = a * c + b * c + a * d + b * d : by rw ←add_assoc

-- 5ª demostración

example : (a + b) * (c + d) = a * c + b * c + a * d + b * d :=

-- by hint

by linarith

-- 6ª demostración

example : (a + b) * (c + d) = a * c + b * c + a * d + b * d :=

by nlinarith

-- 7ª demostración

example : (a + b) * (c + d) = a * c + b * c + a * d + b * d :=

by ring