Utasítások
A feladatod, hogy bebizonyítsd egy egyedi listafordító függvény és a beépített List.reverse egyenlőségét.
Mivel ez a feladat más jellegű, a bizonyítást nem a hagyományos futásidejű tesztek, hanem egy check nevű tétel ellenőrzi.
A tesztet sikeresnek tekintheted, ha ez a tétel átmegy a típusellenőrzésen.
Ha helyben vagy a Lean online játszóterén dolgozol, a Lean InfoView azonnali visszajelzést ad arról, hogy egy tétel sikerül-e vagy elbukik, és hogy miért bukik el.
Ez felbecsülhetetlen értékű eszköz: megmutatja a bizonyításodban használt összes helyi értéket és a jelenlegi célodat.
A sorry taktika bármely bizonyítást helyesnek láttat.
Emiatt előfordulhat, hogy a check tétel már akkor is átmegy a típusellenőrzésen, mielőtt valódi bizonyítást írnál.
Amint eltávolítod a sorry-t a bizonyításodból, a Lean InfoView a helyes visszajelzést mutatja.
Tételek bizonyítása Leanben
A tételbizonyítás a Lean szerves része.
Segítségével a programozók bizonyíthatják programjaik tulajdonságait, érvelhetnek a viselkedésükről, és típusszinten kódolhatják a megkötéseket és a specifikációkat.
Ez a fejezet jó bevezetőt kínál a Lean tételbizonyításához.
Ha mélyebbre szeretnél ásni, ez a könyv hivatalos forrásként szerepel a Lean weboldalán.
A Lean számos taktikát kínál, amelyekkel bizonyításokat, vagy azok részeit automatizálhatod.
Érdemes lehet megnézned a nyelvi referenciát.
Használhatjuk a csimp fordítóattribútumot egy olyan tételen, amely két definíció egyenlőségét bizonyítja.
Ez az attribútum arra utasítja a fordítót, hogy az első definíció helyett a másodikat használja:
@[csimp]
theorem custom_reverse_eq_spec_reverse : @Extra.custom_reverse = @List.reverse := by
... -- proof here
-- now any occurrence of `Extra.custom_reverse` may now compile to `List.reverse`.
Ez különösen olyan helyzetekben hasznos, amikor egy implementáció hatékonyabb, de kevésbé világos.
Írhatunk egy egyszerű specifikációt, és elérhetjük, hogy a lefordított kód helyette a hatékonyabb implementációt használja.
A List és Array számos függvénye ezt a mintát követi.
