問38 Midpoint
https://top-prover.top/problem/38
Require Export Arith. Definition task := forall m n, S m < n -> m < (m + n) / 2 < n.
まず初めに、Search _ inside Lt. SearchAbout "div" inside Nat. などで使えそうな定理を探す。
Phase 1, div2
x / y は divmod という再帰的なアルゴリズムで定義されていて、この第3、第4引数があるため帰納法が使いにくい。
x / 2 は div2 に置き換えると解きやすい。
Phase 2, 2つ前を見る帰納法
div2 (2+n) = 1+(div2 n) を利用して数学的帰納法をしたいので2つ前のステップを見る帰納法をしたい。
つまり普通の帰納法が
P 0 /\ (forall n, P n -> P (1+n)).
を示すのに対して、
P 0 /\ P 1 /\ (forall n, P n -> P (2+n)).
を使いたい。これは (P n /\ P (1+n)) を示すようにすれば1つ前を見る通常の帰納法で解ける。
(P 0 /\ P 1) /\ (forall n, (P n /\ P (1+n)) -> (P (1+n) /\ P (2+n))).
Phase 3, 終わり
m, nをそれぞれ適切に置き換えるとゴールは、div2 (m+m) < div2 (m+n) < div2 (n+n) になる。
解 https://top-prover.top/submission/1256
疑問
- 他の人の解法見るとすごい短いが、どうやってライブラリの定理を探してるの
- Notation が Search コマンドで検索できなくて不便。具体的には lt_0_Sn, lt_n_Sn, lt_S など
- Coq.Arith.Lt は OBSOLETE と書いてある
