aesop に追加の補題を渡す方法を説明する

[Seasawher]

現在 aesop の説明では，attribute をどのように付けるとどのような効果があるかということが書かれていない
それを説明する

[Seasawher]

aesop (add safe [while_iff]) みたいな感じでいける。引数で渡すのではなくて、専用の構文が用意されているようだ。

[Seasawher]

aesopのテストコードを見ればよいということに気づいた

https://github.com/leanprover-community/aesop/blob/master/AesopTest/13_2.lean

[Seasawher]

こういう例を作った

/- # aesop をカスタマイズする -/
import Aesop

inductive MyList (α : Type)
  | nil
  | cons (head : α) (tail : MyList α)

variable {α : Type}

def MyList.append : (as bs : MyList α) → MyList α
  | nil, bs => bs
  | cons a as, bs => cons a (MyList.append as bs)

instance : Append (MyList α) := ⟨MyList.append⟩

@[simp]
theorem nil_append : MyList.nil ++ xs = xs := rfl

@[simp]
theorem cons_append : MyList.cons x xs ++ ys = MyList.cons x (xs ++ ys) := rfl

inductive NonEmpty : MyList α → Prop
  | cons x xs : NonEmpty (MyList.cons x xs)

attribute [aesop safe constructors] NonEmpty

-- aesop で `NonEmpty _` という形のゴールを示せるようになった
example : NonEmpty (MyList.cons 1 MyList.nil) := by aesop

attribute [aesop safe cases] NonEmpty

-- aesop で `NonEmpty _` という形の仮定を利用できるようになった
example (xs ys : MyList α) (h : NonEmpty xs) : NonEmpty (xs ++ ys) := by aesop?