[ 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)


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?


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.


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.


>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.


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

I'll try that, thanks.


I'm trying to follow

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?


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.


Read Coq'Art.


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').