Leanで遊んでいる．しかし簡単な命題の証明も大変だ……．書いているのに無駄が多い気もするけど．Lean勉強会の教材で遊んで，大体終わったのでなんか色々試しているところ．たまにあれこれどうするんだっけというやつをメモ．

• h : Odd nを使いたいときは，rw[Odd] at hとするとOddの定義が展開される．これは∃k n = 2 * k + 1と定義されているので．apply Exists.elimの後intro k hkとすれば整数kとhk : n = 2 * k + 1が得られる．
• 通常の自然数nに関する帰納法は

  induction n with
  | zero => ...
  | succ n => ...
  

  でできるが，n未満のすべてを仮定してnを示すという形の帰納法はNat.strongInductionOnという形で使える．とりあえず次のようにしたら動いた．

  apply Nat.strongInductionOn n
  intro n ih
  

  ihにはn未満での示したい命題（ゴール）の成立が入っている．この場合だと最初のステップは不要なのでnでの証明を試みればいいけど，0だけ議論が変わったりするならmatch n withで場合分けすればよい．ところでmatchとcasesの違いがよくわかっていない．
• 仮定がh ; A ∨ Bの時に場合分けするならば

  cases h with
  | inl h => ...
  | inr h => ...
  

  （基本ですね．）
• 自明な式だがLeanが処理してくれない，ということはよくある．何か命題を持ってくる必要があるのだがapply?とすると対応するものを探してくれる……けど複雑な状況ではうまくいかない．必要な形でシンプルにしてtheorem tmp ***:*** := by apply?とかするとほしいものを出してくれる．
• A ∧ Bを示す時は（And.Introでもよいが）constructorをするとAの証明とBの証明に集中する．
• 次がだめなのはどうすればいいんだろう？（fの定義のRをℤ[X]にすれば通る．）R内の積が認識されていないらしい．

  open Polynomial
  
  def R := ℤ[X]
  noncomputable def f (n : Nat) : R := X^(n)
  
  theorem thm (n m : Nat) : (f n) * (f m) = f (n + m) := by
    simp[f]
    apply (pow_add X n m).symm
  

• 関数のn回合成をf^nとかけるようにと思って次のようにしてみた．

  open Nat
  def fun_pow {α : Type u} (f : α → α) (n : Nat) : (α → α):=
  match n with
  | 0 => id
  | succ n => (fun_pow f n)∘ f
  
  instance {α : Type u} : Pow (α → α) (Nat) := ⟨fun_pow⟩
  
  def f : ℕ → ℕ
  | 0 => 0
  | succ n => n
  
  theorem a : fun_pow f 2 = f ∘ f := by simp
  theorem aa : f^(2) = f ∘ f := by simp
  

  aとaaは何が違うのだろう？（aは通るがaaは駄目，というかf^(n)の方を使うと何も示せない……．）