# Combinatorics on Words Formalized in Isabelle/HOL

This repository contains the formalization of basics of Combinatorics on Words in [Isabelle/HOL](https://isabelle.in.tum.de/).
Note that this is a **work in progress** and future versions may change.
The main motivation for this project is that tedious and repetitive proofs are no exception in Combinatorics on Words, reappearing in many works.
It is desirable to outsource these tasks to a computer. 
Moreover, we hope that systematic use of proof assitants may evetually bring about new results in problems where the main obstacle is an excessive complexity of the proof.

Mature parts are to be part of [Archive of Formal Proofs](https://www.isa-afp.org/).

[[_TOC_]]

## Requirements

Compatible with [Isabelle2021](https://isabelle.in.tum.de/).

The following entries from the [Archive of Formal Proofs](https://www.isa-afp.org/) are used and needed to run some of the theories (currently Lyndon/Lyndon_Addition.thy ):
1. [Szpilrajn](https://www.isa-afp.org/entries/Szpilrajn.html) (used in [Borders_Addition.thy](#borders_additionthy))

See [using the AFP](https://www.isa-afp.org/using.html).

## Documentation

<!-- See the [automatically generated Isabelle document for the latest version.](/../-/jobs/artifacts/master/raw/document.pdf?job=build) -->
TBA.

## Usage

There are 3 ways how to use the presented code:
1. [download the current 'draft' version](/../-/jobs/artifacts/master/download?job=build-draft), unzip it and simply opening any *.thy file in the Isabelle/HOL editor (see below for a short guide)
1. use the mature content via the [Archive of Formal Proofs](https://www.isa-afp.org/using.html) (**to be available soon**)
1. clone this repository and point Isabelle to its ROOTS file (analogously is in [using the AFP](https://www.isa-afp.org/using.html))

<!--
Add this folder path to your Isabelle ROOTS file (`.isabelle/Isabelle20XX/ROOTS` on Mac/Linux/cygwin installations):

On Windows, add the folder as TODO
-->

### A short guide for Isabelle/HOL beginners - How to formalize your Combinatorics on Words result

Isabelle comes with editor included in the package downloadable from [Isabelle homepage](https://isabelle.in.tum.de/).
The easiest way to explore our formalization is to [download the current 'draft' version](/../-/jobs/artifacts/master/download?job=build-draft).

Once downloaded and unzipped, a good starting point is ExampleBasic.thy.
It contains comments aimed at Isabelle beginners and introduces a few concepts of our formalization.
You can try to write your lemma and the end of this example file.

The Isabelle's documentation is available directly in the editor, in the Documentation tab next to the File browser tab.
The basic tutorial is prog-prove: Programming and Proving in Isabelle/HOL.

We'd be happy if you use our formalization of Combinatorics on Words foundations to formalize your results.
Besides the very basic concepts in Basics/CoWBasic.thy, such as prefixes, factors, quotients, powers, roots etc., we already cover and plan to cover more elementary concepts.
For instance, we have the Periodicity lemma, the Graph lemma, the Lyndon-Schützenberger theorem (in directory Basics) and Lyndon words (in directory Lyndon), ready to be used.
See [code organization](#code) for a list of what is formalized and where.
Your results can be built up on our formalization, it suffices to base your theory on ours ( = include the required thy files).

## Suggestions etc.

We are open to suggestions and opinions!


## <a name="code"></a> Code organization and formalized facts/results

### Basics

#### CoWBasic.thy

1. Essential definitions and notation: concatenation, empty word, nonempty element of, prefix, suffix, left and right quotient, longest common prefix, factor, length
1. Equidivisibility properties
1. Total morphisms, reversed morphism
1. Conjugation
1. Root
1. Commutation of 2 words
1. Period root and numeric period
1. Border, shortest border, relation to period
1. Primitive word and primitive root
1. Various auxiliary facts

#### Submonoids.thy

1. Hull
1. Factorization into generators
1. Basis
1. Code
1. Free hull

#### PeriodicityLemma.thy

1. Relaxed version of periodicity lemma
1. Periodicity lemma (also known as the Fine and Wilf theorem)
1. Optimality of the Periodicity lemma (construction of the Fine-and-Wilf-word)

#### LyndonSchutzenberger.thy

1. Lyndon-Schützenberger theorem

### Graph_Lemma

#### GraphLemma.thy

1. Graph lemma
1. Application: two noncommuting words form a code

### Lyndon

#### Lyndon.thy

1. Lyndon words, their properties and characterization
1. Longest Lyndon suffix
1. Lyndon factorization

### Lyndon_Addition.thy

1. Smallest relation guaranteeing lexicographical minimality of a given word (in its conjugacy class)

[Archive of Formal Proofs](https://www.isa-afp.org/) entry [Szpilrajn](https://www.isa-afp.org/entries/Szpilrajn.html) is required in this theory.


### Equations (**work in progress**)

#### Overlaps.thy

1. Overlapping powers
1. Factor interpretation

<!--
#### Equations.thy
-->

## Article versions and references

The code, or its previous versions, was mentioned and used in the following publications:

Š. Holub, Š. Starosta: [Binary Intersection Formalized](https://doi.org/10.1016/j.tcs.2021.03.002), Theoret. Comput. Sci. 866, pp. 14-24, 2021, archived in the branch [Binary-Intersection-Formalized](../../tree/Binary-Intersection-Formalized)

## Tentative roadmap

### 2021

 1. AFP entries
 1. Textbook
 1. Results extending the Lyndon-Schützenberger theorem
 1. Results on binary equality words

## Avatar
The avatar of the repository features a [painting](http://words2005.lacim.uqam.ca/english/AfficheA.html) by [Michel Mendès-France](https://fr.wikipedia.org/wiki/Michel_Mend%C3%A8s_France). Courtesy of [Srecko Brlek](http://lacim-membre.uqam.ca/~brlek/).