-- AGDA IN PADOVA 2022
-- Exercise sheet 5

data  : Set where
  zero : 
  succ :   

data  : Set where

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

infixl 5 _≡_
infixl 6 _+_
infixl 7 _·_

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

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


------------------------------------
----[ GENERALITIES ON EQUALITY ]----
------------------------------------

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

trans : {A : Set} {x y z : A}  x  y  y  z  x  z
trans refl q = q

-- EQUATIONAL REASONING

infix  3 _∎
infixr 2 _≡⟨_⟩_ _≡⟨⟩_
infix  1 begin_

_≡⟨_⟩_ : {A : Set} {y z : A}  (x : A)  x  y  y  z  x  z
x ≡⟨ p  q = trans p q

_≡⟨⟩_ : {A : Set} {y : A}  (x : A)  (q : x  y)  x  y
x ≡⟨⟩ q = q

_∎ : {A : Set}  (x : A)  x  x
x  = refl

begin_ : {A : Set} {x y : A}  x  y  x  y
begin p = p


---------------------------------
----[ EQUALITIES OF NUMBERS ]----
---------------------------------

lemma-+-zero : (a : )  (a + zero)  a
lemma-+-zero zero     = refl
lemma-+-zero (succ a) = cong succ (lemma-+-zero a)
-- (lemma-+-zero a) is a value of type ((a + zero) ≡ a).
-- What we need is a value of type (succ (a + zero) ≡ succ a).

lemma-+-succ : (a b : )  (a + succ b)  succ (a + b)
lemma-+-succ zero     b = refl
lemma-+-succ (succ a) b = cong succ (lemma-+-succ a b)

lemma-+-commutative : (a b : )  (a + b)  (b + a)
lemma-+-commutative zero     b = symm (lemma-+-zero b)
lemma-+-commutative (succ a) b =
  trans (cong succ (lemma-+-commutative a b)) (symm (lemma-+-succ b a))

lemma-+-associative : (a b c : )  (a + (b + c))  ((a + b) + c)
lemma-+-associative a b c = {!!}

lemma-·-distributive : (a b c : )  ((a + b) · c)  ((a · c) + (b · c))
lemma-·-distributive zero b c = refl
lemma-·-distributive (succ a) b c = begin
  ((succ a + b) · c)      ≡⟨⟩
  (succ (a + b) · c)      ≡⟨⟩
  c + ((a + b) · c)       ≡⟨ cong (_+_ c) (lemma-·-distributive a b c) 
  c + ((a · c) + (b · c)) ≡⟨ lemma-+-associative c (a · c) (b · c) 
  (c + (a · c)) + (b · c) ≡⟨⟩
  (succ a · c) + (b · c)  

-- EXERCISE: Prove this theorem.
lemma-+-swap : (a b c : )  (a + (b + c))  (b + (a + c))
lemma-+-swap zero     b c = refl
lemma-+-swap (succ a) b c = begin
  (succ a + (b + c)) ≡⟨⟩
  succ (a + (b + c)) ≡⟨ cong succ (lemma-+-swap a b c) 
  succ (b + (a + c)) ≡⟨ symm (lemma-+-succ b (a + c)) 
  b + succ (a + c)   ≡⟨⟩
  b + (succ a + c)   
-- Note: There is a second solution without a case distinction.
-- This second solution instead appeals to associativity and commutativity.

lemma-+-swap' : (a b c : )  (a + (b + c))  (b + (a + c))
lemma-+-swap' zero     b c = refl
lemma-+-swap' (succ a) b c = trans (cong succ (lemma-+-swap a b c)) (symm (lemma-+-succ b (a + c)))

-- EXERCISE: Verify associativity of multiplication.
lemma-·-associative : (a b c : )  ((a · (b · c))  ((a · b) · c))
lemma-·-associative zero     b c = refl
lemma-·-associative (succ a) b c = begin
  (succ a) · (b · c)    ≡⟨⟩
  (b · c) + a · (b · c) ≡⟨ cong  z  b · c + z) (lemma-·-associative a b c) 
  (b · c) + (a · b) · c ≡⟨ symm (lemma-·-distributive b (a · b) c) 
  (b + a · b) · c       ≡⟨⟩
  (succ a · b) · c      

-- LET'S RESUME AT 15:36 :-)

-- EXERCISE: Fill in this hole.
lemma-·-zero : (a : )  ((a · zero)  zero)
lemma-·-zero a = {!!}

-- EXERCISE: Fill in this hole.
lemma-·-succ : (a b : )  ((a · succ b)  (a + (a · b)))
lemma-·-succ a b = {!!}

-- EXERCISE: Verify commutativity of multiplication.
-- Hint: lemma-·-zero and lemma-·-succ will come in handy.
lemma-·-commutative : (a b : )  ((a · b)  (b · a))
lemma-·-commutative a b = {!!}


-----------------------------
----[ MORE ON RELATIONS ]----
-----------------------------

data Even :   Set where
  base-even : Even zero
  step-even : {n : }  Even n  Even (succ (succ n))

-- 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
  empty : AllEven []
  cons  : {x : } {xs : List }  Even x  AllEven xs  AllEven (x  xs)

data Dec (X : Set) : Set where
  yes : X        Dec X
  no  : (X  )  Dec X

data Odd :   Set where
  base-odd : Odd (succ zero)
  step-odd : {n : }  Odd n  Odd (succ (succ n))

data _⊎_ (A B : Set) : Set where
  left  : A  A  B
  right : B  A  B

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

lemma-odd-and-even : {a : }  Odd a  Even a  
lemma-odd-and-even (step-odd q) (step-even p) = lemma-odd-and-even q p

even? : (n : )  Dec (Even n)
even? n with lemma-even-odd n
... | left  p = yes p
... | right q = no (lemma-odd-and-even q)

all-even? : (xs : List )  Dec (AllEven xs)
all-even? []       = yes empty
all-even? (x  xs) with even? x with all-even? xs
... | yes p | yes f = yes (cons p f)
... | yes p | no  g = {!!}
... | no  q | _ = no λ { (cons r _)  q r }

-- EXERCISE: Show that the sum of the elements of a list satisfying "AllEven" is even.
sum : List   
sum []       = zero
sum (x  xs) = x + sum xs

lemma-+-even : {a b : }  Even a  Even b  Even (a + b)
lemma-+-even p q = {!!}

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

-- EXERCISE: Define the relation _≤_ on natural numbers.
data _≤_ :     Set where
  base : {a : }    a  a
  step : {a b : }  a  b  a  succ b

data Bool : Set where
  false true : Bool

-- Boolean-based approach as in Haskell
≤? :     Bool
≤? zero     b        = true
≤? (succ a) zero     = false
≤? (succ a) (succ b) = ≤? a b

-- translation of the preceding Boolean-based definition to a relational definition:
data _≤'_ :     Set where
  base' : {b : }    zero ≤' b
  step' : {a b : }  a ≤' b  succ a ≤' succ b

{-
data Dec (X : Set) : Set where
  yes : X       → Dec X
  no  : (X → ⊥) → Dec X
  -}

≤'-is-decidable : (a b : )  Dec (a ≤' b)
≤'-is-decidable zero     b        = yes base'
≤'-is-decidable (succ a) zero     = no {!!}
≤'-is-decidable (succ a) (succ b) with ≤'-is-decidable a b
... | yes p = yes (step' p)
... | no  q = no  {!!}
-- EXERCISES: fill these in :-)

{-
foo : (a b : ℕ) → a ≤ b → ...

foo : (a b : ℕ) → ≤? a b ≡ true → ...
-}

-- 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
  empty : All P []
  cons  : {x : A} {xs : List A}  P x  All P xs  All P (x  xs)

-- 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
  here  : {x : A} {xs : List A}  P x       Any P (x  xs)
  there : {x : A} {xs : List A}  Any P xs  Any P (x  xs)

-- 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
  here  : {a : A}   {xs : List A}  a  (a  xs)
  there : {a x : A} {xs : List A}  a  xs  a  (x  xs)

-- EXERCISE: Show that "x ∈ ys" if and only if "Any (_≡_ x) ys".
∈-to-Any : {A : Set} {x : A} {ys : List A}  x  ys  Any (_≡_ x) ys
∈-to-Any = {!!}

Any-to-∈ : {A : Set} {x : A} {ys : List A}  Any (_≡_ x) ys  x  ys
Any-to-∈ = {!!}