A Rocq library written by members of PnV Discord Server.

• Currently, this library is standalone.

git clone https://github.com/PnVDiscord/PnVRocqLib.git
cd PnVRocqLib
eval `opam env`
rocq makefile -f _CoqProject -o CoqMakefile
make -f CoqMakefile -j

The Rocq Prover, version 9.1.0
compiled with OCaml 5.3.0

Our main results are:

• The Kleene fixed-point theorem. (Theorem lfp_returns_the_least_fixed_point in ClassicalDomainTheory.v)

• The weak completeness of propositional logic. (Corollary weak_completeness in PropositionalLogic.v)

• The soundness, completeness, and compactness theorems of propositional logic. (Theorem the_propositional_soundness_theorem, Theorem the_propositional_completeness_theorem, and Corollary the_propositional_compactness_theorem in ClassicalPropositionalLogic.v)

• The soundness and countable completeness theorems of first-order logic. (Theorem HilbertCalculus_sound and Theorem HilbertCalculus_countable_complete in ClassicalFol.v)

• The weak normalisation property of STLC. (Corollary Normalisation_by_Evaluation) in STLC.v

• The Bourbaki-Witt fixed-point theorem and the geneneralised Kleene fixed-point theorem (Theorem BourbakiWittFixedpointTheorem and Theorem generalised_Kleene_fixedpoint_theorem) in ClassicalSetTheory.v

• Category.v : Basic theory on category.

• Monad.v : Basic definitions about monad.

• Aczel.v : Aczel's type theoretic interpretation of set theory.

• Graph.v : Basic graph theory.

• ITree.v : Basic Definitions on interaction tree.

• NumRepr.v : Number Representation.

• Vector.v : Replaces Stdlib.Vectors.VectorDef.t.

• FlowerAxioms.v : Axioms for the sublibrary Flower.

• FlowerPrelude.v : The prelude of the sublibrary Flower.

• Index.v : Accumulates all source files and check their consistency.

• BasicFol.v : Basic definitions of First-Order Logic.

• BasicFol2.v : Extra definitions of First-Order Logic.

• ClassicalFol.v : The meta-theory on Classical First-Order Logic--such as Soundness Theorem and Completeness Theorem.

• ClassicalPropositionalLogic.v : The Soundness, Completeness, and Compactness Theorem for PropositionalLogic.

• ExtraFol.v : Extra def/thm about First-Order Logic.

• HilbertFol.v : Basic facts about Hilbert calculus for First-Order Logic.

• HilbertFol2.v : Advanced facts about Hilbert calculus for First-Order Logic.

• MuRec.v : Basic facts about μ-recursive functions.

• PrimRec.v : Basic facts about primitive recursive functions.

• PropositionalLogic.v : Contructive meta-theory on the Propositional Logic, Weak Completeness Theorem for PropoistionalLogic.

• BooleanAlgebra.v : Basic theory on Boolean algebras.

• ClassicalDomainTheory.v : Classical domain theory.

• ClassicalSetTheory.v : Classical set theory.

• DomainTheory.v : Constructive domain theory.

• OrderTheory.v : Basic order theory.

• SetTheory.v : Constructive set theory.

• ThN.v : Basic facts about the natural numbers.

• ClassicalFacts.v : Facts about CIC + (classic : forall P, P \/ ~ P).

• ConstructiveFacts.v : Facts about CIC.

• Notations.v : Reserves all notations to avoid the conflict.

• SfLib.v : A copy of snu-sf/sflib.v.

• Prelude.v : The prelude.

• BasicITreeTh.v : A basic theory on interaction trees.

• FolFramework.v : A First-Order Logic Framework.

• Lambda1.v : Basic definitions for Church-style stlc.

• P.v : Provides a function nat -> option string by base 36.

• Regex.v : A theory on regular expression.

• STLC.v : Basic theorems for Church-style stlc.

1. sflib
2. stdpp
3. DmxLarchey/Murec_Extraction
4. CoqGym/goedel
5. ernius/formalmetatheory-stoughton
6. uds-psl/Constructive Analysis of First-Order Completeness
7. snu-sf/Ordinal
8. Damhiya/Logos
9. Lean Zulip Chat (1)
10. DeepSpec/Interaction Trees

1. A note written by Jayadev Misra
2. Constructive Completeness Proofs and Delimited Control
3. A Mathematical Introduction to Logic
4. The Lambda Calculus: Its Syntax and Semantics
5. The Power of Parameterization in Coinductive Proof

• Soonwon Moon
• Hanul Jeon
• Clare Jang

1. Ordinal Numbers
2. IPO <=> pointed DCPO
3. Regular Language: Regex, ε-NFA, DFA, and Lexer Genrartor
4. LALR(1) CFG: Parser Generator
5. Gödel's Incompleteness Theorem