A. Flat CPO Definition task := forall (x y : option nat) (n : nat), x = Some n -> x = y \/ x = None -> x = y. x = y \/ x = None について場合分けするのが簡単です。x = y の場合は自明で、x = None の場合はもう一つの仮定 x = Some n と合わせると…

A. Swap Twice Definition swap (t : nat * nat) := match t with (a, b) => (b, a) end. Definition task := forall t, swap (swap t) = t. 組を左右を入れ替える関数 swap が定義されていて、それを二回やると元に戻ることを示せという問題です。 t が必ず…

https://atcoder.jp/contests/asprocon5 に参加しました。第4回同様焼き鈍しじゃないことをしたいなーと思いながら考えたんですが、結局焼き鈍しをしました。でも焼き鈍し部分にはまだだいぶ改善の余地がありそうな状態だったので（具体的にどこに改善の余地…