- 09/22 [Schedule/ProofCafe_23]()
- 時間: 14:30 - 17:30
- 場所: [名古屋大学 理学部1号館(多元数理科学棟)3階307教室](http://www.math.nagoya-u.ac.jp/ja/direction/campus.html)
- 参加登録: [PARTAKE: 第23回 ProofCafe](http://partake.in/events/02b814af-4272-44e6-b7a3-68cbeb0ebb48)
- [ソフトウェアの基礎](http://proofcafe.org/sf/)の[命題と論拠](http://proofcafe.org/sf/Prop_J.html)の「帰納法の仮定」から
- ドキュメントはCoqソースコードから自動生成されています。ソースコード全体はこちら: [http://proofcafe.org/sf/sfja.tar.gz]()
- 参加者 6人

## 練習問題:  ★★ (ev_plus4)
~~~ { .v }
Definition ev_plus4 : forall n, ev n -> ev (4 + n) :=
  fun n : nat => fun H : ev n => (ev_SS (S (S n)) (ev_SS n H)).

Theorem ev_plus4' : forall n,
  ev n -> ev (4 + n).
Proof.
  intros.
  simpl.
  apply ev_SS.                              (* Goal : ev SSSSn *)
  apply ev_SS.                              (* Goal : ev SSn *)
  apply H.                                  (* Goal : n *)
Qed.
~~~

## 練習問題:  ★★★ (ev_ev_even)
~~~ { .v }
Theorem ev_ev_even : forall n m,
  ev (n+m) -> ev n -> ev m.
Proof.
  intros n m H1 H2.
  induction H2.
  apply H1.

  apply IHev.
  simpl in H1.  
  SearchAbout ev.
  apply SSev_even.
  apply H1.
Qed.
~~~