Library LangAlg.w_terms_graphs

This module is devoted to the translation of weak terms into graphs.

Set Implicit Arguments.

Require Export sp_terms_graphs w_terms.

Section s.
  Variable X : Set.
  Variable Λ : decidable_set X.

A weak graph is a pair of a graph and a set of tests.
  Definition weak_graph : Set := (graph nat X) × list X.

We define the graph of a weak term using the graph of its series-parallel term, or the point graph (0,[],0) in the case of the constant None.
  Definition 𝕲w (x : 𝐖 X) : weak_graph :=
    match x with
    | (Some u,A) ⇒ (𝕲 u,A)
    | (None,A) ⇒ ((0,[],0),A)
    end.

We extend the ordering of graphs to an ordering of weak graphs.
  Global Instance weak_graph_inf : SemSmaller weak_graph :=
    fun g h ⇒ snd h ⊆ snd g ∧ snd g ⊨ fst g ⊲ fst h.

This allows us to obtain the following theorem, equating the axiomatic containment of weak terms to the ordering of weak graphs.
  Theorem 𝐖_inf_is_weak_graph_inf : ∀ x y, x ≤ y ↔ 𝕲w x ≲ 𝕲w y.

We can test the ordering of weak graph using a boolean function.
  Definition weak_graph_infb (g h : weak_graph) :=
    forallb (fun n ⇒ existsb (eqX n) (snd g)) (snd h)
            && ex_is_morphismb NatNum NatNum _ (snd g) (fst h) (fst g).

  Lemma weak_graph_infb_correct g h :
    weak_graph_infb g h = true ↔ g ≲ h.
End s.