- 07/28 [Schedule/ProofCafe_22]()
- 時間: 14:30 - 17:30
- 場所: [名古屋大学 理学部1号館(多元数理科学棟)3階307教室]()
- 参加登録: [PARTAKE: 第22回 ProofCafe](http://partake.in/events/84bed6f1-cf07-46da-8776-c79e5b2542ad)
- [ソフトウェアの基礎](http://proofcafe.org/sf/)の[命題と論拠](http://proofcafe.org/sf/Prop_J.html)のはじめから
- ドキュメントはCoqソースコードから自動生成されています。ソースコード全体はこちら: http://proofcafe.org/sf/sfja.tar.gz
- 参加者: 10人

# 特別講演
今日はGarrigue先生の研究留学生の研究に関する講演をお願いしました。

- タイトル: "Proving the Soundness of OCaml's relaxed value restriction in Coq"
- 講演者: Thomas Leventis

参加者の記録: http://researchmap.jp/jovgcx4wj-49935/#_49935

#ソフトウェアの基礎

## 練習問題: ★, optional (okd_before2_valid)
~~~ { .v }
Theorem okd_before2_valid : okd_before2.
Proof.
unfold okd_before2.
intros.
apply okd_before with d2.
apply okd_before with d3.
apply H. apply H1. apply H0.
Qed.  
Print okd_before2_valid.
~~~

## 練習問題: ★, optional (okd_before2_valid_defn)
~~~ { .v }
Print okd_before2_valid.

okd_before2_valid = 
fun (d1 d2 d3 : day) (H : ok_day d3) (H0 : day_before d2 d1)
  (H1 : day_before d3 d2) => okd_before d1 d2 (okd_before d2 d3 H H1) H0
     : okd_before2
~~~


## 練習問題: ★★  (plus_one_r')
~~~ { .v }
[induction] タクティックを使わずに、下記の証明を完成させなさい。

Theorem plus_one_r' : forall n:nat,
  n + 1 = S n.
Proof.
Print plus.
apply nat_ind.
reflexivity.
intros.
change (S (n + 1) = S (S n)).
rewrite H.
reflexivity.
Qed.
~~~

## 練習問題: ★ (ExSet) 
~~~ { .v }
Inductive ExSet : Type :=
 |con1 : bool -> ExSet
 |con2 : nat -> ExSet -> ExSet
.
~~~

参加者の記録：http://researchmap.jp/joyfww4t0-49935/#_49935