新機能 イベントメッセージの予約機能を追加しました。イベント主催者様は、参加者へのメッセージ送信を事前に予約できます。詳しくはこちらをご確認ください。

新機能 イベント詳細画面に「参加者への情報」欄を追加しました。イベント管理者、発表者、参加者(抽選中や補欠は除く)だけに表示されるフィールドです。詳しくはこちら

このエントリーをはてなブックマークに追加

Jul

25

第101回 ProofCafe

名古屋Coq勉強会

Registration info

Description

萩原、アフェルト 著 「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 を定義した場合、同様に証明できるでしょうか。

以上、ちょっと引っ掛け問題です。

Feed

SUHARA Hiromichi

SUHARA Hiromichiさんが資料をアップしました。

07/18/2020 15:12

SUHARA Hiromichi

SUHARA Hiromichiさんが資料をアップしました。

07/11/2020 22:43

SUHARA Hiromichi

SUHARA Hiromichiさんが資料をアップしました。

07/11/2020 22:43

SUHARA Hiromichi

SUHARA Hiromichi published 第101回 ProofCafe.

06/27/2020 17:14

第101回 ProofCafe を公開しました!

Group

ProofCafe

Number of events 47

Members 42

Ended

2020/07/25(Sat)

13:30
16:30

Registration Period
2020/06/27(Sat) 17:14 〜
2020/07/25(Sat) 16:30

Location

オンライン skype

オンライン skype