-- Functional Programming, Spring 2022 -- Module 6: Agda -- Due: Wednesday, March 30 -- -- - To get L1 credit for this module, complete any 7 of exercises 1-11 -- (note that for unfathomable reasons, exercises 7 and 10 do not exist). -- - To get L2 credit, complete all the exercises, including exercise 12. -- -- Remember that you can complete this module using AgdaPad -- (https://agdapad.quasicoherent.io/): -- -- - Create a new Agda session on AgdaPad. -- - From the File menu, select "Visit New File" and create a blank -- file with a name like "Module6.agda". -- - Click on the tiny "clipboard" icon in the bottom right, paste -- the contents of this file into the pink box. -- - Now put the cursor into the editor and hit "Ctrl+Y". The contents -- of the pink box should be pasted into the editor. -- ---------------------------------------------------------------------- -- First, some imports from the standard library. -- -- ACADEMIC INTEGRITY NOTE: If you want to use anything else besides -- what is imported here, please ask me first. In general, I would -- like you to implement anything additional you need, *without* -- looking at the implementations in the standard library. ---------------------------------------------------------------------- open import Data.Nat using ( ℕ -- Natural numbers. Use \bN to enter the symbol ℕ. ; zero ; suc -- Constructors for ℕ. Note because of Agda's -- BUILTIN magic you can also use numerals like 0, -- 19, etc. to write natural numbers. ; _+_ -- Addition of natural numbers. ) open import Data.List using ( List ; [] ; _∷_ -- Polymorphic lists and their two constructors. -- Use \:: to enter the symbol ∷ . ; [_] -- Convenience function for creating a singleton list. -- And some standard list functions. ; map ; length ; _++_ ; foldr ) open import Relation.Binary.PropositionalEquality using ( _≡_ -- The equality relation ≡ (enter this symbol with \==). -- You can use the following properties of equality: ; refl -- reflexivity, i.e. ∀ {x} → x ≡ x ; sym -- symmetry, i.e. ∀ {x y} → x ≡ y → y ≡ x ; trans -- transitivity, i.e. ∀ {x y z} → x ≡ y → y ≡ z → x ≡ z ; cong -- congruence, i.e. for any function/context f, if x ≡ y -- then f x ≡ f y. for example if p : x ≡ y, then cong -- suc p : suc x ≡ suc y. Put another way, if you need -- to prove suc x ≡ suc y, then you can enter 'cong suc' -- in the hole, hit C-c C-r (refine), and now you only -- have to prove x ≡ y. ; cong₂ -- Like congruence, but for 2-argument -- functions/contexts. -- You will certainly need refl and cong on this -- assignment, and you will probably need sym as well. -- When you find yourself directly using trans, -- you may want to instead use the notation for -- structured equational proofs, explained below. ; module ≡-Reasoning ) open ≡-Reasoning {- Defines nice syntax for structured equational proofs, like so: begin a b c ≡⟨ proof that a b c ≡ x y z ⟩ x y z ≡⟨ proof that x y z ≡ q ⟩ q ≡⟨⟩ -- This step is just reflexivity/computation p ∎ Taken all together, this is a proof that a b c ≡ p. In the last step, ≡⟨⟩ means that q ≡ p by reflexivity (i.e. Agda can see that q ≡ p just by doing some computation, unfolding definitions, etc.) So ≡⟨⟩ is just an abbreviation for ≡⟨ refl ⟩. Of course, under the hood this just uses transitivity (trans) to chain all the proofs together into one big proof, but it's often very nice to be able to actually write out the intermediate steps and have them formally checked. If you use trans directly, you only write the proofs (the parts between ⟨ ... ⟩) and have to keep the intermediate steps (a b c, x y z, ...) in your head. Using this equational reasoning syntax is a bit more verbose, but makes proofs using trans much nicer to both read and write. Use \< and \> to enter ⟨ and ⟩ . Use \qed to enter ∎. -} -------------------------------------------------------------------------------- -- Inductive evidence -------------------------------------------------------------------------------- ------------------------------------------------------------ -- Less than or equal to -- EXERCISE 1. Fill in some constructors to represent evidence that -- one number is ≤ another. Hint: -- * zero is less than or equal to any natural number. -- * if m ≤ n, then suc m ≤ suc n. -- Type \<= to produce ≤ data _≤_ : ℕ → ℕ → Set where -- FILL IN HERE -- Recall the definition of the ⊥ type and logical negation. data ⊥ : Set where ¬ : Set → Set ¬ P = P → ⊥ -- EXERCISE 2. Prove that 3 ≤ 7, and 7 is not ≤ 3. threeLeqSeven : 3 ≤ 7 threeLeqSeven = {!!} sevenNotLeqThree : ¬ (7 ≤ 3) sevenNotLeqThree = {!!} ------------------------------------------------------------ -- Properties of relations -- A binary relation on a set A is just a function A → A → Set. That -- is, every pair of elements of A has a corresponding Set which is -- the proposition that those two elements are in the relation to one -- another. Some of the resulting Sets will be inhabited, -- i.e. provable, (when the two elements are in fact related), and -- some will not be provable (when the two elements are not related). -- For example, one relation we have seen is _≡_ . For any x and y of -- some type A, x ≡ y is a Set expressing the proposition that x and y -- are equal. x ≡ y is always a valid Set for any x and y of the -- right type, but it is only *provable* (i.e. inhabited) when x and y -- are in fact equal. Rel : Set → Set₁ Rel A = A → A → Set -- A binary relation is reflexive if every value of type A is related -- to itself, that is, x ~ x is always provable. Reflexive : {A : Set} → Rel A → Set Reflexive {A} _~_ = (x : A) → x ~ x -- EXERCISE 3. Prove that ≤ is reflexive. ≤-refl : Reflexive _≤_ ≤-refl n = {!!} -- EXERCISE 4. Write down a definition of what it means for a relation -- to be transitive. Transitive : {A : Set} → Rel A → Set Transitive = {!!} -- EXERCISE 5. Prove that ≤ is transitive. ≤-trans : Transitive _≤_ ≤-trans = {!!} -- EXERCISE 6. State and prove that ≤ is antisymmetric, that is, -- if x ≤ y and y ≤ x, then x ≡ y. -- FILL IN HERE -------------------------------------------------------------------------------- -- Equational reasoning -------------------------------------------------------------------------------- ------------------------------------------------------------ -- Some preliminary definitions. Of course these are also -- in the standard library, but are included here so you -- can easily see their definitions. ------------------------------------------------------------ id : ∀ {A : Set} → A → A id a = a _∘_ : ∀ {A B C : Set} → (B → C) → (A → B) → A → C (f ∘ g) a = f (g a) -- length : ∀ {A : Set} → List A → ℕ -- length [] = 0 -- length (_ ∷ l) = 1 + length l -- map : ∀ {A B : Set} → (A → B) → List A → List B -- map _ [] = [] -- map f (x ∷ xs) = f x ∷ map f xs -- _++_ : ∀ {A : Set} → List A → List A → List A -- [] ++ l2 = l2 -- (x ∷ l1) ++ l2 = x ∷ (l1 ++ l2) -- foldr : {A B : Set} → (A → B → B) → B → List A → B -- foldr f z [] = z -- foldr f z (x ∷ l) = f x (foldr f z l) ------------------------------------------------------------ -- EXERCISE 8. Prove that map id ≡ id. map-id : ∀ {A : Set} → (as : List A) → map id as ≡ id as map-id = {!!} -- EXERCISE 9. State and prove a theorem relating map and _++_ . map-++ : {!!} map-++ = {!!} ------------------------------------------------------------ data Tree (A : Set) : Set where Empty : Tree A Node : A → Tree A → Tree A → Tree A -- The mirror function reflects a Tree left-to-right. mirror : {A : Set} → Tree A → Tree A mirror Empty = Empty mirror (Node x l r) = Node x (mirror r) (mirror l) -- EXERCISE 11. -- State and prove a theorem that mirror is its own inverse, that is, -- mirroring a tree twice results in the original tree again. -- Hint: you may find it helpful to use cong₂. ------------------------------------------------------------ -- EXERCISE 12 (Level 2). First, define a function to reverse a list. rev : {A : Set} → List A → List A rev = {!!} -- Now prove that reversing a list twice results in the original list -- again. (Hint: you will probably need to prove a lemma or three!) revrev : {A : Set} → (xs : List A) → rev (rev xs) ≡ xs revrev = {!!}