# Preorder on theories.

We say that P,A is smaller than Q,B if for every pair e,f of expressions satisfying P we can find a pair e',f' such that :
• both e' and f' satisfy Q and
• A e f if and only if B e' f'.
Definition included_th (S1 S2 : TyEq) : Prop :=
let (P,A) := S1 in
let (Q,B) := S2 in
e f, P e P f
e' f', Q e' Q f'
(A e f B e' f').
Infix "<<" := included_th (at level 60).
Definition equiv_th S T := (included_th S T)/\(included_th T S).
Infix "≡≡" := equiv_th (at level 60).

Global Instance included_th_PreOrder : PreOrder included_th.
Instance equiv_th_Equivalence : Equivalence equiv_th.

If the theory (P,A) is smaller than (Q,B), and if the equivalence relation B __ is decidable for elements satifying Q, then the equivalence relation A __ is decidable for elements satifying P.
Lemma included_th_decidable :
P A Q B,
(P,A) << (Q,B)
( e f, Q e Q f Decidable.decidable (B e f))
e f, P e P f Decidable.decidable (A e f).

This notion will be instrumental in proving orderings. φ is a transfer morphism between relation P with axioms A to relation Q with axioms B if for every pair e,f related by P, the pair φ e f is related by Q and A e f if and only if B φ e φ f.
Definition transfer_fun (R1 R2 : relation expr × relation expr) φ : Prop :=
let (P,A):= R1 in
let (Q,B):= R2 in
e f, P e f
Q (φ e) (φ f)
(A e f B (φ e) (φ f)).
Notation " φ ⊩ R → S " := (transfer_fun R S φ) (at level 50).

We may use this to define a stronger preorder on theories.
Definition is_model (T1 T2 : TyEq) :=
let (P,A):= T1 in let (Q,B):= T2 in
φ, φ (P^2,A) (Q^2,B).
Infix "⊲" := is_model (at level 60).

Existence of such a morphism is a also a preorder.
This preorder is stronger. Indeed it is straightforward to show that if there is a transfer morphism from P^2 with axioms A to Q^2 with axioms B then P,A is smaller than Q,B.

## Technical lemmas about transfer morphisms.

Global Instance transfer_fun_proper_str_impl :
Proper (Basics.flip (@stronger expr) ==> (@eq_rel expr)
==> (@stronger expr) ==> (@eq_rel expr)
==> Logic.eq
==> Basics.impl)
(fun P A Q Btransfer_fun (P,A) (Q,B)).
Global Instance transfer_fun_proper_eq_impl :
Proper ((@eq_rel expr) ==> (@eq_rel expr)
==> (@eq_rel expr) ==> (@eq_rel expr)
==> Logic.eq
==> Basics.impl)
(fun P A Q Btransfer_fun (P,A) (Q,B)).
Global Instance transfer_fun_proper_eq_impl_rev :
Proper ((@eq_rel expr) ==> (@eq_rel expr)
==> (@eq_rel expr) ==> (@eq_rel expr)
==> Logic.eq
==> Basics.flip Basics.impl)
(fun P A Q Btransfer_fun (P,A) (Q,B)).
Global Instance transfer_fun_proper_iff :
Proper ((@eq_rel expr) ==> (@eq_rel expr) ==> (@eq_rel expr) ==>
(@eq_rel expr) ==> Logic.eq ==> iff)
(fun P A Q Btransfer_fun (P,A) (Q,B)).
Global Instance transfer_fun_proper_iff_1 A Q B φ :
Proper ((@eq_rel expr) ==> Basics.flip Basics.impl)
(fun Pφ (P,A) (Q,B)).
Global Instance transfer_fun_proper_iff_2 P A B φ :
Proper ((@eq_rel expr) ==>Basics.flip Basics.impl)
(fun Qφ (P,A) (Q,B)).
Lemma TTrue_unit_l a A b B φ :
(φ (a,A) (b,B)) φ (TTruea,A) (b,B).
Lemma TTrue_unit_r a A b B φ :
(φ (a,A) (b,B)) φ (a,A) (TTrueb,B).
Lemma incl_p_fun (p q : relation expr) φ P A Q B :
(φ (P,A) (Q,B))
( x y, (pP) x y q (φ x) (φ y))
(φ (pP,A) (qQ,B)).
Lemma incl_p_fun_r (q : relation expr) φ P A Q B :
(φ (P,A) (Q,B))
( x y, P x y q (φ x) (φ y))
(φ (P,A) (qQ,B)).
Lemma incl_p_fun_l (p : relation expr) φ P A Q B :
(φ (P,A) (Q,B)) φ (pP,A) (Q,B).
Lemma augm_transfer (p : predicate expr) φ P A Q B :
(φ (P,A) (Q,B))
( x, p x p (φ x))
(φ (p^2P,A) (p^2Q,B)).
Lemma augm_transfer' (p : predicate expr) φ A B :
(φ (TTrue,A) (TTrue,B))
( x, p x p (φ x))
(φ (p^2,A) (p^2,B)).
Lemma augm_transfer2 (p : predicate expr) φ P A Q B :
(φ (P,A) (Q,B))
( x, p (φ x))
(φ (P,A) (p^2Q,B)).

Lemma technical e0 f0 (p q : exprProp) (a b r s : relation expr) φ :
(φ (r,a) (s,b))
( e f, r e f ¬ p e ¬ p f ¬ (a ef))
¬ (b e0 f0) q e0 q f0
( e f, s e f q ^2 e f (e == f) ¬ (b ef))
(p,a) << (q,b).
Lemma pos_rev_rm0 {A B a} :
(rm0 (a,A) (a,B)) rm0 (poa,B) (poa,A).
Lemma str_pos_rev_rm0 {A B a} :
(rm0 (a,A) (a,B))
rm0 (spa,B) (spa,A).
Lemma po_to_str_rm0 r a s b :
(rm0 (r^2,a) (po∧(s^2),b))
( e, r e ¬ r e)
(( e, s e untyped e)
( A e f, b e f A e A f))
( e f, b e f str_positive e str_positive f)
( e f, ¬ (b e f) (str_positives)^2 e f)
(r,a) << (str_positives,b).

# Order between theories.

## Expressions without explicit permutations.

For untyped and typed expressions, zero may be eliminated.
Typed and untyped expressions are equivalent.

## For positive expressions, it is equivalent to have

explicit and applied permutations.

## Expression with explicit permutations over atoms.

Zero may be eliminated both in the untyped and typed setting.
Typed and untyped expressions are equivalent.

## Expressions over letters (with explicit permutations).

In this theory zero may be eliminated as well.
Typed and untyped versions of the theory are also equivalent.