Write Theorems Using AGDA To Prove 7 Lemmas Haskell Assignment Solutions.

Write a program using AGDA to prove 7 lemmas in Haskell.

Read Chapters 2, 3, and 4 of Verified Functional Programming in Agda, available for free (on campus or VPN) here:

Agda is installed on the CS Windows computers. To remote in, see https://clas.uiowa.edu/linux/services/vmwareview But you will probably find it worth the effort to install Agda on your own computer. For Windows, the easiest thing is to use our installer:

https://homepage.divms.uiowa.edu/~astump/agda/Agda2.6.0.1.v1.msi Otherwise, try following the directions on the Agda wiki, here: https://wiki.portal.chalmers.se/agda/pmwiki.php Essentially you first do cabal install Agda and then agda-mode setup (the latter probably requires that you add ~/.cabal/bin to your path).

22. Open up bool.agda in the IAL. You should see (Agda) at the bottom, but probably will get some error message from emacs. This is because emacs cannot find the "agda" program. We can tell emacs where that program is as follows. Type "Alt-x" and then "customize-group"(no quotes). Hit enter. Then type "agda2" (again no quotes) and hit enter. You will see a list of options. Near the bottom is one for "Agda Program Name". You want to change this one. You click on the little triangle, and you should see a text box that will say "agda". You want to change that to the full path for the agda program on your computer. You figure out what that path is by opening a terminal and typing "which agda" (no quotes), then enter. Copy that path to the little text box (replacing "agda"). Then click the button right under that line that says "State" and select "Save for future sessions". Close emacs and open it up again. If everything goes well, now typing Control-c Control-l in bool.agda should work with syntax highlighting.

You clone the repo here from github:

https://github.com/cedille/ial

Finally, you need to tell Agda how to find the Iowa Agda Library. If you are using a CS Windows machine, then open the file h:/.emacs. Otherwise, open ~/.emacs in emacs (you type \Control-x Control-f /.emacs"). Add the following text, where instead of the word PATH, you should have the path to your copy of the IAL (wherever you put it):

(custom-set-variables '(agda2-program-args (quote ("--include-path=PATH"))))

That should be a single forward tick mark on the second line of that code (might render incorrectly in this PDF). On Windows, I found I could put backslashes if I escaped them (double backslash), like this (where Myself is, of course, your actual Windows username):

C:\\Users\\Myself\\Documents\\ial To prove that all this is working for you, open bool.agda in the IAL and type Control-c Control-l to load the file with Agda. If this succeeds you should get syntax highlighting for the file. Now take a screenshot called ial-screenshot.png, capturing your Emacs window with bool.agda highlighted. (I found that for some reason, Agda often says \Another command is currently in progress" when I do this, and I must first type Control-c Control-x Control-r to restart Agda, andthen do Control-c Control-l.)