第 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

    となる。