The Coq mailing list

[Thomas Knight <tom1vuu2011 AT gmail.com>]

What I like about this series is it is practical, but also well informed -- one of my favorite styles of documentation.

On Tue, Jan 28, 2014 at 11:48 PM, Kevin Sullivan <sullivan.kevinj AT gmail.com> wrote:

I just posted new material on strings today. Links to the Coq files are at the bottom of the 05 page.  Again, this material is intended as an on-ramp for the newcomer. --Kevin 

On Tue, Jan 28, 2014 at 2:23 PM, Thomas Knight <tom1vuu2011 AT gmail.com> wrote:

Hi Kevin

Wow, that's very very useful. I started reading before finishing your email, and I only realized after reading the lessons and Coq files, and then while reading the text of the 5th lesson post that not all material was available yet!

I will definitely enjoy and gain from reading the rest of the series.

Thanks


Tom

On Mon, Jan 27, 2014 at 10:22 PM, Kevin Sullivan <sullivan.kevinj AT gmail.com> wrote:

For what it's worth, here's a lecture (written) with Coq files linked at the bottom, intended to start students off from essentially nothing. 

https://www.kevinjsullivan.com/lets-start-at-the-very-beginning

The idea is to start from nothing and cover everything needed, assuming nothing. I cover data types, function types, propositions and proofs for the Empty_set, unit, and bool types, including data types and values, function types and values, and a range of propositions and proofs about these things. By the end (including the exercises) the students will have seen proof by induction several times: clear for degenerate cases, but the point is to get them ready for what's to come. Perhaps you'll find the "A B C's of Coq" an easy way to start.

What follows is about as far as we've gotten this term: the first bits of nat. Tomorrow is string. For these two types we'll have proved only that O and EmptyString are zeros. That'll suggest an underlying commonality (specifically monoidality). But to make that idea precise, we'll also need proofs of associativity of plus and append. I want to do that property in the context of a more comprehensive list of properties of nat and string, as I've already done with bool. But that's going to require a substantial excursion through logic (so that we can state more interesting propositions), and polymorphism (essential to logic). So that's where we're going as you can see in the stubbed out lectures going forward. Eventually we'll come back and make precise and very clear the notion of monoids and more generally type classes.

This course is taught to 3rd and 4th year undergraduates.  Comments certainly welcome. No videos yet, I'm afraid.

Kevin

On Mon, Jan 27, 2014 at 3: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