José A. Alonso – Página 37 – Vestigium

ForMatUS: Pruebas en Lean de que la identidad es biyectiva

PorJosé A. Alonso 3 noviembre 202022 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 la identidad es biyectiva 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 tactic

open function

variables {X : Type}

-- #print injective
-- #print surjective
-- #print bijective

-- ----------------------------------------------------
-- Ej. 1. Demostrar que la identidad es inyectiva.
-- ----------------------------------------------------

-- 1ª demostración
example : injective (@id X) :=
begin
  intros x₁ x₂ h,
  exact h,
end

-- 2ª demostración
example : injective (@id X) :=
λ x₁ x₂ h, h

-- 3ª demostración
example : injective (@id X) :=
λ x₁ x₂, id

-- 4ª demostración
example : injective (@id X) :=
assume x₁ x₂,
assume h : id x₁ = id x₂,
show x₁ = x₂, from h

-- 5ª demostración
example : injective (@id X) :=
--by library_search
injective_id

-- 6ª demostración
example : injective (@id X) :=
-- by hint
by tauto

-- 7ª demostración
example : injective (@id X) :=
-- by hint
by finish

-- ----------------------------------------------------
-- Ej. 2. Demostrar que la identidad es suprayectiva.
-- ----------------------------------------------------

-- 1ª demostración
example : surjective (@id X) :=
begin
  intro x,
  use x,
  exact rfl,
end

-- 2ª demostración
example : surjective (@id X) :=
begin
  intro x,
  exact ⟨x, rfl⟩,
end

-- 3ª demostración
example : surjective (@id X) :=
λ x, ⟨x, rfl⟩

-- 4ª demostración
example : surjective (@id X) :=
assume y,
show ∃ x, id x = y, from exists.intro y rfl

-- 5ª demostración
example : surjective (@id X) :=
-- by library_search
surjective_id

-- 6ª demostración
example : surjective (@id X) :=
-- by hint
by tauto

-- ----------------------------------------------------
-- Ej. 3. Demostrar que la identidad es biyectiva.
-- ----------------------------------------------------

-- 1ª demostración
example : bijective (@id X) :=
and.intro injective_id surjective_id

-- 2ª demostración
example : bijective (@id X) :=
⟨injective_id, surjective_id⟩

-- 3ª demostración
example : bijective (@id X) :=
-- by library_search
bijective_id

1

2

3

4

5

6

7

8

9

10

11

12

13

14

15

16

17

18

19

20

21

22

23

24

25

26

27

28

29

30

31

32

33

34

35

36

37

38

39

40

41

42

43

44

45

46

47

48

49

50

51

52

53

54

55

56

57

58

59

60

61

62

63

64

65

66

67

68

69

70

71

72

73

74

75

76

77

78

79

80

81

82

83

84

85

86

87

88

89

90

91

92

93

94

95

96

97

98

99

100

101

102

103

104

import tactic

open function

variables {X : Type}

-- #print injective

-- #print surjective

-- #print bijective

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

-- Ej. 1. Demostrar que la identidad es inyectiva.

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

-- 1ª demostración

example : injective (@id X) :=

begin

intros x₁ x₂ h,

exact h,

end

-- 2ª demostración

example : injective (@id X) :=

λ x₁ x₂ h, h

-- 3ª demostración

example : injective (@id X) :=

λ x₁ x₂, id

-- 4ª demostración

example : injective (@id X) :=

assume x₁ x₂,

assume h : id x₁ = id x₂,

show x₁ = x₂, from h

-- 5ª demostración

example : injective (@id X) :=

--by library_search

injective_id

-- 6ª demostración

example : injective (@id X) :=

-- by hint

by tauto

-- 7ª demostración

example : injective (@id X) :=

-- by hint

by finish

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

-- Ej. 2. Demostrar que la identidad es suprayectiva.

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

-- 1ª demostración

example : surjective (@id X) :=

begin

intro x,

use x,

exact rfl,

end

-- 2ª demostración

example : surjective (@id X) :=

begin

intro x,

exact ⟨x, rfl⟩,

end

-- 3ª demostración

example : surjective (@id X) :=

λ x, ⟨x, rfl⟩

-- 4ª demostración

example : surjective (@id X) :=

assume y,

show ∃ x, id x = y, from exists.intro y rfl

-- 5ª demostración

example : surjective (@id X) :=

-- by library_search

surjective_id

-- 6ª demostración

example : surjective (@id X) :=

-- by hint

by tauto

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

-- Ej. 3. Demostrar que la identidad es biyectiva.

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

-- 1ª demostración

example : bijective (@id X) :=

and.intro injective_id surjective_id

-- 2ª demostración

example : bijective (@id X) :=

⟨injective_id, surjective_id⟩

-- 3ª demostración

example : bijective (@id X) :=

-- by library_search

bijective_id

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

1

2

3

4

5

6

7

8

9

10

11

12

13

14

15

16

17

18

19

20

21

22

23

24

25

26

27

28

29

30

31

32

33

34

35

36

37

38

39

40

41

42

43

44

45

46

47

48

49

50

51

52

53

54

55

56

57

58

59

60

61

62

63

64

65

66

67

68

69

70

71

72

73

74

75

76

77

78

79

80

81

82

83

84

85

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

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

1

2

3

4

5

6

7

8

9

10

11

12

13

14

15

16

17

18

19

20

21

22

23

24

25

26

27

28

29

30

31

32

33

34

35

36

37

38

39

40

41

42

43

44

45

46

47

48

49

50

51

52

53

54

55

56

57

58

59

60

61

62

63

64

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

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

Resumen de lecturas compartidas durante octubre de 2020

PorJosé A. Alonso 1 noviembre 202030 agosto 2021

Esta entrada es una recopilación de lecturas compartidas, durante octubre de 2020, en Twitter fundamentalmente sobre programación funcional y demostración asistida por ordenador.

Las lecturas están ordenadas según su fecha de publicación en Twitter.

Al final de cada artículo se encuentran etiquetas relativas a los sistemas que usa o a su contenido.

Una recopilación de todas las lecturas compartidas se encuentra en GitHub.
Read More “Resumen de lecturas compartidas durante octubre de 2020”

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

1

2

3

4

5

6

7

8

9

10

11

12

13

14

15

16

17

18

19

20

21

22

23

24

25

26

27

28

29

30

31

32

33

34

35

36

37

38

39

40

41

42

43

44

45

46

47

48

49

50

51

52

53

54

55

56

57

58

59

60

61

62

63

64

65

66

67

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

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