Matematický korespondenční seminář

Čokoládová výzva v leanu

Co je Lean?
Druhý díl našeho seriálu o indukci se zaměřuje na formální dokazování. Psaní důkazů formálně má tu výhodu, že se dají snadno ověřovat počítačem. Stačí je napsat v jazyce, kterému počítač rozumí. Jeden z nich je Lean. Psaní důkazů v Leanu je interaktivní, takže počítač během psaní důkazu říká, čemu už věří a co je ještě třeba dokázat. Pro vyzkoušení Leanu není třeba nic instalovat a dá se vyzkoušet online tady Lean Natural Number Game.

O čem je soutěž?
Cílem soutěže je dokázat druhou seriálovou úlohu v Leanu. Tedy máme následující axiomy

add_zero (a : mynat) :
   a + 0 = a

add_succ (a b : mynat) :
   a + succ(b) = succ(a + b)

mul_zero (a : mynat) :
   a * 0 = 0

mul_succ (a b : mynat) :
   a * succ(b) = a * b + a

pow_zero (a : mynat) :
   a ^ 0 = 1

pow_succ (a b : mynat) :
   a ^ succ(b) = a ^ b * a

A chceme dokázat následující tři tvrzení

lemma pow_add (a m n : mynat) : a ^ (m + n) = a ^ m * a ^ n
lemma pow_pow (a m n : mynat) : (a ^ m) ^ n = a ^ (m * n)
lemma mul_pow (a b n : mynat) : (a * b) ^ n = a ^ n * b ^ n

Jedná se dokonce přímo o levely 5, 7 a 6 v Natural Number Game ve světě Power World. K důkazu můžete používat pomocná lemmata, ale všechna jsou potřeba dokázat.

Co můžu vyhrát?
Jako odměnu za správná řešení budeme rozdávat čokolády. První člověk, který pošle správné řešení, dostane čokoládu, druhý dostane půl čokolády, třetí čtvrt a tak dále :-).

Kam mám řešení posílat?
Svá řešení posílejte na e-mail . @ gmail com redek39.

Do kdy soutěž probíhá?
Soutěž má stejný termín jako druhá seriálová série, tedy probíhá do 7. února.

Můžu tedy svá řešení v Leanu odevzdat i do Submitovátka jako řešení druhé seriálové úlohy?
Ano, ale budeme rádi i za slovní komentář.

Něco mi není jasné, kam se můžu obrátit?
Své dotazy prosím směřujte na e-mail . @ gmail com redek39.