TopProver.md

TopProver Q&A

1. Q: 自動証明タクティックを使っても良いですか？ A: 標準ライブラリの範囲ならOKです

2. Q: Source code policy とは何ですか？ A: ユーザの提出コードを公開するか、非公開にするかの設定です。 (コンテスト中は Private に設定されていても、コンテスト終了後に Public になることがあります。)

3. Q: SSReflect 使いたいです A: Require Import ssreflect で使えます。MathComp 1.9.0 も最近入れました

4. Q: Pretest とは何ですか？ A: このジャッジシステムでは、作題者の認めていない公理 (Admitted してる、など) を coqchk を用いて利用しているのですが、 coqchk の実行には時間がかかるので、ジャッジを Pretest (coqc のビルドが通るかどうか) と System Test (coqchk によるチェック) の ２ 段階に分け、 Pretest を優先的に実行するようにしています。変なことをしていない限りは基本的に Pretest が通れば System Test も通ります。(具体的には、 Problem.v と Solution.v の Axiom の diff をチェックしています。 Problem.v で認めている公理は用いても OK です。)

5. Q: コンテストの日程がいつの間にか変わっているようです A: 競技プログラミングと参加者層が近いので、その時間帯に競技プログラミングのコンテスト (AtCoder, Codeforces 等) がある場合は、告知なく日程や開始時刻を変更する可能性があります。ご容赦くださいm(_ _)m。

6. Q: Ratingとは何ですか？ A: (TODO)

その他

• 最近ドメイン取りました: https://top-prover.top/#
• 作題者募集してます
• カレンダー
• 質問や要望等あれば連絡ください: https://twitter.com/asi1024
• 最近忙しくて次のコンテストを準備する余裕がないです。すみません。
  • 問題案を募集しています。出題者が現れ次第次のコンテストを開催します。

ここ最近の気持ち

• 計算量上限を証明する問題など出して競技プログラミングから参加者層を引き抜きたいなあと思っている
  • これ の 3.3 節とか使えそうかなあ、とちょっと思ってる
  • 定義を書いてみたけど結構重くなってしまったので、コンテストには不向きかもしれない

Coq のバージョンアップデートについて (2020/05/03)

• 2020/05/02 以前は Coq 8.9.1 を使用していたが、当該バージョンに False が証明できてしまうバグがあることが判明しました。
  • coq/coq#9294 (comment)
  • このバグは Coq 8.10 以降では修正されています。
• そこで、ジャッジに用いる Coq のバージョンを 8.11.1 にアップデートすることでこれに対応することにしました。
• それにともない、過去に出題された問題に対する提出についても、今後は 8.11.1 を用いてジャッジすることにします。
  • Coq のバージョン間の差異により、過去の提出コードの判定結果が変わることがありえます。
  • しかし、一部を除いて、過去の提出コードについてはリジャッジを行わないことにします。
    • 前述のバグを利用した提出 (#1488, #1499) については確認のためリジャッジを行いました。(kaz さん、ご報告ありがとうございます)

Coq 8.9.1, 8.11.1 のバージョン間の差異について

バージョン間での致命的な大差はないと思われますが、現状以下の差異を把握しています。

• 以前は Require Import Lia. しておくと auto with zarith で自動的に omega が使われていたのですが、Require Import ZArith. がないと使われなくなりました．
  • 内部的には、以前は Require Import Lia. しておくと zarith という名前の hint database に omega を自動的に使うヒントが追加されていたのが、Require Import ZArith. しないと追加されなくなったようです。 (kozima さん、ご報告ありがとうございます)