問37 Zero test
https://top-prover.top/problem/37
Inductive iszero : nat -> Prop := | iszero_0 : iszero 0 | iszero_S : forall n, iszero (S n) -> iszero n. Definition task := forall n, iszero n <-> n = 0.
まだcoqに慣れないので翻訳すると、
- Inductive iszero 帰納法を定義したクラス、自然数natによって述語「iszero n」がインデックスされている
- iszero_0 述語「iszero 0」の根拠となるコンストラクタ
- iszero_S 述語「iszero n」の根拠は「iszero (S n)」であることを示すコンストラクタ
名前から察せられるがこのデータ型（集合）には iszero 0 しか存在しない、つまり iszero 0 しか証明できない。iszero 1の証明にはiszero 2が必要で、iszero 3, 4....が必要になる。この定義合法なのか。
右向き iszero n -> n=0 を示す。Inductive の型なのでとりあえず iszero nでinduction してみると、ベースケース iszero_0 は0=0で自明。帰納ステップは
1 subgoal n : nat H : iszero (S n) IHiszero : S n = 0 ______________________________________(1/1) n = 0
なぜか S n = 0 が得られる。なんだこれ。前提が矛盾しているので証明可能。
左向き iszero n <- n=0 はコンストラクタそのもので自明。解 https://top-prover.top/submission/1219
問39 Boolean-hole principle revisited
https://top-prover.top/problem/39
Definition task := (forall P Q R, (P <-> Q) \/ (Q <-> R) \/ (R <-> P)) -> forall P, P \/ ~ P.
Boolean-Holeを検索してもよくわからないけど鳩ノ巣原理のパロディ？時間内に解けなかったけど簡単だった。
~ P は P -> False と等価なので前提にPとFalseを入れたくなる。他に使える述語と言えば True しかない。
解 https://top-prover.top/submission/1244
