1
$\begingroup$

I would like to prove in Haskell, whether in vanilla Haskell or using some libraries / tools, some simple theorems such as:

and [n*(n+1)/2 == sum [0..n] | n <- [0..]]

Is there a simple enough (ie. fully automated) way to prove such theorems involving integers in Haskell? I am not really interested in the proof itself, or a counterexample, but merely a yes/no answer.

There's this publication which doesn't seem practically usable; other than that most of everything else seems to be rather complex, ie. involving a completely separate language and not concerning Haskell.

$\endgroup$
2
1
$\begingroup$

Look at Agda [1][2]

I think that it's exactly what you are looking for.

I recommend using its emacs mode for autocompletion and hole/interactive programming. [2]/quick-guide.html

A very good introduction is plfa [3], also [2]/tutorial-list.html

[1] https://en.wikipedia.org/wiki/Agda_(programming_language)

[2] https://agda.readthedocs.io/en/v2.6.0.1/getting-started/what-is-agda.html

[3] https://plfa.github.io/

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.