7月
25
第101回 ProofCafe
名古屋Coq勉強会
| 募集内容 |
申し込み不要、もしくは当サイト以外で申し込み |
|---|---|
| 開催日時 |
2020/07/25(土) 13:30 ～ 16:30
|
| 募集期間 |
2020/06/27(土) 17:14
〜 |
| 会場 |
オンライン skype オンライン skype マップで見る |
イベントの説明
萩原、アフェルト 著 「Coq/SSReflect/MathCompによる定理証明」森北出版 の4章を読んでいきます。
資料は改訂していますから、申し訳ありまあせんが、再度ダウンロードしなおしてください。
4.4 seq.v
演習問題 リストの最初の要素以外を取り出す関数 tail を次のように定義します。空リストなら空を返すとします。
Definition tail (T : Type) (s : seq T) : seq T :=
match s with
| _ :: b => b
| [::] => [::]
end.
このとき、リストのサイズが減っていくこと size (tail s) < size s を証明してください。
リストの最後の要素以外を取り出す関数 init を定義した場合、同様に証明できるでしょうか。
以上、ちょっと引っ掛け問題です。
フィード
2020/07/18 15:12
2020/07/11 22:43
2020/07/11 22:43
2020/06/27 17:14
第101回 ProofCafe を公開しました！
morita_hm
SUHARA Hiromichi
エンジニアをつなぐ
connpass は株式会社ビープラウドが開発・運営しています