# Coq

See also:

- Type theory
- Proof theory
- HOTT
- Higher order unification

# Coq is Normal

Coq has all sorts of crazy stuff in it, but the core of it can be used as a normal-ish functional programming language.

See my Coq in Y Minutes tutorial

### Interesting commands

`Drop`

vernacular - srops you into an ocaml toplevel- Register
- [Primitive] - register an ocaml primitive

## Inductive Types

Inductive types are prolog

Eliminators and pattern matching

What should be primitive anyway?

## Coindcutive Types

## Reflection

You can use domain specific ADTs to describe a class of problems. You can use coq as an ordinary programming language

## What are Proofs

### match annotations

The `as`

annotation is a realtive of the ocaml `as`

annotation. It is a binding form.
Likewise for the `in`

annotation. This is a pattern matching annotation that binds pattern variables. The scope of the bindings is only over the return clause of the match.
These annotations bring the match closer or exactly equivalent to the “recursor” formulation of pattern matching. This is a higher order function that you give a function specify what to do in each case. In the dependent context, you also give it a return type function.

In any sense does this

# Kernel

## VM

There is a coq vm with a bytecode. The instructions are defined here

Is this bytecode interpreter described anywhere?

Cody suggests Benjamin Gregoire

Sometimes is feels like cody knows a lot https://cstheory.stackexchange.com/questions/18777/is-compiler-for-dependent-type-much-harder-than-an-intepreter leroy gergoire paper bytecode interpreter full reduction at full throttle

# Ocaml

There are plugin tutorials Coq is available as a library. coq-core. Note the Ocam API documentation https://coq.github.io/doc/

- coq-simple-io
- coqffi generates ffi boilerplate for ocaml functions

# Plugins

.mlg files huh? Those are weird I don’t know that any of this is documented except in these tutorials

coqpp is the tool that turns .mlg into .ml files

# misc

- coq-ceres coq sexp stuff
- QED does something serious.
- Surface coq is desugared
- match annnotations are
- Note that the judgement
`a : A, b : B, c : C |- f : F`

is sort of getting Coq to accept`Definition foo (a : A) (b : B) (c : C) : F := f.`

It sort of reorders the pieces and make you give a name to the whole judgement`foo`

. That’s an interesting way of looking at it anyway. Of course the more usual way is that`foo`

is a function definition.

Leroy and Appell caonical binary trees

## Iris

Higher order separation logic. Kind of modelling concurrent ML in Coq I think?

# Compcert

https://github.com/AbsInt/CompCert manual The long form compcert paper seems the most useful

An interpreter of C. It stops if it hits undefined behavior? That’s cool. This seems really useful even for a non verified version

C -> Clight -> C#minor -> Cminor -> CminoSel -> RTL -> LTL -> Linear 0> Mach

Individual folders for each architecture. Interesting.

- backend

autosubst VCFloat gappa flocq mathematical components coq platform

Verified software Toolchain higher order separation logic for C certigraph graph manipulation programs certigc verified garbage collector

# Coq hackthan 2022

https://github.com/coq/coq/tree/master/dev/doc https://github.com/coq/coq/wiki/DevelSetup coq devel setup

- dev helpful information and scripts
- kernel
- interp
- vernac - all sorts of files implementing vernacular commands fixpoint, indcutive, define search etc
- tactics - ocaml code implementing some built in tactics like auto, autorewrite,
- pretyping? Is this elaboration from surface syntax to kernel.
- plugins - some native plugins are implemented. Extraction, btauto. Possibly a good place to look if you want to implement your own plguin. ssr. ring. micromega, ltac, ltac2
- kernel. I’ll try to list these in a dependency order
- names.ml
- univ.ml
- sorts.ml
- constr.ml - internal syntax of terms. “constructions”
- native*.ml stuff related to native compilation to ocaml for normalization

- testuite
- ide - coq ide
- boot

types

- constr
- unsafe_judgement
- evar_map
- glob_constr

You can build coq using dune make -f Makefile.dune

https://github.com/ejgallego/coq/tree/simple_compiler

stm

parse resolution of names interpret type inferrance

compiler/scoq.c vernac com* are implementationso f that vernac vernacexpr.ml vernac as VerancExtend constructor is where extension points hook in

using serapi to probe coq ast camlp5 mlg files. you can find them in _build vernacentires - interpeter out of vernac vernacextend.mli a typed dsl for vernac vernax_interp vernac_state declare.mli

Wehen you do a lemma Proof_info interp/Constrintern first step of elbation

interp/constrr_expr is surface syntax of coq terms. pretyping/glob_contr globalized /internalized term name resolution applied pretyping.mli type inferrence pretyping/understand_tcc is an important entry point?

evar_map

gramlib?

pretypinggggggggg evarconv.mli what is this?

libraries coq_checklib bool clib config coqpp top printer engine 0 actual proof engine gramlib interp kernel lib library parsing parsing pretypng printing parsing proofs legacy sysinti tactics tactics vernac

engine is 2 compoenents in one. pconstr e

https://github.com/ejgallego/coq-serapi/blob/v8.13/FAQ.md#how-many-asts-does-coq-have

## dune

make problmatic

couple of pointers

- build systems a la carte
- podcast about build systems by andrey

language agnostic language secpfic rules in dunesrc dep.mli memo.mli - memo is important huh. Build monad src/dune_rules

- scan all stanzas
- build virtual view of file system
- setup rule
- build a target

(coq.theory

)

- we detect dune file with (coq.theory
- extract generated files
- setup rules, informrm the build enginer about what
*net targets*are in scope

# Examples

```
Compute 1 + 1.
```

Equality eliminator is rewriting.

```
```

# Resources

talia ringer thesis really good explanations

Modular pre-processing for automated reasoning in dependent type theory processing for smtcoq The pro-PER meaning of “proper”