The Coq mailing list

[Thomas Knight <tom1vuu2011 AT gmail.com>]

Hi Daniil

Yes, I had started reading that book, but something more like what is offered by Kevin seems like the right balance between theory and practice for me.

Thanks

Tom

On Mon, Jan 27, 2014 at 8:08 PM, Daniil Frumin <difrumin AT gmail.com> wrote:

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