Proof by computation

Stream: new members

[Li Xuanji]

Is there a way to prove the theorem helpMe in a shorter way?

import Std

def padWithO (n : Nat) (s : String) : String :=
  if s.length ≥ n then
    s
  else
    padWithO n ("o" ++ s)
termination_by n - s.length
decreasing_by
  have : "o".length = 1 := by rfl
  grind [String.length_append]

#eval padWithO 5 "abc"

theorem helpMe : padWithO 5 "abc" = "ooabc" := by
  unfold padWithO
  simp
  rw [show "abc".length = 3 by rfl]
  simp
  unfold padWithO
  simp
  rw [show "oabc".length = 4 by rfl]
  simp
  unfold padWithO
  rw [show "ooabc".length = 5 by rfl]
  simp

[Weiyi Wang]

I go with the title, "proof by computation" would be

theorem helpMe : padWithO 5 "abc" = "ooabc" := by native_decide

But native_decide can be considered dangerous in some context, so please wait for a better answer by someone else

[Weiyi Wang]

Oh, this works

theorem helpMe : padWithO 5 "abc" = "ooabc" := by
  decide +kernel

[Li Xuanji]

Oh, interesting, decide +kernel fails on v24 but succeeds on Latest. Looks like we gained some Decidable instances recently.

[Yan Yablonovskiy 🇺🇦]

Note that if you add @[reducible] to the def then decide works on its own.

Without that you can also do

theorem helpMe : padWithO 5 "abc" = "ooabc" := by with_unfolding_all decide

[Robin Arnez]

@[reducible] is probably not the best idea but @[semireducible] is the right thing to do here.