Fix termination check

[nikivazou]

Check here: https://github.com/plum-umd/lmonad-meta/blob/dev.jp/src/src/Simulations/Programs.hs#L213

[nikivazou]

Here things get more complicated... Note that the size of the expression to be evaluation will not always decrease (e.g., when you have application, the size of the expression might get bigger)

[nikivazou]

@jprider63, I fixed/proved your function and removed the Index things. Check this: https://github.com/plum-umd/lmonad-meta/blob/niki.dev/src/src/Simulations/Programs.hs#L19

The idea is that the mutual recursive functions terminate, because there is this evalSteps quantity that is decreasing (basically the Index in the Coq proof).

But here, the evalSteps does not exists at all, it is just axiomatized (here:https://github.com/plum-umd/lmonad-meta/blob/niki.dev/src/src/Termination.hs) so that if a program terminates, then evalSteps properly decreases. Again, terminates and evalSteps do not exist at Haskell level and are only axiomatized.

What do you think? I prefer this, rather than currying around indexes.

I left for you to prove two theorems:

• https://github.com/plum-umd/lmonad-meta/blob/niki.dev/src/src/Simulations/Helpers.hs#L16 "If a program is ς, its evaluation is also ς"

• and this: https://github.com/plum-umd/lmonad-meta/blob/niki.dev/src/src/Simulations/Helpers.hs#L20 which is all I need to prove this case: https://github.com/plum-umd/lmonad-meta/blob/niki.dev/src/src/Simulations/Programs.hs#L39

Other than Simulations.hs which is still running, does not seem that I broke anything else!

[nikivazou]

So, do prove the two theorems above, merge the niki.dev branch, and let me know if you want to meet in person to explain you what I did.