文件列表:

.prettierignore (8, 2023-12-19)
.prettierrc (86, 2023-12-19)
Codeforces/ (0, 2023-12-19)
Codeforces/contests/ (0, 2023-12-19)
Codeforces/contests/1154/ (0, 2023-12-19)
Codeforces/contests/1154/A/ (0, 2023-12-19)
Codeforces/contests/1154/A/description.md (794, 2023-12-19)
Codeforces/contests/1154/A/restore_three_numbers.v (5230, 2023-12-19)
Codeforces/contests/4/ (0, 2023-12-19)
Codeforces/contests/4/A/ (0, 2023-12-19)
Codeforces/contests/4/A/description.md (1567, 2023-12-19)
Codeforces/contests/4/A/watermelon.v (2692, 2023-12-19)
LICENSE (1211, 2023-12-19)
_CoqProject (726, 2023-12-19)
compiler/ (0, 2023-12-19)
compiler/acorn.d.ts (510, 2023-12-19)
compiler/assert.ts (163, 2023-12-19)
compiler/babel.config.js (132, 2023-12-19)
compiler/cli.ts (4596, 2023-12-19)
compiler/combinedError.d.ts (181, 2023-12-19)
compiler/consumeNever.ts (50, 2023-12-19)
compiler/coqCodegen.ts (21613, 2023-12-19)
compiler/cppCodegen.test.js (3520, 2023-12-19)
compiler/cppCodegen.ts (17618, 2023-12-19)
compiler/exampleCode.ts (1771, 2023-12-19)
compiler/isOneByte.ts (129, 2023-12-19)
compiler/isPure.ts (1378, 2023-12-19)
compiler/jest.config.ts (135, 2023-12-19)
compiler/package-lock.json (203440, 2023-12-19)
compiler/package.json (403, 2023-12-19)
compiler/parse.test.js (17405, 2023-12-19)
compiler/parse.ts (28961, 2023-12-19)
compiler/parseExample.ts (1490, 2023-12-19)
compiler/printCoqCode.ts (145, 2023-12-19)
... ...

**You can't bluff a computer.** This is a repository of formally verified competitive programming code. Formal verification is very important. https://codeforces.com/blog/entry/111737 The problemsetters of this round accidentally [made an NP-complete problem](https://web.archive.org/web/20230125221257/https://codeforces.com/contest/1780/problem/C), and wrote a wrong greedy solution for it. The testers of this round guessed the same incorrect solution. The mistake was not caught during the review and testing phase. In the actual round, many folks also guessed the same incorrect solution. But a few smart folks proved the problem was NP-complete. The problemsetters even wrote [an incorrect proof](https://codeforces.com/blog/entry/111737?#comment-996084) for the greedy solution. Community members said the proof doesn't make sense. This mistake could have been avoided entirely if the folks responsible for the round had used formal verification. I'm learning it. Will you join me? Dependencies: Only `coq-stdpp`. Note: Whenever you create a new file, remember to import `Options` with the `From CoqCP Require Import Options.` command. Coq will then error if you apply a tactic when multiple goals are visible. Documentation: - [Internal imperative language](docs/InternalImperativeLanguage.md)

---

- [Regular bracket strings](docs/RegularBracketString.md) - [Selection sort](docs/SelectionSort.md) - [Repeat and compare](docs/RepeatCompare.md) Tasks: - [Sorting subarrays](docs/SortingSubarrays.md) **Why contribute?** As a contributor, your contributions - **Benefit you personally:** - You have a solid framework to reason about and solve competitive programming problems. - Your performance in programming contests leapfrogs significantly. - As an early adopter of formal verification, you have a competitive advantage in the labor market once formal verification gains widespread traction. - **Benefit society at large:** - As more competitive programming techniques get documented through formal verification, this eases the learning curve for people interested in competitive programming. - Your contributions reduce the reliance on online judges for the verification of program correctness. Test cases on online judges can be not very stringent. Auxiliary programs facilitating the judging process can be wrong. But a formal proof is a sure guarantee of a program's correctness. - Contests become fairer as model solutions and auxiliary judging programs can be formally verified, thus reducing room for deadly errors in the contest preparation stage. - Your contributions will draw more attention to formal verification and aid its widespread adoption.

近期下载者：

相关文件：

评论：[我要评论] [举报此文件]

收藏者：