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
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