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.