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

Generate Rewrite Tactics for Unfolding Definitions #140

Closed euisuny closed 4 years ago

euisuny commented 4 years ago

Haskell function definitions that use where blocks to define local helper functions and recursive functions are compiled to Coq that unfolds in a cumbersome way.

It would be nice to mechanically introduce rewrite lemmas that unfolds definitions "as expected" and add them to the Rewrite hint database.

lastland commented 4 years ago

This sounds useful to have. Another use case for this is with type classes: currently, we have to manually do several unfolds or use computations to get the actual definition of certain type class methods. Automatically generated rewrites would help this as well.

As for local definitions introduced by where, how do you think they should be compiled? One option I can think of is making the local definitions global, but we will need to be careful with their names so that they won't collide with other top-level function definitions. Is that what you have in mind?

euisuny commented 4 years ago

Actually, it turns out (conveniently) that this can be solved by a judicial use of the fold tactic, no need to burden the rewrite database!