Matija Pretnar: Taktike v Coqu

Opozorilo: tudi tokrat bo seminar za diskretno matematiko gostoval pri seminarju za osnove. Zato se dobimo že ob 10h v Plemljevem seminarju.

Povzetek: V dokazovalnem pomočniki Coq lahko marsikateri dokaz skrajšamo z uporabo taktik. Te Coqu povedo korake, s katerimi naj poskuša dokazati cilj. Na seminarju bom predstavil osnovne gradnike taktik, pa tudi zapletenejše taktike, ki analizirajo obliko cilja in hipotez ter so lahko tudi rekurzivne. Kot primer bom pokazal dokaze v formalizaciji abstraktne Stoneove dualnosti. Ko smo jih nazadnje poskušali pisati na seminarju, nam ni uspelo napisati niti enega, s primernimi taktikami pa se skrčijo na par vrstic in postanejo zelo enostavni.

Vabljeni!