null

(大学院) 情報科学概論：第 3 回理解度確認テスト
付録 A
参照物不可。授業の理解度を測るのが目的であり、
本テストの配点は 0 点です。
参考
Inductive nat : Type :=
問 1. n が正の整数のとき、次の等式が成り立つこ
| O : nat
とを証明しなさい。
| S : nat → nat.
1 + 2 + 3 + ··· + n =
1
n(n + 1)
2
(1)
Fixpoint plus (n : nat) (m : nat) : nat :=
match n with
| O => m
| S n’ => S (plus n’ m)
end.
Notation "x + y" :=
(plus x y)
(at level 50, left associativity)
: nat_scope.
問 2. 次の定理に非形式的証明を与えなさい。nat
や + の定義は付録を参考にして下さい。
Theorem plus_0_r : ∀ n:nat,
n + 0 = n.
1

Download Report