Use Equations instead of Program Fixpoint for termination

[lastland]

Issue by joscoh
Wednesday Nov 20, 2019 at 03:28 GMT
Originally opened as antalsz/hs-to-coq#138

---

Currently, hs-to-coq uses Program Fixpoint to deal with more complex termination arguments. However, this makes it extremely hard to work with the resulting code, since Program Fixpoint creates huge proof terms that are difficult and slow to manipulate (for instance, the file examples/graph/theories/HeapEquiv.v, which has a single rewrite lemma for a Program Fixpoint function, takes over 3 minutes to compile - though my proof might not be great). Using Equations instead (or in addition) would have the following advantages:

1. Equations automatically generates a number of useful rewriting and equivalence lemmas that make working with defined function easy and remove the need to prove separate rewriting lemmas by unfolding massive proof terms.
2. Equations is better at automatically solving obligations. For instance, the toList function in examples/graph/lib/Data/Graph/Inductive/Internal/Heap.v was generated by hs-to-coq with Program Fixpoint and requires several lemmas and tactics to solve the obligations. The equivalent Equations version in examples/graph/theories/HeapProofs.v solves the termination obligations automatically.
3. The syntax of Equations is closer to Haskell, which may make it either easier to translate or more similar to the current Haskell code. At the very least, Stephanie seemed to think that it would not be much harder to translate to this syntax.
4. Program Fixpoint doesn't work with some features, namely an "as" pattern in a pattern match. Antal and I discovered this bug, and the details are in the hs-to-coq channel.

I have found it simpler, for most of the functions in examples/graph, to use deferredFix and write an Equations version that I then proved equivalent instead of using Program Fixpoint. I think it would be beneficial to just be able to use Equations directly.

[lastland]

Comment by womeier
Monday May 25, 2020 at 14:29 GMT

---

I am working on this. Where can I find the hs-to-coq channel?

(I am working with Peter Trommler.)

[lastland]

Comment by sweirich
Tuesday May 26, 2020 at 15:11 GMT

---

Hi Wolfgang! Thanks for joining! The hs-to-coq channel is part of an internal Penn slack server. We're looking into creating a more public space for discussion. In the meantime, feel free to use this issue for questions.

[lastland]

Comment by lastland
Tuesday May 26, 2020 at 21:08 GMT

---

Hi @womeier, we have just created a public hs-to-coq channel. It exists as a stream on Coq's Zulipchat: either use https://coq.zulipchat.com/#narrow/stream/240767-hs-to-coq-devs.20.26.20users or find "hs-to-coq devs & users" stream on Coq's Zulipchat (https://coq.zulipchat.com/). And just in case you don't know it yet, there is also an "Equations devs & users" stream on Coq's Zulipchat which you may find useful.

[lastland]

Comment by womeier
Wednesday Jun 03, 2020 at 06:50 GMT

---

Ok, good to know. Thank you @lastland for the suggestion :)

[lastland]

This branch may address this problem: https://github.com/womeier/hs-to-coq/tree/equations I haven't been able to look more closely at it though...