Schedule/ProofCafe_23

練習問題: ★★ (ev_plus4)
練習問題: ★★★ (ev_ev_even)

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

練習問題: ★★ (ev_plus4)

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)

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.