Library LangAlg.expr_terms

This module is devoted to the reductions between expressions and terms.

Set Implicit Arguments.

Require Export terms expr.
Open Scope expr_scope.
Open Scope term_scope.
Section s.

Definitions

  Variable X : Set.
  Variable dec_X : decidable_set X.

Translation of a term as an expression.
  Fixpoint 𝐓_to_𝐄 (t : 𝐓 X) : 𝐄 X :=
    match t with
    | 1 ⇒ 1%expr
    | 𝐓_var a ⇒ 𝐄_var a
    | 𝐓_cvar a ⇒ 𝐄_var a°%expr
    | u ⋅ v ⇒ (𝐓_to_𝐄 u ⋅ 𝐓_to_𝐄 v)%expr
    | u ∩ v ⇒ (𝐓_to_𝐄 u ∩ 𝐓_to_𝐄 v)%expr
    end.

Translation of an expression into a term. Note that this function only makes sense for expressions that are already terms according to is_term (that is expressions that avoid + and 0, and where mirror can only be applied to variables).
  Fixpoint 𝐄_to_𝐓 (e : 𝐄 X) : 𝐓 X:=
    match e with
    | 1%expr ⇒ 1
    | 𝐄_var a ⇒ 𝐓_var a
    | 𝐄_var a°%expr ⇒ 𝐓_cvar a
    | (e ⋅ f)%expr ⇒ (𝐄_to_𝐓 e)⋅(𝐄_to_𝐓 f)
    | (e ∩ f)%expr ⇒ (𝐄_to_𝐓 e)∩(𝐄_to_𝐓 f)
    | _ ⇒ 1
    end.

We transform an expression into a list of terms by first combing it (thus producing a list of term-like expressions), and then translating each of those expressions into terms.
  Definition 𝐄_to_𝐓s e := map 𝐄_to_𝐓 (comb e true).

Given two lists of terms l and m, we write l≤m when every term in l is axiomatically smaller than some term in m.
  Global Instance 𝐓s_inf : Smaller (list (𝐓 X)) :=
    fun l m ⇒ (∀ u, u ∈ l → ∃ v, v ∈ m ∧ u ≤ v).

We write l≡m when both l≤m and m≤l hold.
  Global Instance 𝐓s_eq : Equiv (list (𝐓 X)) :=
    fun l m ⇒ l ≤ m ∧ m ≤ l.

Results

Translating a term as an expression and then translating back does not change the term.
  Lemma 𝐓_to_𝐄_to_𝐓 t : t = 𝐄_to_𝐓 (𝐓_to_𝐄 t).

The other direction also holds for term-like expressions.
  Lemma 𝐄_to_𝐓_to_𝐄 e : is_term e = true → e = 𝐓_to_𝐄 (𝐄_to_𝐓 e).

𝐓_to_𝐄 is monotone.
  Lemma 𝐓_to_𝐄_inf u v : u ≤ v → 𝐓_to_𝐄 u ≤ 𝐓_to_𝐄 v.

The following lemma is critical to relate the contents of comb e true and comb e false.
  Lemma 𝐄_to_𝐓_comb e d :
    ∀ u, u ∈ map 𝐄_to_𝐓 (comb e d) →
         ∃ v, v ∈ map 𝐄_to_𝐓 (comb e (negb d)) ∧ u = v °.

We now prove that for every axiom of the algebra of expressions, the images by 𝐄_to_𝐓s of the left and right side are equivalent. Although the proof is quite routine, it involves a large case analysis, due partly to the number of axioms we have given for expressions, and partly because of the combinatorial nature of the equivalence of lists of terms.
  Lemma ax_𝐄_to_𝐓s_incl e f :
    ax e f → (𝐄_to_𝐓s e) ≡ (𝐄_to_𝐓s f).
    Ltac unravel :=
        (simpl in *;
         match goal with
         | h : 𝐄_to_𝐓 _ = ?x |- _ ⇒ rewrite <- h in *;clear x h
         | h : _ = ?x |- _ ⇒ rewrite <- h in *;clear x h
         | |- _ ∧ _ ⇒ split
         | |- _ ∨ False ⇒ left
         | |- False ∨ _ ⇒ right
         | |- _ ∈ _ ⇒ eassumption
         | |- _ = _ ⇒ reflexivity
         end).

With the previous lemma, it is quite easy to show that 𝐄_to_𝐓s is monotone.
  Lemma 𝐄_to_𝐓s_inf e f : e ≤ f → (𝐄_to_𝐓s e) ≤ (𝐄_to_𝐓s f).

𝐄_to_𝐓s is in fact order preserving.
  Theorem 𝐄_to_𝐓s_inf_iff e f : e ≤ f ↔ (𝐄_to_𝐓s e) ≤ (𝐄_to_𝐓s f).
End s.

The function 𝐓_to_𝐄 is language preserving.
Lemma 𝐓_to_𝐄_lang X (t : 𝐓 X) Σ (σ : 𝕬[X→Σ]) :
  ⟦t⟧σ ≃ ⟦𝐓_to_𝐄 t⟧σ.

Combining this fact with the soundness result we have for expressions and the monotonicity of 𝐓_to_𝐄 we get the soundness of the axiomatization of terms.
Corollary 𝐓_inf_incl_lang (X : Set) {D: decidable_set X} (e f : 𝐓 X) :
  e ≤ f → e ≲ f.

Lemma 𝐄_to_𝐓_lang (X : Set) e :
  is_term e = true → ∀ Σ (σ:𝕬[X→Σ]), ⟦e⟧σ ≃ ⟦𝐄_to_𝐓 e⟧σ.

Lemma 𝐄_to_𝐓s_lang (X : Set) {D: decidable_set X} e :
  ∀ Σ (σ:𝕬[X→Σ]) w, w ⋵ (⟦e⟧σ) ↔ ∃ t, t ∈ (𝐄_to_𝐓s e) ∧ w ⋵ (⟦t⟧σ).

Close Scope term_scope.
Close Scope expr_scope.