[ art / civ / cult / cyb / diy / drg / feels / layer / lit / λ / q / r / sci / sec / tech / w / zzz ] archive provided by lainchan.jp

lainchan archive - /λ/ - 17964



File: 1471212063969.png (650.94 KB, 211x300, 1452715120528.png)

No.17964

I'm trying to learn Coq without much success. I've attempted reading Software Foundations and some tutorials, but I always end up stuck on theorems. The problem is, I have absolutely no idea why am I stuck, what could I do about it, and how did I end up there. To be honest I just throw tactics around without any plan hoping I will solve it by accident.

It seems very alien to programming. How should I go about learning it?

  No.17969

File: 1471222965857.png (3.24 MB, 200x200, The Little Prover.pdf)

This book might help you wrap your head around the concepts. I have not finished it yet but I read some other books of the same series, and found them very helpful and well written.
It uses a proof assistant implemented in Scheme apparently similar to ACL2, but the concepts apply to all proof assistants.
It doesn't require any particular programming knowledge other than recursion and lists.

  No.17971

>>17969
Scratch that: it is implemented in Scheme, Racket and ACL2, and claims to be so simple that you can easily implement it in your language of choice.
http://the-little-prover.github.io

  No.17979

>To be honest I just throw tactics around without any plan hoping I will solve it by accident.
There's your problem. I've ben told that the way you use these theorem provers is that you first do a hand proof, and then you do the machine proof. The hand-proof lets you explore more, without being tied up in the rigour the machine wants.

  No.17980

>>17969
I've already read it but it's very different from the way Coq works.

>>17979
I'll try that, thanks.

  No.18159

I'm trying to follow
https://www.di.ens.fr/~zappa/teaching/coq/ecole10/

It went well until in lecture 7 where they introduced "inductive predicates". Inductive types I understand, but how do these work? Why can I put nearly any statement after the constructor?

There's an exercise to define a relation where the list l' is obtained form l by transposing two consecutive elements. How can I come up with an inductive predicate for something like this?

  No.20049

>>17964
I had to do some Coq work for my Computer Logic course, maybe tomorrow I can post some simple examples and some of the more involved exercises if you're still interested.

  No.20858

Read Coq'Art.

  No.20859

>>18159
In the following code, Trans proves that x :: y :: l and y :: x :: l proves the predicate.
Trsucc is an inductive predicate, it supposes you can prove transpose l l, and then proves that x :: l and x :: l' proves the predicate. It basically like induction in math (or simple recurrence).

Inductive transpose (A : Type) : list A -> list A -> Prop :=
| Trans: forall (x y : A) (l : list A), transpose A (cons x (cons y l)) (cons y (cons x l))
| Trsucc: forall (x : A) (l l' : list A), transpose A l l' -> transpose A (cons x l) (cons x l').