今日のCoq 

(* ev_ev_even *)
Theorem ev_ev_even : forall n m,
 ev (n+ m) -> ev n -> ev m.
Proof.
 intros n m E1 E2.
 
 induction E2 as [|n' E'].
 Case "E2 = ev_O'".  simpl in E1. apply E1.
 Case "E2 = ev_SS n'".   simpl in E1.
    inversion E1 as [|p E1']. apply IHE' in E1'. apply E1'. 
Qed.

Lemma ev_plus_2times : forall n,
  ev (n + n).
Proof.
  intros n.
  induction n as [|n'].
  Case "n = 0".  simpl. apply ev_O.
  Case "n = S n'". simpl. rewrite plus_comm. simpl.
  apply ev_SS. apply IHn'.
Qed.


Theorem ev_plus_plus : forall n m p,
 ev (n + m) -> ev (n + p) -> ev (m + p).
Proof.
 intros n m p E.
 replace (n + p) with (p + n).
 apply ev_ev_even. (* これを思いつくことが出来ないのはなぜか？ *)
 replace (m + p) with (p + m).
 rewrite plus_assoc.
 replace (p + n + p) with (p + p + n).
 replace (p + p + n + m) with (p + p + (n + m)).
 apply ev_sum with (n:=(p + p)) (m:=(n + m)).
 apply ev_plus_2times. 
 apply E.
 apply plus_assoc.
 assert(H:p + n = n + p). apply plus_comm. rewrite H.
 assert(H2:n + (p + p) = n + p + p). apply plus_assoc.
 rewrite <- H2.
 apply plus_comm with (n:= (p + p)) (m:=n).
 apply plus_comm. apply plus_comm.
Qed.

直前に出て来た
Theorem ev_ev_even : forall n m, ev (n+ m) -> ev n -> ev m.
の適用所が分かってない。

答はカンニング。


分からなかったところはProp_J.vの後半に怒涛のように説明が出て来た。

  • ざっくり言うと、Coqにおける「型」は、「式の分類に使われる式」です。例えば、 bool, nat, list bool, list nat, nat→nat などは全て「型」です。
  • 命題とブール値は、一見とてもよく似ているように見えます。しかしこの二つは根本的に違うものです！
    • ブール値は、「計算の世界における値」です。 bool 型の式は全て、（自由変数を持っていない限り）必ず true か false のどちらかに簡約することができます。
    • 命題は「論理の世界にいおける型」です。これらは「証明可能（この型の式を書くことができる）」か、「証明不能（そのような式は存在しない）」かのいずれかです。従って「命題が true である」というような言い方は意味を持ちません。
  • A→B という型も ∀ x:A, B という型も、どちらも型 A から型 B への関数である、という点については同じです。この二つの唯一の違いは、後者の場合戻り値の型 B が引数 x を参照できるということです。
  • Type にしろ Prop にしろ、我々はその値を別の値に変換する関数を書くことができます。 また、関数はそれ自身が値です。 このことは、我々が、次のようなことが出来ることを意味しています。
    • 関数を引数にしたり、関数を戻り値にしたりする高階関数を書くこと。
    • 関数をコンストラクタに適用し、関数を保持したさらに複雑な値を作り出すこと。


まあとにかく何でも関数だということだ。