coq

# Coq and Rocq `Admitted` compiles, and so does a theorem about the wrong proposition. The kernel checks the proof; you check that the statement is the claim, that no assumption was smuggled in, and that the compiled library passes an independent check. Coq 8.x commands and the Rocq 9 `rocq` subcommands are both given; use the pair the installed version provides. ## Project 1. `_CoqProject` lists the logical mapping and the files: `-Q theories MyLib` (or `-R` for recursive legacy mapping), optional `-arg -w -arg -notation-overridden`, then one `.v` path per line. Generate the Makefile with `coq_makefile -f _CoqProject -o Makefile` (Rocq 9: `rocq makefile -f _CoqProject -o Makefile`) and build with `make`. A single file compiles with `coqc -Q theories MyLib theories/File.v` (`rocq compile`). Dune projects use a `(coq.theory (name MyLib))` stanza instead. 2. Install and pin through opam (`opam install coq.8.20.0` or `rocq-prover`), and record the version with `coqc --version` (`rocq --version`). Library packages such as `coq-mathcomp-ssreflect` or `coq-stdpp` change tactic vocabulary; note which are used. 3. Interactive checking: VsCoq or coq-lsp in the editor, `coqtop` (`rocq repl`) for quick experiments. Never trust a proof that was only stepped through interactively; compile the file. ## Statement fidelity 4. Run `Check`, `About`, `Print` and `Locate` on every notation and definition the statement uses. Traps: `nat` subtraction truncates, `/` and `mod` on `nat` and `Z` follow different rounding conventions, `Prop` versus `bool` (`=` versus `=?`, bridged by `reflect`), implicit coercions (`Print Coercions`, `Set Printing Coercions`), notations that hide arguments (`Set Printing All`). Real numbers in the standard library are axiomatized, so `Print Assumptions` on a real-analysis result lists their axioms. 5. Evaluate the statement on a concrete instance: `Compute`, `Eval compute in`, or an `Example` closed by `reflexivity`. Use `Fail` to assert that a wrong variant does not typecheck. Check hypotheses are satisfiable with a concrete witness. 6. Hypotheses belong in the theorem statement. `Axiom` and `Parameter` become genuine assumptions of everything downstream; section `Variable`s are discharged into premises when the section closes. State the claim as one closed theorem so a reader sees every premise. ## Search 7. `Search (_ + _ = _ + _).`, `Search "comm" in Nat.`, `Search plus minus.`, `SearchPattern (_ <= _ + _).`, `SearchRewrite (_ + 0).`; filters `inside` and `outside` restrict modules. `Locate "+"` resolves a notation to its definition. Load `Lia` for `lia` (linear integer arithmetic), `Lra` for `lra`, `Ring`, `Field`, `Nia`. 8. Tactic families: `lia`, `nia`, `lra`, `ring`, `field`, `congruence`, `auto` and `eauto` with hint databases, `firstorder`, `intuition`; ssreflect if MathComp is in use. Name introduced variables (`intros x y H`) rather than relying on generated names. ## Hygiene 9. `Qed` seals a proof as opaque, right for theorems. `Defined` keeps it transparent, needed only when other code must compute through it (definitions built by tactics, `Program`, dependent types). `Opaque` and `Transparent` adjust later; `Print Opaque Dependencies` and `Print Transparent Dependencies` show the consequences. A transparent lemma inside a computation can make `simpl` explode. 10. No `Admitted` and no `admit` in a finished development. Use bullets (`-`, `+`, `*`) or `{ }` for subgoals and `Set Default Goal Selector "!".` so a tactic that accidentally applies to several goals fails loudly. 11. Run the independent checker on the compiled library, `coqchk -Q theories MyLib` followed by the module name (`rocq check` in Rocq 9), with `-o` to print the assumptions it found. It re-verifies the `.vo` files without trusting the compiler's bookkeeping. ## Audit 12. `Print Assumptions my_theorem.` The answer `Closed under the global context` means no axioms and no admitted lemmas. Otherwise it lists each axiom (for example `functional_extensionality_dep`, `Classical_Prop.classic`, `proof_irrelevance`, `Eqdep.Eq_rect_eq.eq_rect_eq`, the real-number axioms) and every `Admitted` result the proof depends on. Quote the list verbatim and say which items are standard classical or extensionality axioms and which are unfinished proofs. 13. Deliver the sources, the `_CoqProject`, the exact build and `coqchk` commands with their output, the `Print Assumptions` output, and a clause-by-clause mapping from the informal claim to the formal statement. ## Checklist - [ ] `_CoqProject` and Makefile build cleanly from scratch; version recorded. - [ ] Every definition and notation in the statement inspected with `Print` or `Locate`. - [ ] Statement evaluated on a concrete instance; hypotheses shown satisfiable. - [ ] No `Admitted`, `admit`, stray `Axiom` or `Parameter`. - [ ] `Print Assumptions` and `coqchk` output recorded and explained. ## Sources - Rocq reference manual (commands, `Search`, `Print Assumptions`, `rocq makefile`): https://rocq-prover.org/doc/V9.0.0/refman/ - Coq 8.20 reference manual: https://coq.inria.fr/doc/V8.20.0/refman/ - Rocq standard library: https://rocq-prover.org/doc/V9.0.0/stdlib/ - Rocq Platform and opam packages: https://github.com/rocq-prover/platform - Software Foundations, Volume 1 (Logical Foundations): https://softwarefoundations.cis.upenn.edu/lf-current/ - Certified Programming with Dependent Types: http://adam.chlipala.net/cpdt/ - coq-lsp: https://github.com/ejgallego/coq-lsp