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.
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.
Theorem completeness_𝐓_equiv (u v : 𝐓 X) : u ≃ v ↔ u ≡ v.
We can then extend this result to expressions.