Dependently typed FizzBuzz, now with 30% more constructive thinking

FizzBuzzC.idr

module FizzBuzzC

%default total

-- Dependently typed FizzBuzz, constructively

-- A number is fizzy if it is evenly divisible by 3
data Fizzy : Nat -> Type where
  ZeroFizzy : Fizzy 0
  Fizz : Fizzy n -> Fizzy (3 + n)

-- Fizzy is a correct specification of divisibility by 3 - that is, if n is
-- fizzy then there exists some k such that n = 3*k.
fizzyCorrect : (n : Nat) -> Fizzy n -> (k : Nat ** n = 3 * k)
fizzyCorrect Z ZeroFizzy = (Z ** Refl)
fizzyCorrect (S (S (S k))) (Fizz x) =
  let (k' ** ih) = fizzyCorrect k x
  in (S k' ** ?fizzyIsAOK)

-- Basic fizziness lemmas
oneNotFizzy : Not (Fizzy 1)
oneNotFizzy (Fizz f) impossible

twoNotFizzy : Not (Fizzy 2)
twoNotFizzy (Fizz f) impossible

fizzyUp : Not (Fizzy n) -> Not (Fizzy (3 + n))
fizzyUp nope ZeroFizzy impossible
fizzyUp nope (Fizz f) = nope f

-- Fizziness is decidable
decFizzy : (n : Nat) -> Dec (Fizzy n)
decFizzy Z = Yes ZeroFizzy
decFizzy (S Z) = No oneNotFizzy
decFizzy (S (S Z)) = No twoNotFizzy
decFizzy (S (S (S k))) with (decFizzy k)
  decFizzy (S (S (S k))) | (Yes prf) = Yes (Fizz prf)
  decFizzy (S (S (S k))) | (No contra) = No $ fizzyUp contra

-- A number is buzzy if it is evenly divisible by 5
data Buzzy : Nat -> Type where
  ZeroBuzzy : Buzzy 0
  Buzz : Buzzy n -> Buzzy (5 + n)

-- Correctness of buzziness spec elided due to verbosity

oneNotBuzzy : Not (Buzzy 1)
oneNotBuzzy (Buzz b) impossible

twoNotBuzzy : Not (Buzzy 2)
twoNotBuzzy (Buzz b) impossible

threeNotBuzzy : Not (Buzzy 3)
threeNotBuzzy (Buzz b) impossible

fourNotBuzzy : Not (Buzzy 4)
fourNotBuzzy (Buzz b) impossible

buzzOff : Not (Buzzy n) -> Not (Buzzy (5 + n))
buzzOff nope ZeroBuzzy impossible
buzzOff nope (Buzz b) = nope b

decBuzzy : (n : Nat) -> Dec (Buzzy n)
decBuzzy Z = Yes ZeroBuzzy
decBuzzy (S Z) = No oneNotBuzzy
decBuzzy (S (S Z)) = No twoNotBuzzy
decBuzzy (S (S (S Z))) = No threeNotBuzzy
decBuzzy (S (S (S (S Z)))) = No fourNotBuzzy
decBuzzy (S (S (S (S (S k))))) with (decBuzzy k)
  decBuzzy (S (S (S (S (S k))))) | (Yes prf) = Yes (Buzz prf)
  decBuzzy (S (S (S (S (S k))))) | (No way) = No (buzzOff way)

-- A version of Dec that tracks two properties - DoubleDec A B is isomorphic
-- to (Dec A, Dec B). This is just for readability.
data DoubleDec : Type -> Type -> Type where
  Neither : Not a -> Not b -> DoubleDec a b
  First : a -> Not b -> DoubleDec a b
  Second : Not a -> b -> DoubleDec a b
  Both : a -> b -> DoubleDec a b

decFizzBuzz : (n : Nat) -> DoubleDec (Fizzy n) (Buzzy n)
decFizzBuzz n with (decFizzy n, decBuzzy n)
  decFizzBuzz n | (Yes f, Yes b) = Both f b
  decFizzBuzz n | (No nf, Yes b) = Second nf b
  decFizzBuzz n | (Yes f, No nb) = First f nb
  decFizzBuzz n | (No nf, No nb) = Neither nf nb


-- Let's show some fizzing and buzzing. Start with all the nats:
nats : Stream Nat
nats = iterate S Z

-- and the fizzed and buzzed nats
fizzBuzz : Stream (n : Nat ** DoubleDec (Fizzy n) (Buzzy n))
fizzBuzz = map (\n => (n ** (decFizzBuzz n))) (tail nats)

instance Show (n : Nat ** DoubleDec (Fizzy n) (Buzzy n)) where
  show (x ** Neither _ _) = show x
  show (x ** First _ _)   = "Fizz"
  show (x ** Second _ _)  = "Buzz"
  show (x ** Both _ _)    = "FizzBuzz"

-- Take the first 100 numbers' FizzBuzzes, then print them to the screen.
namespace Main
  main : IO ()
  main = sequence_ . map (putStrLn . show) . take 100 $ fizzBuzz

---------- Proofs ----------

FizzBuzzC.fizzyIsAOK = proof
  compute
  intros
  rewrite plusSuccRightSucc k' (plus k' 0)
  rewrite plusSuccRightSucc k' (S (plus k' (plus k' 0)))
  rewrite plusSuccRightSucc k' (plus k' (plus k' 0))
  rewrite ih
  trivial

Can you upload this to Github with a proper open source license? I'd like to add as another RosettaCode.org FizzBuzz answer.