module FinQuestions where

data Nat : Set where
  z : Nat
  s : Nat → Nat

_+_ : Nat → Nat → Nat
z   + n = n
s m + n = s (m + n)

data Fin : Nat → Set where
  fz : ∀{n} → Fin (s n)
  fs : ∀{n} → Fin n → Fin (s n)


-- should give return the largest element in the finite set (fz is the smallest)
fmax : ∀{n} → Fin (s n)
fmax = ?

-- should embed a element of a finite set into a larger one preserving its value.
emb : ∀{n} → Fin n → Fin (s n)
emb = ?

data Vec (X : Set) : Nat → Set where
  [] : Vec X z
  _::_ : ∀{n} → X → Vec X n → Vec X (s n)

lookup : ∀{X n} → Vec X n → Fin n →  X
lookup = {!!}

tabulate : ∀{X n} → (Fin n → X) → Vec X n
tabulate = {!!}

-- prove that it's an isomorphism
data _≅_ {A : Set} : {A' : Set} → A → A' → Set where
  refl : {a : A} → a ≅ a

resp : ∀{A B}(f : A → B){a a' : A} → a ≅ a' → f a ≅ f a'
resp f refl = refl

postulate ext : ∀{A B}{f g : A → B} → (∀ a → f a ≅ g a) → f ≅ g

lem1 : ∀{X n}(xs : Vec X n) → tabulate (lookup xs) ≅ xs
lem1 = {!!}

lem2 : ∀{X n}(f : Fin n → X)(i : Fin n) → lookup (tabulate f) i ≅ f i
lem2 = {!!}

id : {X : Set} → X → X
id x = x

_•_ : {A B C : Set} → (B → C) → (A → B) → A → C
f • g = λ a → f (g a)

record Isomorphism (A B : Set) : Set where
  field left  : A → B
        right : B → A
        law1  : (left • right) ≅ id {B}
        law2  : (right • left) ≅ id {A}

looktabIso : ∀{X n} → Isomorphism (Vec X n) (Fin n → X) 
looktabIso = record {
  left  = lookup;
  right = tabulate;
  law1  = ext λ f → ext λ i → lem2 f i;
  law2  = ext lem1}

-- tabulate shows we can give a first order representation of the function space Fin n → X
-- as a vector. Below we narrow it down even further and only consider functions that
-- introduce 'gaps' in the range. These are the so-called thinnings.

data Thin : Nat → Nat → Set where
  done : Thin z z
  keep : ∀{m n} → Thin m n → Thin (s m) (s n)
  skip : ∀{m n} → Thin m n → Thin m     (s n)

mapThin : ∀{m n} → Thin m n → Fin m → Fin n
mapThin = {!!}

idThin : ∀ n → Thin n n
idThin = {!!}

compThin : ∀{m n o} → Thin n o → Thin m n → Thin m o
compThin = {!!}

lem3 : ∀{n}(i : Fin n) → mapThin (idThin n) i  ≅ i
lem3 = {!!}

lem4 : ∀{m n o}(t : Thin n o)(t' : Thin m n)(i : Fin m) → 
       mapThin (compThin t t') i ≅ mapThin t (mapThin t' i)
lem4 = {!!}

lem5 : ∀{m n}(t : Thin m n) → compThin t (idThin m) ≅ t
lem5 = {!!}

lem6 : ∀{m n}(t : Thin m n) → compThin (idThin n) t ≅ t
lem6 = {!!}

lem7 : ∀{m n o p}(t : Thin o p)(t' : Thin n o)(t'' : Thin m n) →
       compThin (compThin t t') t'' ≅ compThin t (compThin t' t'')
lem7 = {!!}

-- starred exercises
--------------------

-- 1.
-- inductively define a more liberal version of Thin which allows multiple
-- inputs to point to the same output value. Define the same operations and prove the same
-- properties.

-- 2.
-- Why did we choose to prove these properties?

data _≤_ : Nat → Nat → Set where
  z≤ : ∀{n} → z ≤ n
  s≤ : ∀{m n} → m ≤ n → s m ≤ s n

-- 3.
weak : ∀ {n} → Thin z n
weak = {!!}

-- 4.
map≤ : ∀{m n} → m ≤ n → Thin m n
map≤ = {!!}

-- 5. what properties should we prove about map and ≤ ? 
-- (I will give you a hint if you're not sure.)
-- 6. Prove them.