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.


  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

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

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 lm 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 lm when both lm and ml hold.
  Global Instance 𝐓s_eq : Equiv (list (𝐓 X)) :=
    fun l ml m m l.


Translating a term as an expression and then translating back does not change the term.
The other direction also holds for term-like expressions.
𝐓_to_𝐄 is monotone.
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
         | |- _ Falseleft
         | |- False _right
         | |- _ _eassumption
         | |- _ = _reflexivity

With the previous lemma, it is quite easy to show that 𝐄_to_𝐓s is monotone.
𝐄_to_𝐓s is in fact order preserving.
The function 𝐓_to_𝐄 is language preserving.
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.