search

antalsz / hs-to-coq

Convert Haskell source code to Coq source code
https://hs-to-coq.readthedocs.io
MIT License
279 stars 27 forks source link

Use `Equations` instead of `Program Fixpoint` for termination #138

Open joscoh opened 5 years ago

joscoh commented 5 years ago

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.

womeier commented 4 years ago

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

(I am working with Peter Trommler.)

sweirich commented 4 years ago

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 commented 4 years ago

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.

womeier commented 4 years ago

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