# 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.

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.

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.

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.

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.

The other direction also holds for term-like expressions.

𝐓_to_𝐄 is monotone.

Lemma 𝐄_to_𝐓_comb e d :

∀ u, u ∈ map 𝐄_to_𝐓 (comb e d) →

∃ v, v ∈ map 𝐄_to_𝐓 (comb e (negb d)) ∧ u = v °.

∀ 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).

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.

𝐄_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.

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.