## Library RelationAlgebra.common

## Library RelationAlgebra.comparisons

- comparisons: types equiped with a comparison function
- Specifying Boolean
- Specifying ternary comparisons
- Structure for types equiped with a Boolean equality and a comparison function.
- Natural numbers as a cmpType
- Booleans as a cmpType
- Pairs of cmpTypes
- Sums of cmpTypes
- Lists of a cmpType

## Library RelationAlgebra.positives

## Library RelationAlgebra.ordinal

- ordinal: finite ordinals, sets of finite ordinals
- Boolean strict order on natural numbers
- Additional induction schemes for natural numbers
- Ordinals
- Finite sets of ordinals as ordinals

## Library RelationAlgebra.denum

## Library RelationAlgebra.pair

## Library RelationAlgebra.powerfix

## Library RelationAlgebra.level

- level: tuples of Booleans identifying a point in the algebraic hierarchy
- Level constraints
- Merging levels
- Tactics for level constraints resolution
- Concrete levels

## Library RelationAlgebra.lattice

- lattice: from preorders to Boolean lattices
- Lattice operations
- Lattice laws (axioms)
- Properties of the preorder (≦) and it kernel (≡)
- Basic properties of ⊔, ⊓, bot, and top
- Subtyping / weakening
- Solving (in)equations in non distributive lattices
- Reasoning by duality
- (⊔,bot) forms a commutative, idempotent monoid
- (⊓,top) forms a commutative, idempotent monoid (by duality)
- Properties of negation
- Morphisms
- Pointwise extension of a structure

## Library RelationAlgebra.monoid

- monoid: typed structures, from ordered monoids to residuated Kleene allegories
- Monoid operations
- Monoid laws (axioms)
- Basic properties
- Subtyping / weakening
- Reasoning by duality
- Functors (i.e., monoid morphisms)

## Library RelationAlgebra.kleene

## Library RelationAlgebra.factors

## Library RelationAlgebra.kat

## Library RelationAlgebra.rewriting

## Library RelationAlgebra.move

## Library RelationAlgebra.lsyntax

- lsyntax: syntactic model for flat structures (lattice operations)
- Free syntactic model
- (In)equality of syntactic expressions.
- Comparing expressions

## Library RelationAlgebra.syntax

- syntax: syntactic model for types structures (monoid operations)
- Free syntactic model
- (In)equality of syntactic expressions.
- Testing for particular constants
- weakening (in)equations
- comparing expressions syntactically
- Packages for typed reification

## Library RelationAlgebra.normalisation

- normalisation: generic normalisation procedure and associated tactics
- normalisation procedure
- partial decision procedure for expressions containment <==
- Associated tactics

## Library RelationAlgebra.prop

## Library RelationAlgebra.boolean

- boolean: Booleans as a lattice, and as a monoid
- Booleans as a lattice
- Boolean as a (flat) monoid
- properties of the ofbool injection

## Library RelationAlgebra.rel

- rel: the main model of heterogeneous binary relations
- Relations as a (bounded, distributive) lattice
- Relations as a residuated Kleene allegory
- Relations as a Kleene algebra with tests
- Functional relations

## Library RelationAlgebra.srel

- srel: heterogeneous binary relations between setoids
- setoid-preserving relations as a lattice
- setoid-preserving relations as a Kleene category
- setoid-preserving relations as a Kleene category with tests

## Library RelationAlgebra.lang

- lang: the (flat) model of languages of finite words
- Languages as a lattice
- Languages a residuated Kleene lattice
- Language derivatives

## Library RelationAlgebra.lset

- lset: finite sets represented as lists
- semi-lattice of finite sets as simple lists
- sorted lists without duplicates

## Library RelationAlgebra.sups

## Library RelationAlgebra.sums

## Library RelationAlgebra.matrix

- matrix: constructing matrices over the various typed structures
- (n,m)-matrices as a lattice
- (n,m)-matrices as a monoid
- Exported matrix construction

## Library RelationAlgebra.matrix_ext

- matrix_ext: additional properties of matrices
- mx_scal is an homomorphism
- scal_mx preserves inclusions/equalities
- extracting components of block matrices
- Kleene star of a block matrix
- induction schemes for proving properties of the Kleene star of a matrix
- pointwise extension of a funcion to matrices
- `functional' matrices, with exactly one z per line, and 0 everywhere else

## Library RelationAlgebra.untyping

- untyping: untyping theorem for typed structures
- Cleaning terms
- Untyping theorem for bottom-free structures
- Extension to structures with bottom element, by factorisation

## Library RelationAlgebra.regex

- regex: the (flat) model of regular expressions
- Regular expressions form a Kleene algebra
- Predicates on regular expressions: 01, simple, pure
- Coalgebraic structure of regular expressions
- Language interpretation of regular expressions

## Library RelationAlgebra.rmx

- rmx: matrices of regular expressions
- Set of variables occurring in a matrix
- Pointwise extension of epsilon to matrices
- Pointwise extension of derivatives to matrices
- Pointwise predicates and operations on matrices
- From 01 row matrices to sets of ordinals, and back

## Library RelationAlgebra.bmx

## Library RelationAlgebra.dfa

- dfa: Deterministic Finite Automata, decidability of language inclusion
- DFA and associated language
- Reduction of DFA language inclusion to DFA language emptiness
- Decidability of DFA language emptiness
- Decidability of DFA language inclusion

## Library RelationAlgebra.nfa

- nfa: Non-deterministic Finite Automata
- Matricial (non deterministic) finite automata
- Language of a NFA
- Injection of DFA into NFA

## Library RelationAlgebra.ka_completeness

- ka_completeness: completeness of Kleene algebra
- 1. constructing eNFA out of regular expressions (Thompson)
- 2. removing espilon-transitions
- 3. determinisation
- Kleene theorem as a corollary
- 4. algebraic correctness of language inclusion checking for DFA
- Completeness of KA
- Decidability of KA

## Library RelationAlgebra.atoms

- atoms: atoms of the free Boolean lattice over a finite set
- Decomposition of the top element into atoms
- Decomposition of the other expressions into atoms
- Atoms are pairwise disjoint

## Library RelationAlgebra.traces

- traces: the model of finite traces
- Untyped traces
- Untyped traces a residuated Kleene lattice
- Typed traces

## Library RelationAlgebra.glang

## Library RelationAlgebra.gregex

- gregex: generalised typed regular expressions, for KAT
- Generalised regular expressions
- Interpretation into an arbitrary Kleene algebra with tests
- generalised regular expressions form a model of KAT
- Interpretation in the guarded strings model

## Library RelationAlgebra.kat_completeness

- kat_completeness: completeness of Kleene algebra with tests
- 1. Definition of the hat function, and correctness
- Relationship between generalised regular expressions and (plain) regular expressions
- From guarded string languages to languages on the extended alphabet
- 2. G (hat e) = R (hat e)
- KAT completeness
- KAT decidability

## Library RelationAlgebra.ugregex

- ugregex: untyped generalised regular expressions
- Syntax
- Language
- Coalgebraic characterisation of the language recognised by an expression
- Comparing expressions

## Library RelationAlgebra.ugregex_dec

- ugregex_dec: simple decision procedure for untyped generalised regular expressions
- Partial derivatives
- Main loop for the on-the-fly bisimulation algorithm
- Correctness of the main loop
- Final algorithm, correctness

## Library RelationAlgebra.kat_untyping

## Library RelationAlgebra.kat_reification

- kat_reification: various definitions to ease the KAT reification process
- Dependently types positive maps
- Syntax of KAT reification
- Interpretation of KAT reified expressions
- Predicate variables of a KAT expression
- From reified KAT expressions to gregex

## Library RelationAlgebra.kat_tac

- kat_tac: decision tactics for KA, KAT, and KAT with Hoare hypotheses
- corollary of kat_untyping and kat_completeness:
- kat tactic, for Kleene algebra with tests
- ka tactic, for Kleene algebra
- hkat tactic, for KAT with Hoare hypotheses

## Library RelationAlgebra.relalg

## Library RelationAlgebra.all

## Library compiler_opts

## Library imp

- imp: a formalisation of the IMP programming language on top of KAT
- Definition of the languague
- Big step semantics
- Some program equivalences
- Reasoning about assignations
- Embedding Hoare logic for partial correctness

## Library paterson

- paterson: Equivalence of two flowchart schemes, due to Paterson
- Memory model
- Arithmetic and Boolean expressions
- Programs
- Bigstep semantics
- Laws of schematic KAT
- Garbage-collecting assignments to unread variables
- Paterson's equivalence

## Library RelationAlgebra.fhrel

## Library RelationAlgebra.rewriting_aac

This page has been generated by coqdoc