Documentazione di lungo

Il tuo primo pacchetto Python costruito da Lean

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

In questa sezione

In questo tutorial scriveremo alcune definizioni Lean sui rettangoli, dimostreremo un fatto che le riguarda, ne genereremo un pacchetto Python con lungo e lo useremo. Il progetto Lean è lo stesso dei tutorial per Go, Swift, TypeScript e C.

Prima di iniziare

Servono:

  • Python 3.9 o successivo, CMake e un compilatore C
  • 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 una directory con un progetto Lake in lean/:

mkdir shapes && cd 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 progetto Python:

project = "lean"

[python]
out = "geometry-py"

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. geometry-py è un progetto Python; aggiungi .lungo/ (lo spazio di lavoro di lungo) a .gitignore. Installalo in un ambiente virtuale; porta con sé lungo-py, che contiene il runtime:

python3 -m venv .venv
.venv/bin/pip install ./geometry-py

Chiamalo da Python

shapes.py:

from geometry import Rect, area, largest, scale

r = Rect(width=3, height=4)
print("area:", area(r))
bigger = scale(10, r)
print("scaled:", bigger)
print("largest:", largest([r, bigger]))

$ .venv/bin/python shapes.py
area: 12
scaled: Rect(width=30, height=40)
largest: Rect(width=30, height=40)

La structure è diventata una dataclass immutabile, Nat un int (uno negativo solleva lungo_py.MalformedError) e Option un valore oppure None.

Che cosa abbiamo fatto

Abbiamo generato un pacchetto Python da un progetto Lake di cui Lean ha controllato le dimostrazioni; le sue funzioni eseguono il codice compilato di Lean sul runtime di lungo. Prossimi passi: