リストに関する証明でもinductionが使えるよという話。まずはリスト中に指定した数がいくつあるかを数えるcountという関数を定義。 Fixpoint count n l := match l with nil => 0 | a::tl => let r := count n tl in if beq_nat n a then 1 + r else r end.…

ex.1 addの定義は以下。 Fixpoint add n m := match n with 0 => m | S p => add p (S m) end.最初は下記のように書いた。 Lemma ex1' : forall n m, add n (S m) = S (add n m). Proof. induction n. intros m. simpl. reflexivity. rewrite IHn. reflexivi…

4.2 タイトルの"Stronger Statements"ってのはより厳密な命題って感じですかね？命題で使われている関数がいくつかのパターンマッチで定義されている場合は、成立すべき初期段階が複数必要ですよという話でいいのかな。例で使われるのはevenb。定義は以下 Fi…

4章は自然数を扱った証明でよく使われるtacticの紹介。 4.1 まずはinductionというtactic。こいつは数学的帰納法ってやつですね。 sum_nは2章で定義していて、 Fixpoint sum_n n := match n with 0 => 0 | S p => p + sum_n p end.ということで数学的帰納法…

ということでexerciseをやってみた。 ex.1 まずは定石に従い、introsすると 1 subgoal A : Prop B : Prop C : Prop H : A /\ B /\ C ============================ A /\ BHをさらに分割するためにdestructを適用。 1 subgoal A : Prop B : Prop C : Prop H1 …

3.3.2 rewrite 次はrewriteというtactic。 式変形だと思えばよいかな。左辺を式変形して右辺と同形になることを示すというわけ。 まずは分配法則を適用してみる。分配法則を表す定理は何かを探すのにはSearchRewriteというコマンドが使える。 SearchRewrite …

3.3 引き続き、いろんなtacticの例。 演算子/\に対して左辺と右辺に分割を行う場合は、3.2で出てきたように destruct H as [H1 H2]という形でdestuctというtacticを適用したけど、\/に対しては destruct H as [H1 | H1]と分割後の仮定を表すシンボルの間に|…

読んだ本の数：12冊 読んだページ数：2782ページバカとテストと召喚獣 (1) (角川コミックス・エース 256-1)読了日：10月04日 著者：夢唄,まったくモー助バカとテストと召喚獣 (2) (角川コミックス・エース 256-2)読了日：10月04日 著者：夢唄,まったくモー助…