第 6 回
リスト，帰納的な命題の定義

• プリント

• 帰納的な命題の定義
  • 命題の各場合分けに名前をつけておく。
  • 例にある even は， nat 型のものを受け取って Prop 型のものを 返す関数と思える。
    また，前回の nengou などと対応させて考えると， even 0 や forall n : nat, ... は型と思える。
• 例えば goal に以下のような if 文が含まれていたとき，
      if le_gt_dec n x then ... else ...
  case le_gt_dec とすると，n <= x と n > x の場合に 分かれた 2 つの sub goal が作られる。
• 練習問題の問 6 は難。