Timeline for Coq: defining more than two mutually recursive functions on inductive type
Current License: CC BY-SA 3.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 13, 2017 at 12:48 | history | edited | URL Rewriter Bot |
replaced http://cs.stackexchange.com/ with https://cs.stackexchange.com/
|
|
| Sep 7, 2016 at 18:34 | answer | added | ejgallego | timeline score: 2 | |
| Sep 7, 2016 at 13:54 | comment | added | Khan |
@Vinz The function round is called from within rounds where the sub-term of e (which is h) is passed (renaming e in round makes no difference). When it is called from within roundinc, as you pointed it out, y is not decreasing. Actually, the real function is using a complex predicate stronglysee on y and e, which include that y is a sub-event of e. The problem now, in addition, is: even if we include that predicate in roundinc, Coq does not understand automatically, that y is indeed a sub-term of e.
|
|
| Sep 7, 2016 at 11:46 | comment | added | Vinz |
Also, in roundinc, the call to round y is not decreasing, it should be something like round l where e = node l
|
|
| Sep 7, 2016 at 11:31 | comment | added | Vinz |
Btw, there is an issue with your round function: it doesn't call parentround on a sub-term of e, but directly on e. I don't think this is allowed.
|
|
| Sep 7, 2016 at 7:05 | answer | added | Vinz | timeline score: 1 | |
| Sep 7, 2016 at 6:24 | history | asked | Khan | CC BY-SA 3.0 |