Hacker News Reader

Comment by incrudible | Hacker News Reader

Neither of these examples answer my question: What's the point? Perhaps FizzBuzz is a terrible example for such a language, but I don't see anything being "proved" here. Can it do something like static asserts on the output, without actually running the program? E.g. can you prove that the outputs will never be anything else than "Fizz", "Buzz" or "FizzBuzz"?

View on HN

Sure!

  def f (n : Nat) : String :=
    String.append
      (if n % 3 = 0 then "Fizz" else "")
      (if n % 5 = 0 then "Buzz" else "")

  #eval List.map f (List.range 100)

  theorem poop (n : Nat) : f n = "FizzBuzz" ∨ f n = "Fizz" ∨ f n = "Buzz" ∨ f n = "" := by
    unfold f
    split <;> split
    · exact Or.inl rfl
    · exact Or.inr (Or.inl rfl)
    · exact Or.inr (Or.inr (Or.inl rfl))
    · exact Or.inr (Or.inr (Or.inr rfl))

Awesome! Where did the "split_ifs" tactic come from though? Mathlib? In your opinion does it make sense to do program verification without using Mathlib, or would you recommend just using it pretty much all the time?

Yes split_ifs is in Mathlib so I have replaced it with split (twice) which is in Core. I believe there is also an intermediate level Std. I'm not sure why you'd want to avoid Mathlib but I daresay it's possible for many types of problem.

Thank you. I must admit, I have trouble making sense of it.

Just for comparison, in Typescript you can write:

  function f(n:number){
    if (n%3==0 && n%5==0) return "FizzBuzz"
    if (n%3==0) return "Fizz"
    if (n%5==0) return "Buzz"
    return "";
  }

The return type of this function will be inferred as "Fizz"|"Buzz"|"FizzBuzz"|"".

Then, I can write:

  function *iFizzBuzz(steps:number){
     for (let i=0; i<steps; i++){
        const fb = f(i); 
        if (fb) yield fb;
     }
  }

  const fizzBuzz100 = Array.from(iFizzBuzz(100));

The type of fizzBuzz100 will be inferred as ("Fizz"|"Buzz"|"FizzBuzz")[];

Lean will not create a custom type to infer for each function; it will either infer an existing type or report failure; it will also not automatically coerce to String. What you see above is a proof in tactic mode of your specification as a theorem. If you want to guarantee the outputs of a function, you need to specify a custom type. For instance:

    inductive FizzBuzz where
      | fizz
      | buzz
      | fizzBuzz
      | none
    
    def fizzBuzz (n : Nat) : FizzBuzz :=
      if n % 15 == 0 then .fizzBuzz
      else if n % 3 == 0 then .fizz
      else if n % 5 == 0 then .buzz
      else .none
    
    instance : ToString FizzBuzz where
    toString : FizzBuzz → String
      | .none => ""
      | .fizz => "Fizz"
      | .buzz => "Buzz"
      | .fizzBuzz => "FizzBuzz"
    
    def stringFizz (n : Nat) : String :=
      toString <| fizzBuzz n
    
    def printFizz (n : Nat) : IO Unit := do
      println! s!"{fizzBuzz n}"

Oops! I checked the spec and it's supposed do something more like this:

  def f (n : Nat) : String :=
    Option.getD
      (Option.merge String.append
        (if n % 3 = 0 then "Fizz" else none)
        (if n % 5 = 0 then "Buzz" else none))
      (toString n)

  #eval List.map (fun k => f (k + 1)) (List.range 100)

  theorem poop (n : Nat) :
      f n = "FizzBuzz" ∨ f n = "Fizz" ∨ f n = "Buzz" ∨ f n = toString n := by
    unfold f
    split <;> split
    · exact Or.inl rfl
    · exact Or.inr (Or.inl rfl)
    · exact Or.inr (Or.inr (Or.inl rfl))
    · exact Or.inr (Or.inr (Or.inr rfl))

The examples were not meant to answer your question, but the question kristopolous set. Ask your question at top level and some of us, perhaps myself, will answer.

Reply on news.ycombinator.com