delta タクティクを紹介する

割と必要になることがある。再帰関数が等しいことを証明しようとすると必要だったり。

以下は delta が必要な例

import Plausible

namespace Foldr
  /- ## foldr で書ける関数たち -/

  variable {α β : Type}

  /-- 和の計算 -/
  def sum [Zero α] [Add α] (xs : List α) : α :=
    match xs with
    | [] => 0
    | x :: xs => x + sum xs

  -- インスタンス暗黙引数を使うことはできない(未実装)
  #guard_msgs (drop error) in
    #test ∀{α : Type}[Zero α][Add α](xs : List α), sum xs = xs.foldr (· + ·) 0

  example [Zero α] [Add α] (xs : List α) : sum xs = xs.foldr (· + ·) 0 := by
    -- 単に rfl としても失敗する
    fail_if_success rfl

    -- simp では示すことができない
    fail_if_success simp_all [sum, List.foldr]

    delta sum List.foldr
    rfl

end Foldr

Start with the supplied Foldr example and its use of the delta tactic. Add an explanation of when delta is needed for unfolding definitions, keeping the example understandable and accurate. Done means the documentation clearly introduces delta and includes the demonstrated proof context.