Taller de Lean 4

Curs 23/24

Autors/es

Enric Cosme

Mario Vago

Publicat

2023

Lean és un llenguatge de programació funcional que pot ser utilitzat com demostrador de teoremes interactiu. Podeu consultar els manuals Lean Manual i Theorem Proving in Lean 4 o visitar la Comunitat de Lean. Podeu trobar este curs i altres en la pàgina de cursos de la Comunitat de Lean.

Si has treballat amb la versió anterior de Lean tal vegada t’interesse llegir Lean 4 survival guide for Lean 3 users. Podeu vore una xicoteta presentació de les característiques principals de Lean impartida pel seu creador, Leonardo de Moura. Si voleu provar Lean sense fer cap instal·lació, podeu anar a la seua versió web.

Sessions

El treball de les sessions està a la vostra disposició en un repositori de Github.

  • Primeres definicions i sintaxi
  • Proposicions
  • Quantificadors
  • Igualtats i aplicacions
  • Subtipus i tipus quocients
  • Tipus producte i suma
  • Tipus inductius
  • Operadors clausura
  • L’ordre habitual dels naturals
  • Estructures i classes

Instal·lació

Comencem instal·lant Visual Studio Code. Aquest programa tindrà dues utilitats, la d’editor de text i la de compilador del llenguatge. Podeu seguir els passos indicats a continuació des del manual Quickstart.

  1. Instal·lem l’editor VSCode.
  2. (Usuaris de Windows) Instal·lem Git Bash.
  3. Obrim VSCode i instal·lem l’extensió lean4.
  4. Creem un nou fitxer (File/New Text File) i seleccionem el llenguatge Lean4.
  5. Apareixerà un error. Seleccionem Instal·lar Lean utilitzant Elan.
  6. En finalitzar apareixeran dues finestres. La de l’esquerra és un editor i la de la dreta és el compilador. Per a vore que tot funcione correctament escrivim en la de l’esquerra #eval Lean.versionString. Si tot funciona bé, en situar el cursor a la dreta del text que acabem d’escriure, en la finestra de la dreta apareixerà “4.0.0”. Açò vol dir que l’instal·lació ha acabat.

Creació d’un nou projecte

Per a començar a treballar necessitem crear un projecte que incorpore les llibreries necessàries. Podeu seguir els passos indicats a continuació des del manual Lean projects.

  1. Obrim el Terminal de VSCode i escrivim
lake +leanprover/lean4:nightly-2023-02-04 new Lean4 math

Açò crea una carpeta anomenada Lean4 amb un nou projecte vinculat a la llibreria mathlib4.

  1. En VSCode obrim la carpeta Lean4 i tornem al terminal per a escriure
lake update
lake exe cache get

Obrim el fitxer Lean4.lean i escrivim #eval hello i comprovem que retorna “world”.

  1. Dins de la carpeta Lean4 creem una carpeta i dins d’aquesta un fitxer amb l’extensió .lean. Obrim aquest fitxer i comencem a treballar.

Inicialització del repositori TallerLean4

  1. Podeu clonar aquest repositori dins de la carpeta de la vostra elecció
git clone https://github.com/encosllo/TallerLean4
  1. A continuació, dins de la carpeta TallerLean4, procediu a actualitzar el repositori
lake exe cache get
  1. Recordeu obrir la carpeta TallerLean4 al Visual Studio Code.

Paperproof

Paperproof és una interfície per a la presentació de les demostracions. Podeu trobar tota la informació en la pàgina web del projecte.

  1. Instal·lem l’extensió de vscode Paperproof.
  2. En l’arxiu lakefile.lean escrivim
require Paperproof from git 
  "https://github.com/Paper-Proof/paperproof.git"@"main"/"lean"
  1. En la terminal escrivim
lake update Paperproof
  1. Si volem utilitzar Paperproof, en l’encapçalament de l’arxiu de treball escrivim import Paperproof.