The Coq mailing list

[Nuno Gaspar <nmpgaspar AT gmail.com>]

Well, Its in French, but the following is fantastic and probably more related to what you are asking for (since you mentioned a video..)

http://fuscia.inrialpes.fr/cours/coq/

hope it helps (despite being in French :-))

2014-01-24 Thomas Knight <tom1vuu2011 AT gmail.com>

Hi everyone,

I looked at various parts of the documentation available for Coq, and I have a suggestion that would really help me.

Andrej Bauer has a video showing how to do induction with natural numbers and binary trees ( http://www.youtube.com/watch?v=fbt0TcLzrNg ).

What would be really helpful is a set of 100 examples of that kind of utility all available online.

In the video he mentions some particularly useful tactics for that specific application, and that kind of practical advice would allow me to use Coq properly as a proof tool.

I hope you can do this.


Thanks


Tom

--
Bart: Look at me, I'm a grad student, I'm 30 years old and I made $600 dollars last year.
Marge: Bart! Don't make fun of grad students, they just made a terrible life choice.