{-# OPTIONS --allow-unsolved-metas #-}
{-
  AGDA IN PADOVA 2024
  Exercise sheet 2

  ┌─ 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/exercise02.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 ~/solutions02.agda.
-}


-- ─────────────────────────────
-- ────[ BASIC DEFINITIONS ]────
-- ─────────────────────────────

data Bool : Set where
  false : Bool
  true  : Bool

_&&_ : Bool  Bool  Bool
false && b     = false
true  && false = false
true  && true  = true

!_ : Bool  Bool
! false = true
! true  = false

data  : Set where
  zero : 
  succ :   

_+_ :     
zero   + b = b
succ a + b = succ (a + b)

_·_ :     
zero   · b = zero
succ a · b = b + (a · b)

data  : Set where


-- ──────────────────────────────────
-- ────[ PROGRAMMING WITH LISTS ]────
-- ──────────────────────────────────

data List (A : Set) : Set where
  []  : List A
  _∷_ : A  List A  List A

-- EXERCISE: Define a function which sums the numbers of a given list.
sum : List   
sum xs = {!!}

-- EXERCISE: Define a function which computes the length of a given list.
length : List   
length xs = {!!}

-- EXERCISE: Define the "map" function.
-- For instance, "map f (x ∷ y ∷ z ∷ []) = f x ∷ f y ∷ f z ∷ []".
map : {A B : Set}  (A  B)  List A  List B
map f xs = {!!}


-- ────────────────────────────────────
-- ────[ PROGRAMMING WITH VECTORS ]────
-- ────────────────────────────────────

data Vector (A : Set) :   Set where
  []  : Vector A zero
  _∷_ : {n : }  A  Vector A n  Vector A (succ n)

-- EXERCISE: Define a function which computes the length of a given vector.
-- There are two possible implementations, one which runs in constant time
-- and one which runs in linear time.
lengthV : {n : } {A : Set}  Vector A n  
lengthV = {!!}

lengthV' : {n : } {A : Set}  Vector A n  
lengthV' = {!!}

-- EXERCISE: Define the "map" function for vectors.
-- For instance, "map f (x ∷ y ∷ z ∷ []) = f x ∷ f y ∷ f z ∷ []".
mapV : {n : } {A B : Set}  (A  B)  Vector A n  Vector B n
mapV f xs = {!!}

-- EXERCISE: Define these vector functions.
-- For instance, "zipWithV f (x ∷ y ∷ []) (a ∷ b ∷ [])" should evaluate to "f x a ∷ f y b ∷ []".
zipWithV : {A B C : Set} {n : }  (A  B  C)  Vector A n  Vector B n  Vector C n
zipWithV f xs ys = {!!}

-- For instance, "dropV (succ zero) (a ∷ b ∷ c ∷ [])" should evaluate to "b ∷ c ∷ []".
dropV : {A : Set} {n : } (k : )  Vector A (k + n)  Vector A n
dropV k xs = {!!}

-- For instance, "takeV (succ zero) (a ∷ b ∷ c ∷ [])" should evaluate to "a ∷ []".
takeV : {A : Set} {n : } (k : )  Vector A (k + n)  Vector A k
takeV n xs = {!!}

-- For instance, "(a ∷ b ∷ []) ++ (c ∷ d ∷ [])" should evaluate to "a ∷ b ∷ c ∷ d ∷ []".
_++_ : {A : Set} {n m : }  Vector A n  Vector A m  Vector A (n + m)
xs ++ ys = {!!}

-- For instance, "snocV (a ∷ b ∷ []) c" should evaluate to "a ∷ b ∷ c ∷ []".
snocV : {A : Set} {n : }  Vector A n  A  Vector A (succ n)
snocV xs y = {!!}

-- For instance, "reverseV (a ∷ b ∷ c ∷ [])" should evaluate to "c ∷ b ∷ a ∷ []".
reverseV : {A : Set} {n : }  Vector A n  Vector A n
reverseV xs = {!!}

-- For instance, "concatV ((a ∷ b ∷ []) ∷ (c ∷ d ∷ []) ∷ [])" should evaluate to
-- "a ∷ b ∷ c ∷ d ∷ []".
concatV : {!!}
concatV = {!!}


-- ────────────────────────────────────────────
-- ────[ MORE PROOFS WITH NATURAL NUMBERS ]────
-- ────────────────────────────────────────────

-- "Even n" is the type of witnesses that "n" is even.
data Even :   Set where
  base-even : Even zero
  step-even : {n : }  Even n  Even (succ (succ n))

-- "Odd n" is the type of witnesses that "n" is odd.
data Odd :   Set where
  base-odd : Odd (succ zero)
  step-odd : {n : }  Odd n  Odd (succ (succ n))

-- EXERCISE: Show that the sum of even numbers is even.
lemma-sum-even : {a b : }  Even a  Even b  Even (a + b)
lemma-sum-even = {!!}

-- EXERCISE: Show that the successor of an even number is odd and vice versa.
lemma-succ-even : {a : }  Even a  Odd (succ a)
lemma-succ-even = {!!}

lemma-succ-odd : {a : }  Odd a  Even (succ a)
lemma-succ-odd = {!!}

-- EXERCISE: Show that the sum of odd numbers is even.
lemma-sum-odd : {a b : }  Odd a  Odd b  Even (a + b)
lemma-sum-odd = {!!}

-- EXERCISE: Show that the sum of an odd number with an even number is odd.
lemma-sum-mixed : {a b : }  Odd a  Even b  Odd (a + b)
lemma-sum-mixed = {!!}

-- EXERCISE: Show that it cannot be that a number is both even and odd.
lemma-odd-and-even : {a : }  Odd a  Even a  
lemma-odd-and-even P q = {!!}

-- EXERCISE: Show that every number is even or odd.
data _⊎_ (A B : Set) : Set where
  left  : A  A  B
  right : B  A  B
-- For instance, if x : A, then left x : A ⊎ B.

lemma-even-odd : (a : )  Even a  Odd a
lemma-even-odd a = {!!}


-- ─────────────────────────────
-- ────[ PROOFS WITH LISTS ]────
-- ─────────────────────────────

-- EXERCISE: Define a predicate "AllEven" for lists of natural numbers
-- such that "AllEven xs" is inhabited if and only if all entries of the list "xs" are even.
-- By convention, the empty list counts as consisting of even-only elements.
data AllEven : List   Set where
  {- supply appropriate clauses here -}

lemma-sum-of-even-list-is-even : (xs : List )  AllEven xs  Even (sum xs)
lemma-sum-of-even-list-is-even xs p = {!!}

-- EXERCISE: Define a predicate "All P" for lists of elements of some type A
-- and predicates "P : A → Set" such that "All P xs" is inhabited if
-- and only if all entries of the list "xs" satisfy P.
-- The special case "All Even" should coincide with the predicate
-- "AllEven" from the previous exercise.
data All {A : Set} (P : A  Set) : List A  Set where
  {- give appropriate clauses -}

-- EXERCISE: Define a predicate "Any P" for lists of elements of some type A
-- and predicates "P : A → Set" such that "Any P xs" is inhabited if
-- and only if at least one entry of the list "xs" satisfies P.
data Any {A : Set} (P : A  Set) : List A  Set where
  {- give appropriate clauses -}

-- EXERCISE: Define a relation "_∈_" such that "x ∈ ys" is the type
-- of witnesses that x occurs in the list ys.
data _∈_ {A : Set} : A  List A  Set where
  {- give appropriate clauses -}