- Coq is Normal
- Type theory
- Proof theory
- 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
Cody’s intro to coq https://github.com/codyroux/broad-coq-tutorial
Inductive weekday := | monday | tuesday.
Dropvernacular - srops you into an ocaml toplevel
- Register making names accessible to ocaml
- [Primitive] - register an ocaml primitive
Showgives infromation during proof.
Show Proofshows intermediate stuff.
Search. Very important. Lots of features.
Inductive types are prolog
Eliminators and pattern matching
What should be primitive anyway?
You can use domain specific ADTs to describe a class of problems. You can use coq as an ordinary programming language
What are Proofs
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
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
There are plugin tutorials Coq is available as a library. coq-core. Note the Ocam API documentation https://coq.github.io/doc/
.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
Higher order separation logic. Kind of modelling concurrent ML in Coq I think?
SSReflect emphasizes proof by reflection. It is a really succinct inscrutable looking syntax.
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.
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
- 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
- constr.ml - internal syntax of terms. “constructions”
- native*.ml stuff related to native compilation to ocaml for normalization
- ide - coq ide
You can build coq using dune make -f Makefile.dune
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?
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
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
- we detect dune file with (coq.theory
- extract generated files
- setup rules, informrm the build enginer about what net targets are in scope
Compute 1 + 1.
Equality eliminator is rewriting.
https://github.com/dwarfmaster/commutative-diagrams tactic for categroy proofs
- 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 : Fis 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
foois a function definition.
autosubst VCFloat gappa flocq mathematical components coq platform