# About this repository

This repository contains a formalization in Coq of a technical Lemma to the
paper "Efficiently recognizing regular expressions with vectorization and
algebra" authored by :
- Charles Paperman
- Sylvain Salvati
- Claire Soyez-Martin


This formalization proves two things :

1. The equi-expressivity property of vectorial circuits that use as gates (+, ∨,
   ∧, ¬) and vectorial circuits that use (xu, ∨, ∧, ¬). The operator xu
   corresponds the operator 'next-until' of forward-LTL.

   More specifically we show that (⊕ denotes bitwise xor):

   1. x + y = x ⊕ y ⊕ ((x ∨ y) xu (x ∧ y))
   2. x xu y = (y + (y ∨ x)) ⊕ y ⊕ (y ∨ x).

   This gives us a method about how to use addition so as model logical
   properties in bit-vectors.

2. Lemma 1 of the paper also called 'Addition Lemma'. More specifically, this
   lemma builds upon the relation between the next-until operator and addition
   so as to relate the vectorial circuit (y + (y ∨ ¬z)) ∧ x with a logical
   property about its output v, mainly that if, for all positions i,

   x[i] = 1 ∨ y[i] = 1 ⇒ z[i] = 1

   then, for all positions i:

   v[i] = 1 iff x = 1 ∧ ∃ k. k < i ∧ y[k] = 1 ∧ ∀ j. k < j < i ⇒ z[j] = 0.


The motivation for us to write this formalization in coq is two-fold:

1. Avoid to have in the paper technical proofs that contain uninteresting
 details.
2. Give strong evidence that the presented properties are valid.