{-# OPTIONS --allow-unsolved-metas #-} {- AGDA IN PADOVA 2024 Exercise sheet 3 ┌─ SHORTCUTS ───────────────────────┐ ┌─ BACKSLASH CHARACTERS ─┐ │ C-c C-l = load file │ │ \bN = ℕ │ │ C-c C-c = case split │ │ \alpha = α │ │ C-c C-SPC = check hole │ │ \to = → │ │ C-c C-, = see context │ │ \cdot = · │ │ C-c C-. = see context and goal │ │ \:: = ∷ │ │ C-c C-d = display type │ │ \== = ≡ │ │ C-c C-v = evaluate expression │ └────────────────────────┘ │ C-z = enable Vi keybindings │ Use M-x describe-char to │ C-x C-+ = increase font size │ lookup input method for └───────────────────────────────────┘ symbol under cursor. You can open this file in an Agdapad session by pressing C-x C-f ("find file") and then entering the path to this file: ~/Padova2024/exercise03.agda. As this file is read-only, you can then save a copy of this file to your personal directory and edit that one: File > Save As... For instance, you can save this file as ~/solutions03.agda. -} -- ───────────────────────────── -- ────[ BASIC DEFINITIONS ]──── -- ───────────────────────────── data Bool : Set where false : Bool true : Bool data ℕ : Set where zero : ℕ succ : ℕ → ℕ data ⊥ : Set where ¬ : Set → Set ¬ X = X → ⊥ ! : Bool → Bool ! false = true ! true = false _+_ : ℕ → ℕ → ℕ zero + b = b succ a + b = succ (a + b) _·_ : ℕ → ℕ → ℕ zero · b = zero succ a · b = b + (a · b) pred : ℕ → ℕ pred zero = zero pred (succ a) = a infix 5 _≡_ data _≡_ {X : Set} : X → X → Set where refl : {a : X} → a ≡ a {-# BUILTIN EQUALITY _≡_ #-} cong : {A B : Set} {x y : A} → (f : A → B) → x ≡ y → f x ≡ f y cong f refl = refl symm : {A : Set} {x y : A} → x ≡ y → y ≡ x symm refl = refl -- ──────────────────────────────────── -- ────[ GENERALITIES ON EQUALITY ]──── -- ──────────────────────────────────── -- EXERCISE: Fill in this hole, thereby proving that equality is transitive. trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z trans p q = {!!} -- EXERCISE: Prove that equal functions have equal values. -- (The converse is a principle known as "function extensionality" which -- can be postulated in Agda but is not assumed by default.) equal→pwequal : {A B : Set} {f g : A → B} {x : A} → f ≡ g → f x ≡ g x equal→pwequal p = {!!} -- EXERCISE: Think about the expression "(⊥ ≡ ℕ)". Is it well-defined? -- What would be its meaning? -- EXERCISE: Fill in this hole. This lemma will be used below -- in the proof that the double of any number is even. transport : {A : Set} {x y : A} → (F : A → Set) → x ≡ y → F x → F y transport F p s = {!!} -- ───────────────────────────────── -- ────[ EQUALITIES OF NUMBERS ]──── -- ───────────────────────────────── -- EXERCISE: Show that the predecessor of the successor of a number is that number again. lemma-pred-succ : (a : ℕ) → pred (succ a) ≡ a lemma-pred-succ a = {!!} -- EXERCISE: Show that the two functions "even?" and "even?'" have the same values. even? : ℕ → Bool even? zero = true even? (succ n) = ! (even? n) even?' : ℕ → Bool even?' zero = true even?' (succ zero) = false even?' (succ (succ n)) = even?' n lemma-even?-even?' : (a : ℕ) → even? a ≡ even?' a lemma-even?-even?' a = {!!} -- EXERCISE: Show that it is not the case that "succ (pred a) ≡ a" for all natural numbers a. lemma-succ-pred : ((a : ℕ) → succ (pred a) ≡ a) → ⊥ lemma-succ-pred f = {!!} -- The following defines a type family "Positive : ℕ → Set" such that "Positive a" is the -- type of witnesses that a is positive: The type "Positive zero" is empty -- and the types "Positive (succ n)" are inhabited for every n. data Positive : ℕ → Set where -- on purpose, we do NOT include this constructor: zero-is-positive : Positive zero succs-are-positive : {n : ℕ} → Positive (succ n) -- EXERCISE: Fill in this hole. lemma-succ-pred' : (a : ℕ) → Positive a → succ (pred a) ≡ a lemma-succ-pred' a p = {!!} -- EXERCISE: Verify the following two auxiliary lemmas, establishing that we -- could have equivalently defined addition also by recursion on the second argument. lemma-+-zero : (a : ℕ) → (a + zero) ≡ a lemma-+-zero a = {!!} lemma-+-succ : (a b : ℕ) → (a + succ b) ≡ succ (a + b) lemma-+-succ a b = {!!} -- EXERCISE: Verify that addition is commutative. lemma-+-commutative : (a b : ℕ) → (a + b) ≡ (b + a) lemma-+-commutative a b = {!!} -- EXERCISE: Verify that addition is associative. lemma-+-associative : (a b c : ℕ) → (a + (b + c)) ≡ ((a + b) + c) lemma-+-associative a b c = {!!} -- EXERCISE: Verify the distributive law. Similar as the implementation/proof -- of lemma-+-commutative, the result will not be easy to read. -- By a technique called "equational reasoning", to be introduced next time, -- we will be able to clean up the proof. lemma-distributive : (a b c : ℕ) → ((a + b) · c) ≡ ((a · c) + (b · c)) lemma-distributive a b c = {!!} -- EXERCISE: Show that the double of any number is even. data Even : ℕ → Set where base-even : Even zero step-even : {n : ℕ} → Even n → Even (succ (succ n)) lemma-double-even : (a : ℕ) → Even (a + a) lemma-double-even a = {!!} -- ─────────────────────────────── -- ────[ EQUALITIES OF LISTS ]──── -- ─────────────────────────────── data List (A : Set) : Set where [] : List A _∷_ : A → List A → List A module _ {A : Set} where -- the "snoc" operation ("backwards cons"), -- i.e. append an element at the end _∷ʳ_ : List A → A → List A [] ∷ʳ y = y ∷ [] (x ∷ xs) ∷ʳ y = x ∷ (xs ∷ʳ y) -- for instance, "reverse (a ∷ b ∷ c ∷ [])" is "c ∷ b ∷ a ∷ []". reverse : List A → List A reverse [] = [] reverse (x ∷ xs) = reverse xs ∷ʳ x -- EXERCISE: Verify the following lemma. lemma-reverse-∷ʳ : (ys : List A) (x : A) → reverse (ys ∷ʳ x) ≡ (x ∷ reverse ys) lemma-reverse-∷ʳ ys x = {!!} lemma-reverse-reverse : (xs : List A) → reverse (reverse xs) ≡ xs lemma-reverse-reverse xs = {!!} -- EXERCISE: State and prove that _++_ on lists is associative. _++_ : List A → List A → List A [] ++ ys = ys (x ∷ xs) ++ ys = x ∷ (xs ++ ys) -- The following relation relates exactly those lists which have the same length -- and whose corresponding entries are equal. data _≈_ : List A → List A → Set where both-empty : [] ≈ [] both-same-cons : {xs ys : List A} {x y : A} → x ≡ y → xs ≈ ys → (x ∷ xs) ≈ (y ∷ ys) -- EXERCISE: Show that equal lists are related by _≈_. ≡→≈ : {xs ys : List A} → xs ≡ ys → xs ≈ ys ≡→≈ p = {!!} -- EXERCISE: Show that related lists are equal. ≈→≡ : {xs ys : List A} → xs ≈ ys → xs ≡ ys ≈→≡ p = {!!} -- EXERCISE: Regarding "Any" and "_∈_" from exercise02.agda, show that -- "Any (x ≡_) xs" implies "x ∈ xs" and conversely. -- ───────────────────────────────── -- ────[ EQUALITIES OF VECTORS ]──── -- ───────────────────────────────── data Vector (A : Set) : ℕ → Set where [] : Vector A zero _∷_ : {n : ℕ} → A → Vector A n → Vector A (succ n) drop : {A : Set} {n : ℕ} (k : ℕ) → Vector A (k + n) → Vector A n drop zero xs = xs drop (succ k') (x ∷ xs') = drop k' xs' take : {A : Set} {n : ℕ} (k : ℕ) → Vector A (k + n) → Vector A k take zero xs = [] take (succ k') (x ∷ xs') = x ∷ take k' xs' _++ᵥ_ : {A : Set} {n m : ℕ} → Vector A n → Vector A m → Vector A (n + m) [] ++ᵥ ys = ys (x ∷ xs') ++ᵥ ys = x ∷ (xs' ++ᵥ ys) -- EXERCISE: Verify the following lemma. lemma-take-drop : {A : Set} {n : ℕ} → (k : ℕ) → (xs : Vector A (k + n)) → (take k xs ++ᵥ drop k xs) ≡ xs lemma-take-drop = {!!} -- EXERCISE: Find out where the difficulty is in stating that _++ᵥ_ on -- vectors is associative.