module X3 where ---------------------------------------------------------------------- -- Lecture 3 : Finite Sets -- ---------------------------------------------------------------------- data Nat : Set where zero : Nat suc : Nat -> Nat data Fin : Nat -> Set where fzero : {n : Nat} -> Fin (suc n) fsuc : {n : Nat} -> Fin n -> Fin (suc n) data Maybe (X : Set) : Set where just : X -> Maybe X nothing : Maybe X {- The following function converts a Fin to a Nat, forgetting the knowledge that its size is bounded. -} # : {n : Nat} -> Fin n -> Nat # fzero = zero # (fsuc i) = suc (# i) {- (3.1) Define, for each n, the largest element of Fin (suc n) -} fmax : {n : Nat} -> Fin (suc n) fmax {n} = {! !} {- (3.2) Define the function fembed, taking Fin n to Fin (suc n), preserving #, ie we want that # (fembed i) = # i -} fembed : {n : Nat} -> Fin n -> Fin (suc n) fembed i = {! !} {- (3.3) Define thin, such that such that thin i is injective and order preserving, and such that thin i j is not equal to i -} {- Informally, the idea is that thin i gives anything but i, so that thin 2 0 = 0 thin 2 1 = 1 thin 2 2 = 3 thin 2 3 = 4 ... -} thin : {n : Nat} -> Fin (suc n) -> Fin n -> Fin (suc n) thin i j = {! !} {- (3.4*) Define thick i to be the partial inverse of thin i, so that thick i i = nothing, and thick i j = just k implies thin i k = j -} thick : {n : Nat} -> Fin (suc n) -> Fin (suc n) -> Maybe (Fin n) thick i j = {! !} -- Additive Structure _+_ : Nat -> Nat -> Nat zero + y = y suc x + y = suc (x + y) data _:+:_ (S T : Set) : Set where inl : S -> S :+: T inr : T -> S :+: T -- Let's construct an isomorphism between -- Fin m :+: Fin n and Fin (m + n) {- (3.5) Show how to map Fin m to the lowest m elements of Fin (m + n) -} finl : (m n : Nat) -> Fin m -> Fin (m + n) finl m n i = {! !} {- (3.6) Show how to map Fin n to the highest n elements of Fin (m + n) -} finr : (m n : Nat) -> Fin n -> Fin (m + n) finr m n j = {! !} -- So now we have finSum : (m n : Nat) -> Fin m :+: Fin n -> Fin (m + n) finSum m n (inl i) = finl m n i finSum m n (inr j) = finr m n j {- (3.7) Show how to invert finSum -} finCase : (m n : Nat) -> Fin (m + n) -> Fin m :+: Fin n finCase m n i = {! !} {- (3.8*) Now play the same game with multiplication -} _*_ : Nat -> Nat -> Nat zero * y = zero suc x * y = y + (x * y) data _:*:_ (S T : Set) : Set where _,_ : S -> T -> S :*: T finPair : (m n : Nat) -> Fin m :*: Fin n -> Fin (m * n) finPair m n (i , j) = {! !} finSplit : (m n : Nat) -> Fin (m * n) -> Fin m :*: Fin n finSplit m n ij = {! !}