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)

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.
  Lemma co_nth_inj i j l :
    i โˆˆ l โ†’ j โˆˆ l โ†’ co_nth i l = co_nth j l โ†’ i = j.

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

  Definition ฯƒ' (u : ๐– X) : ๐•ฌ[Xโ†’nat] :=
    match u with
    | (None,A) โ‡’ fun a w โ‡’ a โˆˆ A โˆง w = []
    | (Some u,A) โ‡’ ฯƒ u A

  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).
  Definition ฯƒฮž (t:๐–') : ๐•ฌ[Xโ†’nat] :=
    fun a w โ‡’
      ((a,true) โˆˆ (snd (ฯ€{t})) โˆง w = [])
      โˆจ (โˆƒ u, fst (ฯ€{t}) = Some u
                    โˆง (โˆƒ i j,
                          ((i,(a,true),j) โˆˆ (edges (๐•ฒ u))
                            โˆง w = ฯ‰ u i j)
                           ((i,(a,false),j) โˆˆ (edges (๐•ฒ u))
                            โˆง w = rev (ฯ‰ u i j)))).

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.