# Library LangAlg.to_lang_witness

In most this module, we establish the following lemma: for every series-parallel term u, there exists a word w and an interpretation ฯ such that for every other ๐๐ term v, the graph of v is larger than the graph of u if and only if w belongs to the ฯ-interpretation of v. This lemma will allow us to prove completeness of our axiomatization with respect to language interpretations.
In the second part of the module, we generalise the result to weak terms and primed weak terms.
In this module, we call a list of natural numbers a sequence is it of the form [a(0);a(1);...;a(n)] such that for every i<n, a(i)+1=a(i+1). Equivalently, they are those sequences produced using the function seq.

Set Implicit Arguments.

Require Export w_terms_graphs.
Require Import PeanoNat.
Section s.

# Main construction

Variable X : Set.
Variable dec_X : decidable_set X.
Let us fix a term u and a set of variables ๐ for this section.
Variable u : ๐๐ X.
Variable ๐ : list X.
We write the reachability relation in the graph of u as โค.
Notation " i โค j " := (i -[๐ฒ u]โ j) (at level 60).

To make some definitions easier, we define the function co_nth i l. This function returns the smallest index j such that the jth element of the list l is equal to i.
Fixpoint co_nth i l :=
match l with
| [] โ 0
| a::l โ
if i =? a
then 0
else S (co_nth i l)
end.

If i appears in the list l, then the element at index co_nth i l in the list l is equal to i.
Lemma co_nth_In i l :
i โ l โ nth (co_nth i l) l 0 = i.

If i is in l, this function returns an index smaller than the length of l.
The following simple observation follows easily from co_nth_In.
We will mainly apply this function on lists without duplicates. In such lists, the function is injective.
Lemma nth_NoDup {A} i j l (d1 d2 : A) :
NoDup l โ i < length l โ j < length l โ
nth i l d1 = nth j l d2 โ i = j.

In lists with no duplicates, we can prove the dual of lemma co_nth_In.
Lemma co_nth_nth i l :
NoDup l โ i < length l โ co_nth (nth i l 0) l = i.

Vert is a list containing exactly the vertices of the graph of u, without any duplication, and listed in increasing order.
Definition Vert :=
filter (fun i โ inb i (vertices u)) (seq 0 (S (ln u))).

Lemma Vert_NoDup : NoDup Vert.

Lemma Vert_vertices : Vert โ vertices u.

N is the number of vertices in the graph of u.
Definition N := length Vert.

The word w_u will be the witness we announced earlier. It is defined as the sequence of natural numbers from 0 to 2 ร N - 1.
Definition w_u := seq 0 (2*(N-1)).

The function ฮณ finds the index of a vertex in the list Vert. It provides us with a bijection between the vertices of u and the numbers from 0 to N-1.
ฮณ is order preserving.
Moreover, we know that the ordering of natural numbers contains the path ordering of vertices. Therefore using the previous lemma we get the following monotonicity property.
The following two observations are fairly self evident.
Lemma ฮณ0 : ฮณ 0 = 0.

Lemma N_non_zero : 1 < N.

The next few lemmas are simple observations on sequences and on the function co_nth.
Lemma seq_app i k l :
seq i (k+l) = seq i k ++ seq (i+k) l.

Lemma seq_last i l : seq i (S l) = seq i l ++ [i+l].

Lemma rev_seq n1 l1 n2 l2 : seq n1 l1 = rev (seq n2 l2)
โ l1 = l2 โง (n1 = n2 โง l1 = 1 โจ l1 = 0).

Lemma firstn_seq n m l :
m โค l โ firstn m (seq n l) = seq n m.

Lemma skipn_seq n m l :
m โค l โ skipn m (seq n l) = seq (n+m) (l-m).

Lemma co_nth_app_right i l m :
ยฌ i โ l โ i โ m โ co_nth i (l++m) = length l + co_nth i m.

Lemma co_nth_app_left i l m :
i โ l โ co_nth i (l++m) = co_nth i l.

These observations allow us to prove that the image of the output of the graph of u by ฮณ is N-1.
Lemma ฮณN : ฮณ (ln u) = N - 1.

ฯ i j is the sequence of numbers from 2*ฮณ i to 2*ฮณ j - 1.
Definition ฯ i j :=
seq (2 ร ฮณ i) (2 ร (ฮณ j - ฮณ i)).

In particular we can use ฯ to define w_u.
Lemma ฯ_word : w_u = ฯ 0 (ln u).

This lemma is almost tautological, but it turns out to come in handy several times.
We now define the witnessing interpretation. For every edge (i,a,j) in the graph of u, the word ฯ i j is in ฯ a. Furthermore, if a belongs to the set ๐, then the empty word is in ฯ a.
Definition ฯ : ๐ฌ[Xโnat] :=
fun a w โ
(a โ ๐ โง w = [])
โจ (โ i j, (i,a,j) โ (edges (๐ฒ u)) โง w = ฯ i j).

The only way for the empty word to appear in ฯ a is when a belongs to the set ๐.
A simple observation we can make is that for any letter a the length of any word in ฯ a is even. This can be neatly extended to the language of any series-parallel term according to ฯ.
This result mainly relies on the fact that the seq function is essentially bijective.
Lemma ฯ_seq n l i j :
seq n (S l) = ฯ i j โ 2 ร ฮณ j = S (n + l) โง 2 ร ฮณ i = n.

If a word in the ฯ-interpretation of some term v is a sequence, then it can be expressed as ฯ i j, for some vertices i,j such that iโคj.
For every pair of vertices iโคj, if ฯ i j belongs to the ฯ-interpretation of a sequential product v1โจพv2, then there exists a vertex k between i and j, such that ฯ i k belongs to the language of v1 and ฯ k j to that of v2. This lemma is critical in the proof of the main lemma to make the induction case for products go through.
By a simple induction on v, one can check that the empty word belongs to the language of v exactly if all of the variables in v belong to the set ๐.
To prove that from the fact that w_u is in the language โฆvโง ฯ we can build a morphism from v to u, we need to strengthen the statement slightly to make the induction work better. The statement that turns out to be sufficient is the following: if ฯ i j belongs to โฆvโง ฯ, then there is an internal premorphism from v to u that must in addition map 0 to i and ln v to j.
For the converse direction, we use the following lemma, also proved by induction on the term v.
With the two technical lemmas we just proved, the proof of the main result of this module becomes very simple.

# Weak terms

Nothing deep happens here, we just apply the results and constructions above to get a similar theorem.
Variable X : Set.
Variable dec_X : decidable_set X.

Definition word (u : ๐ X) :=
match u with
| (None,_) โ []
| (Some u,_) โ w_u u
end.

Definition ฯ' (u : ๐ X) : ๐ฌ[Xโnat] :=
match u with
| (None,A) โ fun a w โ a โ A โง w = []
| (Some u,A) โ ฯ u A
end.

Lemma ฯ'_nil u a : ฯ' u a [] โ a โ (snd u).

Lemma word_of_term_correct u v :
word u โต (โฆvโง(ฯ' u)) โ ๐ฒw u โฒ ๐ฒw v.

Corollary not_incl_witness u :
โ w (ฯ : ๐ฌ[Xโnat]), โ v, ๐ฒw u โฒ ๐ฒw v โ w โต (โฆvโงฯ).
End w.

Section t.

# Primed weak terms

For primed weak terms, another problem arises. Because of the way we have set up the translation form terms and expressions into weak terms, it is not sufficient to have a lemma of the shape
โ w (ฯ: ๐ฌ[X'โnat]), โ v : ๐', ๐ฒw (ฯ{u}) โฒ ๐ฒw (ฯ{v}) โ w โต โฆฯ{v}โงฯ.
We need our witnessing interpretation ฯ to arise as ฮ ฯ' for some ฯ' : ๐ฌ[Xโnat]. Thus we massage the construction we proved correct earlier, to put it into the appropriate shape.
Variable X : Set.
Variable dec_X : decidable_set X.
Hint Resolve dec_X' dec_X.

This is the witnessing interpretation. It works mostly like the one we built for series-parallel terms, but we make use of the boolean in the letters from the duplicated alphabet: if (i,a,j) is an edge, then ฯ i j is in the language ฯฮ (a,true), and its mirror image is in the language of ฯฮ (a,false).
First, we make some observations about ฯฮ.
When looking for sequences, we can relate ฮ ฯฮ and ฯ'.
Hence we can transfer the presence of a witness in โฆvโง(ฮ (ฯฮ u)) to the presence of the witness in the interpretation we set up for weak terms.
We now prove our witnessing lemma by putting together lemmas witness_ฮ and word_of_term_correct.