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.
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) → ¬ (t≤s).
Definition 𝕲e (e : 𝐄 X) := List.map 𝕲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 m ⇒ l ≲ 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 g ⇒ existsb
(@weak_graph_infb
(@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.
¬ (e ≤ f) → ∃ t, t ∈ (𝐄_to_𝐓s e) ∧ ∀ s, s ∈ (𝐄_to_𝐓s f) → ¬ (t≤s).
Definition 𝕲e (e : 𝐄 X) := List.map 𝕲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 m ⇒ l ≲ 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 g ⇒ existsb
(@weak_graph_infb
(@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.