Timeline for Does anyone actually publish "structured proofs"?
Current License: CC BY-SA 3.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 13, 2015 at 7:01 | comment | added | David Ketcheson | Thanks! This is interesting, though I don't believe these are examples of exactly what I asked for. | |
| Sep 12, 2015 at 14:58 | comment | added | darij grinberg | And there I was like "why the hell doesn't my LaTeX work?". This question really should be on mathoverflow. | |
| Sep 12, 2015 at 14:48 | comment | added | darij grinberg | ... ssreflect people, conversely, seem to define maps between finite sets as tuples with certain properties, just because tuples know how to be equal!), and (3) that the infrastructure is still very much in flux and proofs might break with the next update of Coq or ssreflect. But this is absolutely a thing that will work one day. | |
| Sep 12, 2015 at 14:47 | comment | added | darij grinberg | Modern Coq proofs written in ssreflect (e.g., github.com/hivert/Coq-Combi ) are actually not that long! The problems, as far as I can discern them from (unfortunately) somewhat afar are (1) that the Coq format does not easily support human readability (it is very hard to follow a Coq proof on pen and paper), (2) that lack of function extensionality and (lack of) good support for setoids make a lot of mathematical constructions forbiddingly hard to deal with (forget about encoding a tuple of elements of $A$ as a map $\left\{1,2,\ldots,n\right\} \to A$; the ... | |
| Sep 12, 2015 at 13:51 | history | answered | jakebeal | CC BY-SA 3.0 |