+1 (315) 557-6473 

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


Instructions

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

Requirements and Specifications

  • Reading
Read Chapters 2, 3, and 4 of Verified Functional Programming in Agda, available for free (on campus or VPN) here:
  • Installing Agda
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: http://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.
  • Installing the IAL
You clone the repo here from github:
  • Configuring and testing Agda and the IAL [10 points]
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.)
Screenshots of output
Program to create theorems using AGDA to prove 7 lemmas in Haskell
Program to create theorems using AGDA to prove 7 lemmas in Haskell 1
Program to create theorems using AGDA to prove 7 lemmas in Haskell 2
Source Code
Bools.agda
module bools where
open import lib
{---------------------------------------------------------------------
 these problems are about the nand operator, also known as the Scheffer stroke
 See bool.agda in the IAL for the definition
 ---------------------------------------------------------------------}
nand-not : ∀ (b : 𝔹) → ~ b ≡ b nand b
nand-not ff = refl
nand-not tt = refl
nand-or : ∀ (b1 b2 : 𝔹) → b1 || b2 ≡ (b1 nand b1) nand (b2 nand b2)
nand-or ff ff = refl
nand-or ff tt = refl
nand-or tt ff = refl
nand-or tt tt = refl
nand-and : ∀ (b1 b2 : 𝔹) → b1 && b2 ≡ (b1 nand b2) nand (b1 nand b2)
nand-and ff ff = refl
nand-and ff tt = refl
nand-and tt ff = refl
nand-and tt tt = refl
nand-imp : ∀ (b1 b2 : 𝔹) → b1 imp b2 ≡ b1 nand (b2 nand b2)
nand-imp ff ff = refl
nand-imp ff tt = refl
nand-imp tt ff = refl
nand-imp tt tt = refl
ite-not : ∀(A : Set)(x : 𝔹)(y : A)(z : A) → if x then y else z ≡ if ~ x then z else y
ite-not A ff y z = refl
ite-not A tt y z = refl
&&-distrib : ∀ x y z → x && (y || z) ≡ (x && y) || (x && z)
&&-distrib ff y z = refl
&&-distrib tt y z = refl
combK : ∀ x y → x imp (y imp x) ≡ tt
combK ff y = refl
combK tt ff = refl
combK tt tt = refl
Equational.agda
module equational where
open import lib
postulate
  A : Set
  a : A
  b : A
  c : A
  d : A
  f : A → A
  g : A → A
  h : A → A → A
  p : a ≡ b
  q : b ≡ c
  r : f a ≡ a
  s : h a a ≡ a
  t : ∀ x → f (g x) ≡ g (f x)
  u : ∀ {x} → f x ≡ x → g (g x) ≡ x -- {x} means x is implicit, so you do not need to write it when you call u
  v : ∀ x → h x d ≡ x
L0 : c ≡ c
L0 = refl
L1 : c ≡ a
L1 = trans (sym q) (sym p)
L2 : h (f a) (f (f a)) ≡ a
L2 = trans (cong2 h r (trans (cong f r) r)) s
L3 : f b ≡ b
L3 = trans (sym (cong f p)) (trans r p)
L4 : h (h d d) d ≡ d
L4 = trans (v (h d d)) (v d)
L5 : f (g (g a)) ≡ a
L5 = trans (cong f (u{a} r)) r
L6 : f (g (f (g a))) ≡ g (g (f (f a)))
L6 = trans (cong f (trans (cong g (t a)) (u (cong f r)))) (sym (u (cong f (cong f r))))
L7 : ∀ x → f (f (f x)) ≡ x → f (f (f (f (f x)))) ≡ x → f x ≡ x
L7 x f3 f5 = trans (sym (cong f f5)) (trans (cong f (cong f (cong f f3))) f3)