Library order

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.

Lemma transfer_fun_preorder : PreOrder is_model.

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.

Lemma transfer_fun_included_th t1 t2 : t1 ⊲ t2 → t1 << t2.

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 B ⇒ transfer_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 B ⇒ transfer_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 B ⇒ transfer_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 B ⇒ transfer_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 )) ↔ φ ⊩ (TTrue ∧a ,A ) → (b ,B ).
Lemma TTrue_unit_r a A b B φ :
  (φ ⊩ (a ,A ) → (b ,B )) ↔ φ ⊩ (a ,A ) → (TTrue ∧b ,B ).
Lemma incl_p_fun (p q : relation expr) φ P A Q B :
  (φ ⊩ (P ,A ) → (Q ,B )) →
  (∀ x y, (p ∧P) x y → q (φ x) (φ y)) →
  (φ ⊩ (p ∧P ,A ) → (q ∧Q ,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 ) → (q ∧Q ,B )).
Lemma incl_p_fun_l (p : relation expr) φ P A Q B :
  (φ ⊩ (P ,A ) → (Q ,B )) → φ ⊩ (p ∧P ,A ) → (Q ,B ).
Lemma augm_transfer (p : predicate expr) φ P A Q B :
  (φ ⊩ (P ,A ) → (Q ,B )) →
  (∀ x, p x → p (φ x)) →
  (φ ⊩ (p ^2 ∧P ,A ) → (p ^2 ∧Q ,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 ^2 ∧Q ,B )).

Lemma technical e0 f0 (p q : expr →Prop) (a b r s : relation expr) φ :
  (φ ⊩ (r ,a ) → (s ,b )) →
  (∀ e f, r e f ∨ ¬ p e ∨ ¬ p f ∨ ¬ (a ⊢ e ≡f )) →
  ¬ (b ⊢ e0 ≡ f0 ) → q e0 → q f0 →
  (∀ e f, s e f → q ^2 e f ∨ (e == f ) ∨ ¬ (b ⊢ e ≡f )) →
  (p ,a ) << (q ,b ).
Lemma pos_rev_rm0 {A B a} :
  (rm0 ⊩ (a ,A ) → (a ,B )) → rm0 ⊩ (po ∧a ,B ) → (po ∧a ,A ).
Lemma str_pos_rev_rm0 {A B a} :
  (rm0 ⊩ (a ,A ) → (a ,B )) →
  rm0 ⊩ (sp ∧a ,B ) → (sp ∧a ,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_positive ⊗s )^2 e f ) →
  (r ,a ) << (str_positive ⊗s ,b ).

Transfer morphisms.

Lemma NKA_NKA_p : rm0 ⊩ (np ∧ut ,NKA ) → (np ∧ut ,NKA_p ).
Lemma NKA_incl_NKA_p : rm0 ⊩ (np ∧ut ,NKA ) → (po ∧(np ∧ut ),NKA_p ).
Lemma NKA_incl_NKA_p_nm :
  rm0 ⊩ (mlt ∧(np ∧ut ),NKA ) → (mlt ∧(po ∧(np ∧ut )),NKA_p ).
Lemma NKA_incl_NKA_p_ns :
  rm0 ⊩ (sg ∧(np ∧ut ),NKA ) → (sg ∧(po ∧(np ∧ut )),NKA_p ).

Lemma NKA_p_incl_NKA : rm0 ⊩ (sp ∧(np ∧ut ),NKA_p ) → (np ∧ut ,NKA ).
Lemma NKA_p_incl_NKA_nm :
  rm0 ⊩ (mlt ∧(sp ∧(np ∧ut )),NKA_p ) → (mlt ∧(np ∧ut ),NKA ).
Lemma NKA_p_incl_NKA_ns :
  rm0 ⊩ (sg ∧(sp ∧(np ∧ut )),NKA_p ) → (sg ∧(np ∧ut ),NKA ).

Lemma NKA_t_NKA_tp : rm0 ⊩ (np ∧ty ,NKA_t ) → (np ∧ty ,NKA_tp ).
Lemma NKA_t_incl_NKA_tp : rm0 ⊩ (np ∧ty ,NKA_t ) → (po ∧(np ∧ty ),NKA_tp ).
Lemma NKA_t_incl_NKA_tp_nm :
  rm0 ⊩ (mlt ∧(np ∧ty ),NKA_t ) → (mlt ∧(po ∧(np ∧ty )),NKA_tp ).
Lemma NKA_t_incl_NKA_tp_ns :
  rm0 ⊩ (sg ∧(np ∧ty ),NKA_t ) → (sg ∧(po ∧(np ∧ty )),NKA_tp ).

Lemma NKA_tp_incl_NKA_t :
  rm0 ⊩ (sp ∧(np ∧ty ),NKA_tp ) → (np ∧ty ,NKA_t ).
Lemma NKA_tp_incl_NKA_tnm :
  rm0 ⊩ (mlt ∧(sp ∧(np ∧ty )),NKA_tp ) → (mlt ∧(np ∧ty ),NKA_t ).
Lemma NKA_tp_incl_NKA_tns :
  rm0 ⊩ (sg ∧(sp ∧(np ∧ty )),NKA_tp ) → (sg ∧(np ∧ty ),NKA_t ).

Lemma NKA_θ_NKA_θp : rm0 ⊩ (ut ,NKA_θ ) → (ut ,NKA_θp ).
Lemma NKA_θ_incl_NKA_θp : rm0 ⊩ (ut ,NKA_θ ) → (po ∧ut ,NKA_θp ).
Lemma NKA_θ_incl_NKA_θp_s : rm0 ⊩ (sg ∧ut ,NKA_θ ) → (sg ∧(po ∧ut ),NKA_θp ).
Lemma NKA_θ_incl_NKA_θp_m :
  rm0 ⊩ (mlt ∧ut ,NKA_θ ) → (mlt ∧(po ∧ut ),NKA_θp ).

Lemma NKA_θp_incl_NKA_θ :
  rm0 ⊩ (sp ∧ut ,NKA_θp ) → (ut ,NKA_θ ).
Lemma NKA_θp_incl_NKA_θ_s : rm0 ⊩ (sg ∧(sp ∧ut ),NKA_θp ) → (sg ∧ut ,NKA_θ ).
Lemma NKA_θp_incl_NKA_θ_m :
  rm0 ⊩ (mlt ∧(sp ∧ut ),NKA_θp ) → (mlt ∧ut ,NKA_θ ).

Lemma NKA_θt_NKA_θtp : rm0 ⊩ (ty ,NKA_θt ) → (ty ,NKA_θtp ).

Lemma NKA_θt_incl_NKA_θtp : rm0 ⊩ (ty ,NKA_θt ) → (po ∧ty ,NKA_θtp ).
Lemma NKA_θt_incl_NKA_θtp_s :
  rm0 ⊩ (sg ∧ty ,NKA_θt ) → (sg ∧(po ∧ty ),NKA_θtp ).
Lemma NKA_θt_incl_NKA_θtp_m :
  rm0 ⊩ (mlt ∧ty ,NKA_θt ) → (mlt ∧(po ∧ty ),NKA_θtp ).

Lemma NKA_θtp_incl_NKA_θt :
  rm0 ⊩ (sp ∧ty ,NKA_θtp ) → (ty ,NKA_θt ).
Lemma NKA_θtp_incl_NKA_θt_s :
  rm0 ⊩ (sg ∧(sp ∧ty ),NKA_θtp ) → (sg ∧ty ,NKA_θt ).
Lemma NKA_θtp_incl_NKA_θt_m :
  rm0 ⊩ (mlt ∧(sp ∧ty ),NKA_θtp ) → (mlt ∧ty ,NKA_θt ).

Lemma NKA_θp_NKA_θtp_fun :
  typed_vers ⊩ (Bs ut ,NKA_θp ) → (ty',NKA_θtp ).
Lemma NKA_θp_NKA_θtp_precise :
  typed_vers ⊩ (ut ,NKA_θp ) → (ty ,NKA_θtp ).
Lemma NKA_θtp_NKA_θp_fun :
  erase ⊩ (sp ∧ ty',NKA_θtp ) →
  (sp ∧ ut ,NKA_θp ).
Lemma NKA_p_NKA_tp :
  typed_vers ⊩ (sp ∧(np ∧Bs ut ),NKA_p ) →
  (sp ∧(np ∧ty'), NKA_tp ).
Lemma NKA_p_NKA_tp_precise :
  typed_vers ⊩ (sp ∧(np ∧ut ),NKA_p ) → (sp ∧(np ∧ty ),NKA_tp ).
Lemma NKA_tp_NKA_p :
  erase ⊩ (sp ∧(np ∧ty'),NKA_tp ) →
  (sp ∧(np ∧ut ),NKA_p ).
Lemma NKA_p_NKA_tp_s:
  typed_vers
    ⊩ (sg ∧(sp ∧ (np ∧ Bs ut )), NKA_p ) → (sg ∧(sp ∧ (np ∧ ty')), NKA_tp ).
Lemma NKA_θp_NKA_θtp_s:
  typed_vers ⊩ (sg ∧(Bs ut ), NKA_θp ) → (sg ∧ty', NKA_θtp ).
Lemma NKA_p_NKA_tp_m:
  typed_vers
    ⊩ (mlt ∧(sp ∧(np ∧Bs ut )),NKA_p ) → (mlt ∧(sp ∧ (np ∧ ty')), NKA_tp ).
Lemma NKA_θp_NKA_θtp_m:
  typed_vers ⊩ (mlt ∧(Bs ut ), NKA_θp ) → (mlt ∧ty', NKA_θtp ).

Lemma NKA_tp_NKA_p_s :
  erase
    ⊩ (sg ∧ (sp ∧ (np ∧ ty')), NKA_tp ) → (sg ∧ (sp ∧ (np ∧ ut )),NKA_p ).
Lemma NKA_θtp_NKA_θp_s:
  erase ⊩ (sg ∧ (sp ∧ ty'), NKA_θtp ) → (sg ∧ (sp ∧ ut ), NKA_θp ).
Lemma NKA_tp_NKA_p_m:
  erase ⊩ (mlt ∧(sp ∧(np ∧ty')),NKA_tp ) → (mlt ∧ (sp ∧ (np ∧ ut )), NKA_p ).
Lemma NKA_θtp_NKA_θp_m:
  erase ⊩ (mlt ∧ (sp ∧ ty'), NKA_θtp ) → (mlt ∧ (sp ∧ ut ), NKA_θp ).

Lemma NKA_θ_NKA_fun :
  rm_perm ∘ (apply_perm [])⊩(sp ∧ut ,NKA_θp )→ (np ∧(sp ∧ut ),NKA_p ).
Lemma NKA_θt_NKA_t_fun :
  rm_perm ∘ (apply_perm [])⊩(sp ∧ty ,NKA_θtp )→ (np ∧(sp ∧ty ),NKA_tp ).
Lemma NKA_θ_NKA_s :
  rm_perm ∘ (apply_perm [])
          ⊩(sg ∧(sp ∧ut ),NKA_θp )→ (sg ∧(np ∧(sp ∧ut )),NKA_p ).
Lemma NKA_θ_NKA_m :
  rm_perm ∘ (apply_perm [])
          ⊩(mlt ∧(sp ∧ut ),NKA_θp )→ (mlt ∧(np ∧(sp ∧ut )),NKA_p ).
Lemma NKA_NKA_θ_fun :
  (fun e ⇒ e ) ⊩ (np ∧(sp ∧ut ),NKA_p )→(sp ∧ut ,NKA_θp ).
Lemma NKA_t_NKA_θt_fun :
  (fun e ⇒ e ) ⊩ (np ∧(sp ∧ty ),NKA_tp )→(sp ∧ty ,NKA_θtp ).
Lemma NKA_NKA_θ_s :
  (fun e ⇒ e ) ⊩ (sg ∧(np ∧(sp ∧ut )),NKA_p )→(sg ∧(sp ∧ut ),NKA_θp ).
Lemma NKA_NKA_θ_m :
  (fun e ⇒ e ) ⊩ (mlt ∧(np ∧(sp ∧ut )),NKA_p )→(mlt ∧(sp ∧ut ),NKA_θp ).

Lemma single_multi_ut :
  single_to_multi ⊩ (sg ∧(sp ∧ut ),NKA_θp ) →
  (mlt ∧(sp ∧ut ),NKA_θp ).
Lemma single_multi_ty :
  single_to_multi ⊩ (sg ∧(sp ∧ty ),NKA_θtp ) →
  (mlt ∧(sp ∧ty ),NKA_θtp ).

Order between theories.

Expressions without explicit permutations.

Lemma NKAnspu_is_model_NKAnsu : NKAnspu ⊲ NKAnsu.

For untyped and typed expressions, zero may be eliminated.

Lemma NKAnsu_NKAnspu_eq : NKAnsu ≡≡ NKAnspu.
Lemma NKAnmpu_is_model_NKAnmu : NKAnmpu ⊲ NKAnmu.
Lemma NKAnmu_NKAnmpu_eq : NKAnmu ≡≡ NKAnmpu.
Lemma NKAnspt_is_model_NKAnst : NKAnspt ⊲ NKAnst.
Lemma NKAnst_NKAnspt_eq : NKAnst ≡≡ NKAnspt.
Lemma NKAnmpt_is_model_NKAnmt : NKAnmpt ⊲ NKAnmt.
Lemma NKAnmt_NKAnmpt_eq : NKAnmt ≡≡ NKAnmpt.

Typed and untyped expressions are equivalent.

Lemma NKAnmpu_is_model_NKAnmpt : NKAnmpu ⊲ NKAnmpt.

Lemma NKAnspu_is_model_NKAnspt : NKAnspu ⊲ NKAnspt.
Lemma NKAnspu_NKAnspt_eq : NKAnspu ≡≡ NKAnspt.
Lemma NKAnmpu_NKAnmpt_eq : NKAnmpu ≡≡ NKAnmpt.

For positive expressions, it is equivalent to have

explicit and applied permutations.

Lemma NKAnspu_is_model_NKAspu : NKAnspu ⊲ NKAspu.
Lemma NKAspu_is_model_NKAnspu : NKAspu ⊲ NKAnspu.
Lemma NKAnspu_NKAspu_eq : NKAnspu ≡≡ NKAspu.
Lemma NKAnmpu_is_model_NKAmpu : NKAnmpu ⊲ NKAmpu.
Lemma NKAmpu_is_model_NKAnmpu : NKAmpu ⊲ NKAnmpu.
Lemma NKAnmpu_NKAmpu_eq : NKAnmpu ≡≡ NKAmpu.

Lemma NKAnspt_is_model_NKAspt : NKAnspt ⊲ NKAspt.
Lemma NKAspt_is_model_NKAnspt : NKAspt ⊲ NKAnspt.
Lemma NKAnspt_NKAspt_eq : NKAnspt ≡≡ NKAspt.
Lemma NKAnmpt_is_model_NKAmpt : NKAnmpt ⊲ NKAmpt.
Lemma NKAmpt_is_model_NKAnmpt : NKAmpt ⊲ NKAnmpt.
Lemma NKAnmpt_NKAmpt_eq : NKAnmpt ≡≡ NKAmpt.

Expression with explicit permutations over atoms.

Zero may be eliminated both in the untyped and typed setting.

Lemma NKAspu_is_model_NKAsu : NKAspu ⊲ NKAsu.
Lemma NKAmpu_is_model_NKAmu : NKAmpu ⊲ NKAmu.
Lemma NKAspt_is_model_NKAst : NKAspt ⊲ NKAst.
Lemma NKAmpt_is_model_NKAmt : NKAmpt ⊲ NKAmt.
Lemma NKAspu_is_model_NKAspt : NKAspu ⊲ NKAspt.
Lemma NKAmpu_is_model_NKAmpt : NKAmpu ⊲ NKAmpt.

Lemma NKAsu_NKAspu_eq : NKAsu ≡≡ NKAspu.
Lemma NKAst_NKAspt_eq : NKAst ≡≡ NKAspt.

Typed and untyped expressions are equivalent.

Lemma NKAspu_NKAspt_eq : NKAspu ≡≡ NKAspt.

Expressions over letters (with explicit permutations).

In this theory zero may be eliminated as well.

Lemma NKAmu_NKAmpu_eq : NKAmu ≡≡ NKAmpu.
Lemma NKAmt_NKAmpt_eq : NKAmt ≡≡ NKAmpt.

Typed and untyped versions of the theory are also equivalent.

Lemma NKAmpu_NKAmpt_eq : NKAmpu ≡≡ NKAmpt.

The theory of expressions over atoms may be encoded in that of expressions over letters.

Theorem ut_Single_to_Multi : NKAspu ⊲ NKAmpu.
Theorem ty_Single_to_Multi : NKAspt ⊲ NKAmpt.