Documentazione di lungo

Il tuo primo pacchetto Go costruito da Lean

Scrivi definizioni Lean e una dimostrazione, genera da esse un pacchetto Go con lungo e chiamalo da un programma Go.

In questa sezione

In questo tutorial scriveremo alcune definizioni Lean sui rettangoli, dimostreremo un fatto che le riguarda, ne genereremo un pacchetto Go e lo chiameremo da un programma Go. Lo stesso progetto Lean è usato dai tutorial per Python, Swift, TypeScript e C.

Prima di iniziare

Servono:

  • Go 1.22 o successivo con cgo, e un compilatore C (su Windows, GCC di MinGW-w64)
  • elan, il gestore delle toolchain di Lean
  • il comando lungo
elan toolchain install leanprover/lean4:v4.34.1
brew install machinefabric/tap/lungo   # apt, dnf, Windows, cargo: vedi il riferimento del comando lungo

Scrivi il progetto Lean

Crea un modulo Go con un progetto Lake in lean/:

mkdir shapes && cd shapes
go mod init example.com/shapes
mkdir lean
echo 'leanprover/lean4:v4.34.1' > lean/lean-toolchain

lean/lakefile.toml dichiara una libreria il cui modulo radice Lake compila per impostazione predefinita:

name = "geometry"
version = "0.1.0"
defaultTargets = ["Geometry"]

[[lean_lib]]
name = "Geometry"

lean/Geometry.lean contiene le definizioni e la dimostrazione:

namespace Geometry

structure Rect where
  width : Nat
  height : Nat
deriving Repr

def area (r : Rect) : Nat := r.width * r.height

def scale (k : Nat) (r : Rect) : Rect :=
  { width := k * r.width, height := k * r.height }

/-- Scaling by `k` multiplies the area by `k * k`. -/
theorem area_scale (k : Nat) (r : Rect) : area (scale k r) = k * k * area r := by
  simp only [area, scale]
  exact Nat.mul_mul_mul_comm k r.width k r.height

/-- The rectangle with the largest area, if any. -/
def largest (rs : List Rect) : Option Rect :=
  rs.foldl (fun best r => match best with
    | some b => if area r > area b then some r else some b
    | none => some r) none

end Geometry

Crea una volta il manifest di Lake (fa parte del progetto):

(cd lean && lake update)

Genera il pacchetto

lungo.toml indica il progetto Lake e dove va il pacchetto Go:

project = "lean"

[go]
out = "geometry"

lungo generate

La prima esecuzione compila il progetto Lean, e quindi controlla la dimostrazione: cambia k * k in k nel teorema e lungo generate fallisce con l’errore di Lean. Stampa generated go into geometry. La directory contiene geometry.go e i file C del programma; aggiungi .lungo/ (lo spazio di lavoro di lungo) a .gitignore. Scarica il modulo di supporto importato dal pacchetto:

go mod tidy

Chiamalo da Go

main.go:

package main

import (
	"fmt"
	"log"
	"math/big"

	"example.com/shapes/geometry"
)

func main() {
	r := geometry.Rect{Width: big.NewInt(3), Height: big.NewInt(4)}
	area, err := geometry.Area(r)
	if err != nil {
		log.Fatal(err)
	}
	fmt.Println("area:", area)

	bigger, err := geometry.Scale(big.NewInt(10), r)
	if err != nil {
		log.Fatal(err)
	}
	fmt.Println("scaled:", bigger.Width, "x", bigger.Height)

	best, err := geometry.Largest([]geometry.Rect{r, bigger})
	if err != nil {
		log.Fatal(err)
	}
	if best.Valid {
		fmt.Println("largest:", best.Value.Width, "x", best.Value.Height)
	}
}

$ go run .
area: 12
scaled: 30 x 40
largest: 30 x 40

Nat è diventato *big.Int (non ha limite superiore), la structure una struct Go, Option un lungo.Option, e ogni funzione restituisce un errore oltre al risultato: qui può essere solo un *lungo.MalformedError, per un numero negativo, che il Nat di Lean non può contenere.

Che cosa abbiamo fatto

Abbiamo generato un pacchetto Go da un progetto Lake di cui Lean ha controllato le dimostrazioni, e lo abbiamo chiamato come qualsiasi pacchetto Go; esegue il codice compilato di Lean sul runtime di lungo, che il modulo lungo-go collega nel binario. Prossimi passi: