TaPL24章のネタです。まずStatementがcoqで正しく書けているか怪しいですが… Theorem exists_forall_second: forall T: Prop -> Prop, ((exists X, T X) <-> (forall Y: Prop, (forall X, T X -> Y) -> Y)). intros. split. - intros. destruct H. now apply…

D - Halftree意外とこの解き方している人が少ないように見えたので。例えば入力が7 3の場合は (0,1)(1,2)(2,3) と辺を張れば0~6の線グラフが得られることが分かると思います。 9 3の場合は頂点7, 8が残ってしまいますが、(7,5)と辺を張ることで、線グラフ+α…