Library LangAlg.expr_graphs

Stringing together the various translations we've defined so far, we may associate with every expression a set of weak graphs. This implies decidability of the axiomatic equivalence for expressions.
Set Implicit Arguments.

Require Export w_terms_graphs terms_graphs expr_terms.

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

Because the containment of terms is decidable, we have the following property.
  Lemma 𝐄_neq_𝐓s_neq (e f : 𝐄 X) :
    ¬ (e f) t, t (𝐄_to_𝐓s e) s, s (𝐄_to_𝐓s f) ¬ (ts).

  Definition 𝕲e (e : 𝐄 X) := 𝕲t (𝐄_to_𝐓s e).

  Global Instance graphs_smaller :
    SemSmaller (list (weak_graph (@X' X))) :=
    fun l m g, g l h, h m g h.

  Global Instance graphs_equiv : SemEquiv (list (weak_graph (@X' X))) :=
    fun l ml m m l.

  Theorem smaller_𝕲e e f : e f 𝕲e e 𝕲e f.

  Theorem equiv_𝕲e e f : e f 𝕲e e 𝕲e f.

  Definition graphs_smallerb l m :=
    forallb (fun gexistsb
                           (@X' X)
                           (@dec_X' _ dec_X) g) m) l.

  Lemma graphs_smallerb_correct l m :
    graphs_smallerb l m = true l m.

  Lemma graphs_equivb_correct l m :
    graphs_smallerb l m && graphs_smallerb m l = true l m.

  Corollary decidable_𝐄_inf (e f : 𝐄 X) : {e f} + {¬ (e f)}.

  Corollary decidable_𝐄_equiv (e f : 𝐄 X) : {e f} + {¬ (e f)}.

End s.