`termination_by` を使うと rfl が通らなくなる例を紹介する

[Seasawher]

同じことをする関数であっても、整礎再帰を使っていると irreducible になってしまって rfl や decide が通らなくなる

/-- 整礎再帰(well-founded recursion)を使用したバージョン -/
def String.padLeftWF (input : String) (padChar : Char) (length : Nat) : String :=
  if input.length ≥ length then
    input
  else
    String.padLeftWF (padChar.toString ++ input) padChar length
termination_by length - input.length

example : String.padLeftWF "42" '0' 5 = "00042" := by
  -- rfl では証明することができない
  fail_if_success rfl

  -- decide でも証明できない
  fail_if_success decide

  native_decide

/-- 整礎再帰(well-founded recursion)を使用していないバージョン -/
def String.padLeft (input : String) (padChar : Char) (length : Nat) : String :=
  if input.length ≥ length then
    input
  else
    let padding : String := String.pushn "" padChar (length - input.length)
    padding ++ input

example : String.padLeft "42" '0' 5 = "00042" := by
  -- rfl で証明できる
  rfl