The Coq mailing list

[Daniil Frumin <difrumin AT gmail.com>]

I recommend you to check out the Software Foundations book [1] in
particular the chapters Lists, Induction, Logic.

[1] http://www.cis.upenn.edu/~bcpierce/sf

On Sat, Jan 25, 2014 at 1:35 AM, Thomas Knight 
<tom1vuu2011 AT gmail.com>
 wrote:
> 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



-- 
Sincerely yours,
-- Daniil