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