Library RelationAlgebra.common

• common: basic modules, utilities, and tactics

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

• positives: basic facts about binary positive numbers

Library RelationAlgebra.ordinal

• ordinal: finite ordinals, sets of finite ordinals
• Boolean strict order on natural numbers
• Additional induction schemes for natural numbers
• Ordinals
  • ordinals as a cmpType
  • basic properties
  • sequence of all ordinals below n
  • shifting ans splitting ordinals
• Finite sets of ordinals as ordinals
  • on natural numbers
  • encapsulation into ordinals
  • additional lemmas

Library RelationAlgebra.denum

• denum: retracting various countable types into positives
• Sums
• Pairs
• Natural numbers
• Ordinals

Library RelationAlgebra.pair

• pair: encoding pairs of ordinals as ordinals

Library RelationAlgebra.powerfix

• powerfix: bounded fixpoint operator

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
  • Basic properties of the converse operation
  • Basic properties of composition
  • Basic properties of left division
  • Schroeder rules
  • Basic properties of Kleene star
• Subtyping / weakening
• Reasoning by duality
• Functors (i.e., monoid morphisms)

Library RelationAlgebra.kleene

• properties of Kleene star
• counterparts for strict iteration
• converse and iteration commute

Library RelationAlgebra.factors

• factors: additional properties of left and right factors

Library RelationAlgebra.kat

• KAT operations
• KAT laws
• Basic properties of KAT
• dual KAT, for duality reasoning

Library RelationAlgebra.rewriting

• rewriting: additional rewriting support
• rewriting modulo associativity of dot

Library RelationAlgebra.move

• move: simple tactics allowing to move subterms inside products

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
  • normalising sums
  • normalising intersections
  • normalising products
  • normalising converses
  • removing toplevel iterations in an iterated sum
  • global normalisation function
• partial decision procedure for expressions containment <==
• Associated tactics
  • ra: solve goals by normalisation.
  • ra_normalise/simpl: normalise the current goal

Library RelationAlgebra.prop

• prop: Propositions (Prop) as a bounded distributive lattice

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 operations
  • languages form 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

• sups: finite joins (or supremums), a la ssreflect
• Supremums
  • basic facts about sup
  • swapping and reindexing indices
  • notations
  • additional properties
• Infimum (or intersections)

Library RelationAlgebra.sums

• sums: finite sums, a la ssreflect

Library RelationAlgebra.matrix

• matrix: constructing matrices over the various typed structures
• (n,m)-matrices as a lattice
  • scalar (1,1)-matrices
  • block matrix operations
• (n,m)-matrices as a monoid
  • matrices form a BSL-monoid
  • properties of block matrix multiplication
  • matrices have a converse if the underlying monoid has one
  • matrices have a Kleene star if the underlying monoid has one
    • properties of the auxiliary mx_str_build functional
    • packing everything by induction to get properties of the
• 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
  • key lemma 1: equivalent expressions reduce to 0 simultaneously
  • key lemma 2: proofs with bottom elements can be factorised
• Untyping theorem for bottom-free structures
  • key lemma 3: injectivity of typing derivations
  • main lemma
• Extension to structures with bottom element, by factorisation

Library RelationAlgebra.regex

• regex: the (flat) model of regular expressions
• Regular expressions form a Kleene algebra
  • Operations
  • Laws
• Predicates on regular expressions: 01, simple, pure
• Coalgebraic structure of regular expressions
  • epsilon membership
  • derivatives
  • fundamental expansion theorem
  • monotonicity of epsilon
  • monotonicity of derivation
  • deriving and expanding 01 regular expressions
  • `pure part' of a regular expression
  • expanding simple regular expressions
  • epsilon, derivatives, and expansion of pure regular expressions
• Language interpretation of regular expressions
  • language of a regular expression, coalgebraically
  • lang is a KA morphism

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
  • 01 matrices
  • simple matrices
  • pure matrices
  • deriving and expanding various classes of matrices
• From 01 row matrices to sets of ordinals, and back

Library RelationAlgebra.bmx

• bmx: Boolean matrices, characterisation of reflexive transitive closure

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)
  • construction
  • correctness
• 2. removing espilon-transitions
  • construction
  • correctness
• 3. determinisation
  • construction
  • correctness
• 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 as a lattice
• Untyped traces a residuated Kleene lattice
  • traces operations
  • traces form a residuated Kleene lattice
  • untyped traces derivatives
  • particular elements
• Typed traces
  • packing typed traces as a residuated Kleene lattice
    • lattice structure
    • monoid structure
  • particular elements
  • properties of the embedding of untyped sets of traces into

Library RelationAlgebra.glang

• glang: the KAT model of guarded string languages
• Untyped model
• Typed model

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
  • externally guarded terms
  • inductive cases for the hat function
    • predicates
    • unit
    • letters
    • composition
    • Kleene star
  • summing up the constructions, by induction
• Relationship between generalised regular expressions and (plain) regular expressions
  • extended alphabet
  • regular expressions on the extended alphabet
  • o: gregex n m → expr3 n m
  • o': expr3 n m → gregex n m
  • expr3 -v→ regex -w→ uexpr3
• From guarded string languages to languages on the extended alphabet
• 2. G (hat e) = R (hat e)
  • properties of gl
  • clean terms: those on which G and R coincide
  • the basic ingredients of the hat function preserve cleaness
  • the hat function produces clean terms
• 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

• kat_untyping: untyping theorem for KAT

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

• relalg: standard relation algebra facts and definitions

Library RelationAlgebra.all

Library compiler_opts

• compiler_opts: certifying compiler optimisations
  • preliminary lemmas
  • 3.1 Deadcode elimination
  • 3.2 Common sub-expression elimination
  • 3.3 Copy propagation
  • 3.4 Loop Hoisting
  • 3.5 Induction variable elimination
  • (3.6 and 3.7 are void)
  • 3.8 Loop unrolling
  • 3.9 Redundant loads and stores
  • 3.10 Array bounds check elimination
  • 3.11 Introduction of sentinels

Library imp

• imp: a formalisation of the IMP programming language on top of KAT
• Definition of the languague
• Big step semantics
  • using KAT expressions in the model of relations
  • using an inductive predicate, as in standard textbooks
  • equivalence between the two definitions
• Some program equivalences
  • denesting nested loops
  • folding a loop
  • eliminating deadcode
• Reasoning about assignations
  • stacking assignations
  • removing duplicates
  • commuting assignations
  • delaying choices
• Embedding Hoare logic for partial correctness
  • correspondence w.r.t. the standard interpretation of Hoare triples
  • deriving Hoare logic rules using the hkat tactic

Library paterson

• paterson: Equivalence of two flowchart schemes, due to Paterson
• Memory model
• Arithmetic and Boolean expressions
  • evaluation of expressions
  • Free variables
  • Substitution
• Programs
• Bigstep semantics
  • variables read by a program
  • Additional notation
• Laws of schematic KAT
• Garbage-collecting assignments to unread variables
• Paterson's equivalence

Library RelationAlgebra.fhrel

• fhrel: The model of finite heterogeneous relations
  • Lattice Operations
  • Monoid Operations
  • KAT Operations
  • Cardinality

Library RelationAlgebra.rewriting_aac

• rewriting_aac: bridge with AAC_tactics