termination_by 利用時に rfl / decide が失敗する具体例を TerminationBy に追加

[Copilot]

termination_by を使った整礎再帰定義は、同等の計算をする非再帰定義と比べて還元性が異なり、rfl や decide が通らないケースがあります。
この差分が伝わるよう、TerminationBy の解説に対比付きの最小例を追加しました。

• 追加: 整礎再帰版の実例 (String.padLeftWF)

  • termination_by length - input.length を使う左パディング関数を追加
  • 期待どおり rfl / decide が失敗し、native_decide で示せることを明示

• 追加: 非再帰版の対比例 (String.padLeftSimple)

  • 同等機能の非再帰実装を追加
  • 同じ命題が rfl で証明できることを並べて提示

• ドキュメント構成

  • 既存の termination_by 解説フロー内に、還元性の違いを示す短い説明とコード例を挿入

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
  fail_if_success rfl
  fail_if_success decide
  native_decide