Timeline for Formalizing "finite or infinite" in Coq
Current License: CC BY-SA 4.0
13 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 27 at 21:42 | vote | accept | Julio Di Egidio | ||
| Jun 26 at 17:37 | answer | added | Julio Di Egidio | timeline score: 1 | |
| Jun 25 at 7:24 | answer | added | Dominique Larchey-Wendling | timeline score: 2 | |
| Jun 25 at 5:46 | vote | accept | Julio Di Egidio | ||
| Jun 27 at 21:42 | |||||
| Jun 24 at 10:59 | answer | added | Li-yao Xia | timeline score: 4 | |
| Jun 23 at 17:41 | comment | added | Naïm Favier |
"Decidable" is how I interpreted your "and/or computable function to determine/state/distinguish between finite and infinite runs". If you use your definition of run then you can only semidecide whether a run is finite.
|
|
| Jun 23 at 17:14 | comment | added | Naïm Favier |
Having $A : \mathrm{Set}$ does not guarantee that $A$ is decidable in the sense that $A \lor \neg A$ is inhabited. Assuming this for all sets $A$ (or more precisely the ones that are h-propositions) is postulating the law of excluded middle. Decidable propositions are classified by Bool.
|
|
| Jun 23 at 17:07 | history | edited | Julio Di Egidio | CC BY-SA 4.0 |
added a link to stdlib plus fixed a typo
|
| Jun 23 at 17:02 | comment | added | Julio Di Egidio |
Thanks very much @NaïmFavier . This indeed works: Definition IsFinRun (r : run) : Set := {p : pos | r = pos_to_run p}. -- OTOH, I had thought about the coproduct, but then I thought, maybe wrongly, that it would be less elegant than structural subtyping as well as less faithful to the informal progression and notions... anyway, as for decidability, I'd have thought working in Set was the critical factor: I am missing the distinction you are making in that sense.
|
|
| Jun 23 at 16:58 | answer | added | Greg Nisbet | timeline score: 2 | |
| Jun 23 at 16:33 | comment | added | Naïm Favier |
Using your definitions, a run is finite if and only if it is in the image of pos_to_run, so you could define it this way (and this is a proposition because pos_to_run is an embedding, so you can represent this with a $\Sigma$-type). If you want a decidable criterion, then you'd need something like a coproduct of (inductive) lists and streams.
|
|
| Jun 23 at 16:31 | history | edited | Andrej Bauer | CC BY-SA 4.0 |
deleted 83 characters in body
|
| Jun 23 at 16:24 | history | asked | Julio Di Egidio | CC BY-SA 4.0 |