PnVRocqLib

A Coq library written by members of PnV Discord Server.

Currently, this library is standalone.

1. Quick Start

git clone https://github.com/PnVDiscord/PnVRocqLib.git
cd PnVRocqLib
eval `opam env`
coq_makefile -f _CoqProject -o Makefile
make -j4 -k

coqc -v

The Coq Proof Assistant, version 8.18.0

2. Contents

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 completeness theorems of first-order logic. (Theorem HilbertCalculus_sound and Theorem HilbertCalculus_complete in ClassicalFol.v)

Data

• Aczel.v : Aczel's Type Theoretic Interpretation of Set Theory.

• Graph.v : Basic Graph Theory.

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

Logic

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

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

• ClassicalFol.v : Meta-theories on Classical First-Order Logic--such as Soundness Theorem and Completeness Theorem.

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

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

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

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

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

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

Index

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

Math

• BooleanAlgebra.v : Basic theory on Boolean Algebras.

• ClassicalDomainTheory.v : Classical domain theory.

• DomainTheory.v : Constructive domain theory.

• OrderTheory.v : Basic order theory.

• Ordinal.v : Theory on ordinal numbers.

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

Prelude

• AC.v : Facts on CIC + Axiom of Choice.

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

• ConstructiveFacts.v : Facts on CIC.

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

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

• Prelude.v : The prelude code.

3. References

1. sflib

2. stdpp

3. A note written by Jayadev Misra

4. Constructive Completeness Proofs and Delimited Control

5. Murec_Extraction

6. CoqGym/goedel

7. formalmetatheory-stoughton

8. Constructive Analysis of First-Order Completeness