01 exercises

This commit is contained in:
Michael Zhang 2024-06-24 12:28:32 -05:00
parent 8bc705c0ab
commit a44df7d34a

View file

@ -40,7 +40,10 @@ the leftmost argument only.
```agda
_&&'_ : Bool → Bool → Bool
a &&' b = {!!}
true &&' true = true
true &&' false = false
false &&' true = false
false &&' false = false
```
One advantage of this definition is that it reads just like a Boolean truth
@ -54,7 +57,10 @@ verbose definition.
```agda
_xor_ : Bool → Bool → Bool
a xor b = {!!}
true xor true = false
true xor false = true
false xor true = true
false xor false = false
```
### Exercise 3 (★)
@ -67,16 +73,18 @@ left hand side and the right hand side compute to the same value.
```agda
_^_ :
n ^ m = {!!}
n ^ zero = 1
n ^ suc m = n * (n ^ m)
^-example : 3 ^ 4 ≡ 81
^-example = {!!} -- refl 81 should fill the hole here
^-example = refl 81 -- refl 81 should fill the hole here
_! :
n ! = {!!}
zero ! = 1
suc n ! = (suc n) * (n !)
!-example : 4 ! ≡ 24
!-example = {!!} -- refl 24 should fill the hole here
!-example = refl 24 -- refl 24 should fill the hole here
```
### Exercise 4 (★)
@ -93,10 +101,13 @@ max (suc n) (suc m) = suc (max n m)
```agda
min :
min = {!!}
min zero zero = zero
min zero (suc y) = zero
min (suc x) zero = zero
min (suc x) (suc y) = 1 + min x y
min-example : min 5 3 ≡ 3
min-example = {!!} -- refl 3 should fill the hole here
min-example = refl 3 -- refl 3 should fill the hole here
```
### Exercise 5 (★)
@ -110,10 +121,11 @@ element of the list `xs` and returns the resulting list.
```agda
map : {X Y : Type} → (X → Y) → List X → List Y
map f xs = {!!}
map {X} {Y} f [] = []
map {X} {Y} f (x :: xs) = f x :: map f xs
map-example : map (_+ 3) (1 :: 2 :: 3 :: []) ≡ 4 :: 5 :: 6 :: []
map-example = {!!} -- refl _ should fill the hole here
map-example = refl _ -- refl _ should fill the hole here
-- We write the underscore, because we don't wish to repeat
-- the relatively long "4 :: 5 :: 6 :: []" and Agda can
@ -130,14 +142,15 @@ should return [4 , 3 , 1], see the code below.
```agda
filter : {X : Type} (p : X → Bool) → List X → List X
filter = {!!}
filter p [] = []
filter p (x :: xs) = if p x then x :: filter p xs else filter p xs
is-non-zero : → Bool
is-non-zero zero = false
is-non-zero (suc _) = true
filter-example : filter is-non-zero (4 :: 3 :: 0 :: 1 :: 0 :: []) ≡ 4 :: 3 :: 1 :: []
filter-example = {!!} -- refl _ should fill the hole here
filter-example = refl _ -- refl _ should fill the hole here
```
## Part II: The identity type of the Booleans (★/★★)
@ -152,7 +165,10 @@ are the same natural number, or else is empty, if `x` and `y` are different.
```agda
_≣_ : Bool → Bool → Type
a ≣ b = {!!}
true ≣ true = 𝟙
true ≣ false = 𝟘
false ≣ true = 𝟘
false ≣ false = 𝟙
```
### Exercise 2 (★)
@ -161,7 +177,8 @@ a ≣ b = {!!}
```agda
Bool-refl : (b : Bool) → b ≣ b
Bool-refl = {!!}
Bool-refl true = ⋆
Bool-refl false = ⋆
```
### Exercise 3 (★★)
@ -175,10 +192,16 @@ back and forth between `a ≣ b` and `a ≡ b`.
```agda
≡-to-≣ : (a b : Bool) → a ≡ b → a ≣ b
≡-to-≣ = {!!}
≡-to-≣ true true x = ⋆
≡-to-≣ true false ()
≡-to-≣ false true ()
≡-to-≣ false false x = ⋆
≣-to-≡ : (a b : Bool) → a ≣ b → a ≡ b
≣-to-≡ = {!!}
≣-to-≡ true true ⋆ = refl _
≣-to-≡ true false ()
≣-to-≡ false true ()
≣-to-≡ false false ⋆ = refl _
```
## Part III: Proving in Agda (★★/★★★)
@ -199,7 +222,10 @@ Use pattern matching to **prove** that `||` is commutative.
```agda
||-is-commutative : (a b : Bool) → a || b ≡ b || a
||-is-commutative a b = {!!}
||-is-commutative true true = refl _
||-is-commutative true false = refl _
||-is-commutative false true = refl _
||-is-commutative false false = refl _
```
### Exercise 2 (★★)
@ -208,8 +234,11 @@ Taking inspiration from the above, try to **state** and **prove** that `&&` is
commutative.
```agda
&&-is-commutative : {!!}
&&-is-commutative = {!!}
&&-is-commutative : (a b : Bool) → a && b ≡ b && a
&&-is-commutative true true = refl _
&&-is-commutative true false = refl _
&&-is-commutative false true = refl _
&&-is-commutative false false = refl _
```
### Exercise 3 (★★)
@ -218,10 +247,24 @@ commutative.
```agda
&&-is-associative : (a b c : Bool) → a && (b && c) ≡ (a && b) && c
&&-is-associative = {!!}
&&-is-associative true true true = refl _
&&-is-associative true true false = refl _
&&-is-associative true false true = refl _
&&-is-associative true false false = refl _
&&-is-associative false true true = refl _
&&-is-associative false true false = refl _
&&-is-associative false false true = refl _
&&-is-associative false false false = refl _
&&'-is-associative : (a b c : Bool) → a &&' (b &&' c) ≡ (a &&' b) &&' c
&&'-is-associative = {!!}
&&'-is-associative true true true = refl _
&&'-is-associative true true false = refl _
&&'-is-associative true false true = refl _
&&'-is-associative true false false = refl _
&&'-is-associative false true true = refl _
&&'-is-associative false true false = refl _
&&'-is-associative false false true = refl _
&&'-is-associative false false false = refl _
```
**Question**: Can you spot a downside of the more verbose definition of `&&'`
@ -249,7 +292,10 @@ max-is-commutative (suc n) (suc m) = to-show
```agda
min-is-commutative : (n m : ) → min n m ≡ min m n
min-is-commutative = {!!}
min-is-commutative zero zero = refl _
min-is-commutative zero (suc m) = refl _
min-is-commutative (suc n) zero = refl _
min-is-commutative (suc n) (suc m) = ap suc (min-is-commutative n m)
```
### Exercise 5 (★★★)
@ -259,7 +305,8 @@ number `n`.
```agda
0-right-neutral : (n : ) → n ≡ n + 0
0-right-neutral = {!!}
0-right-neutral zero = refl _
0-right-neutral (suc n) = ap suc (0-right-neutral n)
```
### Exercise 6 (★★★)
@ -271,9 +318,11 @@ Try to **prove** these equations using pattern matching and inductive proofs.
```agda
map-id : {X : Type} (xs : List X) → map id xs ≡ xs
map-id xs = {!!}
map-id {X} [] = refl _
map-id {X} (x :: xs) = ap (λ xs → x :: xs) (map-id xs)
map-comp : {X Y Z : Type} (f : X → Y) (g : Y → Z)
(xs : List X) → map (g ∘ f) xs ≡ map g (map f xs)
map-comp f g xs = {!!}
map-comp {X} {Y} {Z} f g [] = refl _
map-comp {X} {Y} {Z} f g (x :: xs) = ap (λ xs → g (f x) :: xs) (map-comp f g xs)
```