Machine learning and hammers for Coq

Incidentally, tactictoe for coq