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

[ Return /
Go to bottom ]

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?

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.

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.

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

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

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

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'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?

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?

Read Coq'Art.

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

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

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