Some of my ramblings in
The Coq Proof Assistant
. For works about imperative programming go
here
.
coqdoc
A little theorem for gauss
reduced
bidimensional
lattice
over the l1-norm
Works over Z, using absolute values and inequalities.
coqdoc
Proof of |{n:a<=n<=b}|=b-a+1
Beginning to work with ensembles.
coqdoc
Ensembles:
bijection, apply function to ensemble, bijective_eqcardinal, reductions of a set by a function (aka summatory)
compile as .vo for next to use it.
coqdoc
Graphs:
definition, (un)directed, neighborhood, isomorphism, outdegree, outregular, vertex-transitivity, inverse and compostion of isomorphisms are isomorphisms, stronglyconnected, lemmas on paths and lists
compile as .vo. Uses EnsembleFacts.vo.
coqdoc
Zfacts:
Some things about integers
compile as .vo.
coqdoc
Zmod:
definition of Z/nZ as Type, some easy theorems
compile as .vo. Uses Zfacts.vo and EnsembleFacts.vo. It defines some Axioms :S.
coqdoc
Circulant:
definition of the circulant graphs, a=-a->undirected, vertexsymmetric
Uses graphs.vo and Zmod.vo. It is directly defined, without using CayleyGraph.
coqdoc
Groups:
definition of group, abelian group, unicity of inverses, left/right simplify, left/right addition are bijections, some algebraic manipulations
compile as .vo. Uses EnsembleFacts.vo.
coqdoc
CayleyGraphs:
definition of CayleyGraph, left addition are automorphism, vertex-transitivity, group inversion is automorphism, my IWONT10 result of when an Abelian Cayley graph lacks of nontrivial 4-cycles all graph automophisms f(0)=0 are group automorphisms (f(v+w)=f(v)+f(w))
Uses graphs.vo and Groups.vo.
coqdoc
Rings:
Definition of Ring and some algebra.
coqdoc
types:
Loads types_base and JMeqmaptype. Adds some basic properties.
coqdoc
types_base:
Fundamental properties and tactics. Choice with Type instead of Set.
coqdoc
JMeqmaptype:
Creates a identity between equal types. Extensive use of the axiom JMeq_eq, note this axiom is deducible from the unicity of equality proofs (or more generally from proof_irrelevance or classical logic). Solves problems for dependent types. JMeq is denoted ==.
coqdoc
Range:
Properties of {k|k<=u} and similar. Includes a proof without axioms of {k|k<=m}={k|k<=n}->m=n
coqdoc
Array:
array A n is the type of the lists over A of length n. (a++b)++c==a++(b++c). Constructions to make arrays from functions, and so, to work everything by index.
coqdoc
Vector:
Arithmetic over Arrays. ScalarProduct, UnitVector, summatory.
coqdoc
Matrix:
Loads Matrix_base and Matrix_arith.
coqdoc
Matrix_base:
Basic operations over rectangular arrays. Appendings, Transposition, Matrix from function.
coqdoc
Matrix_arith:
Arithmetic over matrices. MatrixProduct is Associative.
coqdoc
ListFacts:
Some additional results about List. List of the consecutive pairs of another list. Rotations.
coqdoc
Network:
A graph with queues in the edges. I proof that the bubble routing works over Networks with a Hamiltonian cycle.
coqdoc
Turing:
A first try for defining complexity classes in Coq. I define deterministic Turing machines with one tape over any alphabet. I define the class P.
coqdoc
godel:
Defining GĂ¶del formulas over Coq itself. You only end obtaining that Prop is a lot larger than nat.
coqdoc
Chaos: Period 3 implies chaos.
coqdoc