Schedule/ProofCafe_22
- 07/28 Schedule/ProofCafe_22
- 時間: 14:30 - 17:30
- 場所: 名古屋大学 理学部1号館(多元数理科学棟)3階307教室
- 参加登録: PARTAKE: 第22回 ProofCafe
- ソフトウェアの基礎の命題と論拠のはじめから
- ドキュメントはCoqソースコードから自動生成されています。ソースコード全体はこちら: http://proofcafe.org/sf/sfja.tar.gz
- 参加者: 10人
特別講演
今日はGarrigue先生の研究留学生の研究に関する講演をお願いしました。
- タイトル: “Proving the Soundness of OCaml’s relaxed value restriction in Coq”
- 講演者: Thomas Leventis
#ソフトウェアの基礎
練習問題: ★, optional (okd_before2_valid)
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)
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’)
[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)
練習問題: ★ (tree)
Inductive tree (X:Type) : Type :=
| leaf : X -> tree X
| node : tree X -> tree X -> tree X.
(* ==>
tree_ind : forall (X : Type) (P : tree X -> Prop),
(forall x : X, P (leaf x)) -> (* c1 *)
(forall t1 : tree X, P t1 -> (forall t2 : tree X, P t2 -> P (node t1 t2))) -> (* c2 *)
(forall t : tree X, P t).
*)
(* 補足説明：
1行め、全体がX:Typeでパラメータ化される。(forall X)
2行め、leafコンストラクタの場合。 (* c1 *)
3行め、nodeコンストラクタの場合。引数二つを受け取る。(t1 と t2) (* c2 *)
4行め、2行め3行めがみたされたt:tree Xは、P tを満たす。
*)