Timeline for Theorem Proofs in Coq
Current License: CC BY-SA 3.0
16 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 10, 2013 at 2:25 | answer | added | Luke Mathieson | timeline score: 4 | |
| Dec 10, 2013 at 0:44 | vote | accept | user11942 | ||
| Dec 9, 2013 at 21:26 | answer | added | cody | timeline score: 7 | |
| S Dec 9, 2013 at 18:57 | history | suggested | daniel gratzer | CC BY-SA 3.0 |
Indented code
|
| Dec 9, 2013 at 18:33 | review | Suggested edits | |||
| S Dec 9, 2013 at 18:57 | |||||
| Dec 9, 2013 at 15:34 | comment | added | cody | I'll add to @LukeMathieson's comment, and say that almost all your definitions are given, usually in a more usable form, in the Logic and Arith modules: coq.inria.fr/stdlib/index.html It's probably a good idea to have a look at the definitions there to get an idea of how things are done. | |
| Dec 9, 2013 at 9:54 | history | edited | user11942 | CC BY-SA 3.0 |
added 17 characters in body
|
| Dec 9, 2013 at 9:53 | comment | added | user11942 | I have posted the Coq code that I have written so far. | |
| Dec 9, 2013 at 9:40 | history | edited | user11942 | CC BY-SA 3.0 |
I added the Coq code that I have written so far in order to make it easier for others to assist me.
|
| Dec 9, 2013 at 5:03 | comment | added | Luke Mathieson | Another note, Thm P5 (inductive principle) is built in to Coq in a stronger form (structural induction), so you don't need to explicitly take that as an axiom. | |
| Dec 9, 2013 at 2:03 | comment | added | Luke Mathieson | ... is about verifying programs etc., the start is quite a good introduction to Coq, and has theorems like the ones you've got as exercises and examples. It's free, and it's actually all written as Coq scripts, so you can do the exercises and compile them as you're reading through. For what you're doing here, there's interesting bits and pieces in the chapters Basics, Induction, Prop and Logic - and probably some dependencies from the bits inbetween. | |
| Dec 9, 2013 at 2:00 | comment | added | Luke Mathieson | A couple of comments and clarifying questions:- Would it be sufficient for your purposes to just use syntactic equality ("=" in Coq) instead of I(N,x,y)? Is there a reason for using 'or' the way you've defined it? Coq (well, the basic libraries for Coq) have a way of expression logical disjunction that facilitates certain nice aspects of proofs. Similarly there's a way to define 'less' that may be more workable for you. To this end you might want to have a look at the early chapters of Software Foundations. While the end of the book... | |
| Dec 9, 2013 at 1:44 | history | tweeted | twitter.com/#!/StackCompSci/status/409861043981418496 | ||
| Dec 9, 2013 at 0:13 | review | First posts | |||
| Dec 10, 2013 at 3:37 | |||||
| Dec 9, 2013 at 0:09 | comment | added | Gilles 'SO- stop being evil' | To understand how far you've got, it would help if you'd post your Coq code so far, so that we could load it and check that what we propose works for your definitions. | |
| Dec 8, 2013 at 23:54 | history | asked | user11942 | CC BY-SA 3.0 |