{-# 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.