1 noviembre 2020 – Vestigium

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

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

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