Library LangAlg.completeness

We finally arrive to the main result of this development: the proof that our axiomatization is complete for the equational theory of languages.

Set Implicit Arguments.

Require Export expr_graphs terms_graphs terms_w_terms to_lang_witness.

Section t.
  Variable X : Set.
  Variable dec_X : decidable_set X.

We begin by proving the axiomatization of terms complete. The proof uses the witness pair w associated with the term u, the equivalence between the weak graph preorder and axiomatic containment, and the fact that 𝐓_to_𝐖' is language preserving.
  Lemma 𝐓_incl_lang_inf (u v : 𝐓 X) : u v u v.

This allows us to check that we have sound and complete axiomatizations of both equality and containment for terms.
  Theorem completeness_𝐓_inf (u v : 𝐓 X) : u v u v.

  Theorem completeness_𝐓_equiv (u v : 𝐓 X) : u v u v.

We can then extend this result to expressions.
  Theorem completeness_𝐄_inf (e f : 𝐄 X) : e f e f.

  Theorem completeness_𝐄_equiv (e f : 𝐄 X) : e f e f.
End t.