第 5 回
帰納的なデータ型 (再帰を含まないもの/含むもの) ，
再帰関数の定義， 帰納法

• プリント

• 2 節の例の
      Definition f :=
          season_rec (fun _ => nat) 0 1 2 3.
  で，_ はワイルドカード。x : season などと書いても同じ。
  後ろの 0 1 2 3 は，各季節を受け取ったときに返す値。
• 4 節の nengou の例で，OCaml では，
      type nengou = Meiji of int ...
  などとなるが，Coq では，
      Meiji : nat -> nengou ...
  であることに注意。nat -> nengou というのが Meiji 自体の持つ型で あり，Meiji は関数である。
• simpl は仮定にもかけられる。
  例えば，H という仮定があったときに，
      simpl in H.
  とすると，H に simpl がかかる。
• 再帰を含まない帰納的なデータ型に対する証明のとき， 場合分けで case を使って証明がうまく行かなかったら， induction のほうを使う。
  case だと，Goal だけが場合分けされて case に適用した仮定もそのまま仮定に残るが， induction では induction に適用した仮定は消えて， 場合分けされた値が他の仮定に代入された上で証明を進める ことができる。
  例えば，季節を受け取ったら次の季節を返すという関数 next_season を定義した上で，
      Lemma before_summer_is_spring :
          forall s : season, (next_season s = Summer) -> s = Spring.
  という補題を証明する場合，
  
      intros s H.
      case s.
  
  とすると，
  
    4 subgoals
  
      s : season
      H : next_season s = Summer
      ==========================
        Spring = Spring
  
    subgoal 2 is:
      Summer = Spring
    subgoal 3 is:
      Fall = Spring
    subgoal 4 is:
      Winter = Spring
  
  となるが，
  
      intros s H.
      induction s.
  
  とすると，
  
    4 subgoals
  
      H : next_season Spring = Summer
      ==========================
        Spring = Spring
  
    subgoal 2 is:
      Summer = Spring
    subgoal 3 is:
      Fall = Spring
    subgoal 4 is:
      Winter = Spring
  
  となる。