×
Samples Blogs Make Payment About Us Reviews 4.9/5 Order Now

Write Theorems Using AGDA To Prove 7 Lemmas Haskell Assignment Solutions

July 09, 2024
Nadia Dubois
Nadia Dubois
🇨🇦 Canada
Haskell
Nadia is a seasoned developer with over 6 years of experience in building dynamic web applications using Haskell and WAI frameworks. Having completed over 700 assignments, she thrives on helping students understand real-world use cases of WAI, including form handling, user interaction, and data validation. Nadia also enjoys delving into front-end integration with frameworks like Elm.
Key Topics
  • Instructions
  • Requirements and Specifications
Tip of the day
Use the REPL (Read-Eval-Print Loop) to test your code interactively, and practice writing concise, readable expressions to harness Scala’s powerful syntax effectively.
News
In 2024, JavaScript's Redux saw updates for efficient state management, and Tailwind CSS gained traction for responsive design. Meanwhile, C++ libraries like Boost.

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: 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).

    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:

    https://github.com/cedille/ial

  • 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, and then 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 Haskell1
Program to create theorems using AGDA to prove 7 lemmas in Haskell2

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)

Related Samples

At ProgrammingHomeworkHelp.com, students can explore a variety of Haskell assignment samples. These expertly crafted examples are designed to provide clear insights and practical solutions to common challenges faced in Haskell programming. Our website is dedicated to supporting students in their academic journey, ensuring they have access to high-quality resources that enhance their learning experience. Whether you're tackling functional programming concepts or advanced Haskell techniques, our assignment samples are here to guide you towards academic success.