Library theories

Equationnal theories.

Definition TyEq := (predicate expr ×relation expr)%type.

Definition NKA_θtp :=
  (ka_eq_t ∨eq_perm ∨eq_perm_ω ∨eq_perm_elim
          ∨eq_ν_smpl ∨eq_ω _smpl ∨eq_nom_typed_p ∨eq_nom_typed).
Definition NKAmpt : TyEq := (multi ⊗str_positive ⊗typed ,NKA_θtp ).
Definition NKAspt : TyEq := (single ⊗str_positive ⊗typed ,NKA_θtp ).

Definition NKA_θt :=NKA_θtp ∨zero_eq_t.
Definition NKAmt : TyEq := (multi ⊗typed ,NKA_θt ).
Definition NKAst : TyEq := (single ⊗typed ,NKA_θt ).

Definition NKA_θp :=
  (ka_eq_u ∨eq_perm ∨eq_perm_elim
          ∨eq_ν_smpl ∨eq_nom_untyped_p ∨eq_nom_untyped).
Definition NKAmpu : TyEq := (multi ⊗str_positive ⊗untyped ,NKA_θp ).
Definition NKAspu : TyEq := (single ⊗str_positive ⊗untyped ,NKA_θp ).

Definition NKA_θ := NKA_θp ∨zero_eq_u.
Definition NKAmu : TyEq := (multi ⊗untyped ,NKA_θ ).
Definition NKAsu : TyEq := (single ⊗untyped ,NKA_θ ).

Definition NKA_tp :=
  (ka_eq_t ∨eq_ν_smpl ∨eq_ω _smpl ∨eq_nom_typed ∨eq_nom_typed_np).
Definition NKAnspt : TyEq := (no_perm ⊗single ⊗str_positive ⊗typed ,NKA_tp ).
Definition NKAnmpt : TyEq := (no_perm ⊗multi ⊗str_positive ⊗typed ,NKA_tp ).

Definition NKA_t := NKA_tp ∨zero_eq_t.
Definition NKAnst : TyEq := (no_perm ⊗single ⊗typed ,NKA_t ).
Definition NKAnmt : TyEq := (no_perm ⊗multi ⊗typed ,NKA_t ).

Definition NKA_p :=
  (ka_eq_u ∨eq_ν_smpl ∨eq_nom_untyped ∨eq_nom_untyped_np).
Definition NKAnspu : TyEq :=
  (no_perm ⊗single ⊗str_positive ⊗untyped ,NKA_p ).
Definition NKAnmpu : TyEq := (no_perm ⊗multi ⊗str_positive ⊗untyped ,NKA_p ).

Definition NKA := NKA_p ∨zero_eq_u.
Definition NKAnsu : TyEq := (no_perm ⊗single ⊗untyped ,NKA ).
Definition NKAnmu : TyEq := (no_perm ⊗multi ⊗untyped ,NKA ).

The following sets of axioms will only be used as intermediary in proofs.

Definition NKA_tp' :=
  (((ka_eq_t ∨ eq_ν_smpl ) ∨ eq_ω _smpl ) ∨ eq_nom_typed )
    ∨ (np ∧ eq_nom_typed_np ).
Definition NKA_p' :=
  ((ka_eq_u ∨ eq_ν_smpl ) ∨ eq_nom_untyped )
    ∨ (np ∧ eq_nom_untyped_np ).
Definition NKA' :=
  ut ∧ NKA_p.

Simple Properties of these theories.

Preservation of single.

Lemma NKA_p_single : Proper (NKA_p ==> iff) single.
Lemma NKA_tp_single : Proper (NKA_tp ==> iff) single.
Lemma NKA_θp_single : Proper (NKA_θp ==> iff) single.
Lemma NKA_θtp_single : Proper (NKA_θtp ==> iff) single.

Preservation of multi.

Lemma NKA_p_multi : Proper (NKA_p ==> iff) multi.
Lemma NKA_tp_multi : Proper (NKA_tp ==> iff) multi.
Lemma NKA_θp_multi : Proper (NKA_θp ==> iff) multi.
Lemma NKA_θtp_multi : Proper (NKA_θtp ==> iff) multi.

Preservation of str_positive.

Lemma NKA_p_str_positive : Proper (NKA_p ==> iff) str_positive.
Lemma NKA_tp_str_positive : Proper (NKA_tp ==> iff) str_positive.
Lemma NKA_θp_str_positive : Proper (NKA_θp ==> iff) str_positive.
Lemma NKA_θtp_str_positive : Proper (NKA_θtp ==> iff) str_positive.

Type preservation.

Lemma NKA_θtp_has_type A : Proper (NKA_θtp ==> iff) (has_type A).
Lemma NKA_θt_has_type A : Proper (NKA_θt ==> iff) (has_type A).
Lemma NKA_tp_has_type A : Proper (NKA_tp ==> iff) (has_type A).
Lemma NKA_t_has_type A : Proper (NKA_t ==> iff) (has_type A).
Lemma NKA_θp_untyped : Proper (NKA_θp ==> iff) untyped.
Lemma NKA_θ_untyped : Proper (NKA_θ ==> iff) untyped.
Lemma NKA_p_untyped : Proper (NKA_p ==> iff) untyped.
Lemma NKA_untyped : Proper (NKA ==> iff) untyped.
Lemma NKA_tp'_has_type A : Proper (NKA_tp' ==> iff) (has_type A).
Lemma NKA_p'_untyped : Proper (NKA_p' ==> iff) untyped.
Lemma NKA'_untyped : Proper (NKA' ==> iff) untyped.

NKA' is not different from NKA_p.

Lemma switch_NKA'_NKA_p :
∀ e f, ut e f → NKA_p ⊢ e ≡ f → NKA' ⊢ e ≡ f.
Lemma switch_NKA_p_NKA' :
∀ e f, NKA' ⊢ e ≡ f → NKA_p ⊢ e ≡ f.

Preservation of eq0.

Lemma NKA_θtp_eq0 : Proper (NKA_θtp ==> Logic.eq) eq0.
Lemma NKA_θt_eq0 : Proper (NKA_θt ==> Logic.eq) eq0.
Lemma NKA_tp_eq0 : Proper (NKA_tp ==> Logic.eq) eq0.
Lemma NKA_t_eq0 : Proper (NKA_t ==> Logic.eq) eq0.
Lemma NKA_θp_eq0 : Proper (NKA_θp ==> Logic.eq) eq0.
Lemma NKA_θ_eq0 : Proper (NKA_θ ==> Logic.eq) eq0.
Lemma NKA_p_eq0 : Proper (NKA_p ==> Logic.eq) eq0.
Lemma NKA_eq0 : Proper (NKA ==> Logic.eq) eq0.

Preservation of rm0.

Lemma NKA_θtp_rm0 : Proper (ty' ∧ NKA_θtp ==> eq NKA_θtp) rm0.
Lemma NKA_tp_rm0 : Proper (ty' ∧ NKA_tp ==> eq NKA_tp) rm0.
Lemma NKA_θp_rm0 : Proper (ut ∧ NKA_θp ==> eq NKA_θp) rm0.
Lemma NKA_p_rm0 : Proper (ut ∧ NKA_p ==> eq NKA_p) rm0.

support preservation.

Lemma NKA_θp_support : Proper (NKA_θp ==> equiv_lst) support.
Lemma NKA_p_support : Proper (NKA_p ==> equiv_lst) support.
Lemma NKA_p'_support : Proper (NKA_p' ==> equiv_lst) support.
Lemma NKA'_support : Proper (NKA' ==> equiv_lst) support.

Preservation of erase.

Lemma NKAθ_erase : Proper (ty' ∧ NKA_θtp ==> eq NKA_θp) erase.
Lemma NKA_erase' : Proper (ty' ∧ NKA_tp' ==> eq NKA_p') erase.

Preservation of typed_vers.

Lemma NKAθ_typed_vers : Proper (ut ∧ NKA_θp ==> eq NKA_θtp) typed_vers.
Lemma NKA_typed_vers' : Proper (ut ∧ NKA_p' ==> eq NKA_tp') typed_vers.

Preservation of str_positive.

Lemma NKA'_pos : ∀ e f, NKA' ⊢ e ≡ f →
(str_positive e ↔ str_positive f ).
Lemma NKA_pos : ∀ e f, NKA_p ⊢ e ≡ f →
(str_positive e ↔ str_positive f ).

Preservation of no_perm.

Lemma NKA_p_Np : Proper (NKA_p ==> iff) no_perm.
Lemma NKA_tp_Np : Proper (NKA_tp ==> iff) no_perm.

Zero is different than One.

Lemma zero_diff_un_NKA_θp : ¬ (NKA_θp ⊢ 0 ≡ 1 ).
Lemma zero_diff_un_NKA_θtp : ¬ (NKA_θtp ⊢ ⊥ [] ≡ id []).
Lemma zero_diff_un_NKA_p : ¬ (NKA_p ⊢ 0 ≡ 1 ).
Lemma zero_diff_un_NKA_tp : ¬ (NKA_tp ⊢ ⊥ [] ≡ id []).
Lemma at_diff_un_NKA_θp a : ¬ (NKA_θp ⊢ vat a ≡ 1 ).
Lemma le_diff_un_NKA_θp x : τ x ≠ [] → ¬ (NKA_θp ⊢ var x ≡ 1 ).
Lemma id_a_diff_un_NKA_θtp a : ¬ (NKA_θtp ⊢ id [a ] ≡ id []).
Lemma at_diff_un_NKA_p a : ¬ (NKA_p ⊢ vat a ≡ 1 ).
Lemma le_diff_un_NKA_p x : τ x ≠ [] → ¬ (NKA_p ⊢ var x ≡ 1 ).
Lemma id_a_diff_un_NKA_tp a : ¬ (NKA_tp ⊢ id [a ] ≡ id []).

Transfer lemmas from one system to the other.

NKA_tp' is equivalent to NKA_tp for typed expressions without permutation over single variables.

Lemma NKA_tp'_NKA_tp_eq :
∀ e f,(np ∧ ty) e f →
(NKA_tp'⊢ e ≡f ↔ NKA_tp ⊢ e ≡f ).

NKA_p' is equivalent to NKA_p for untyped expressions without permutation over single variables.

Lemma NKA_p'_NKA_p_eq :
∀ e f,(np ∧ut) e f →
(NKA_p'⊢ e ≡f ↔ NKA_p ⊢ e ≡f ).

For positive untyped expressions, eq NKA' entails eq NKA_θp.

Lemma NKA'_NKA_θp e f :
  NKA' ⊢ e ≡ f → positive e → positive f →
  untyped e → untyped f →
  NKA_θp ⊢ e ≡ f.

Lemma NKA_tp_NKA_θtp e f:
  ty e f ∧ sp e f ∧ np e f →
  NKA_tp ⊢ e ≡ f → NKA_θtp ⊢ e ≡ f.

For every permutation p, the function rm_perm ∘ apply_perm p is a morphism between NKA_θp and eq (NKA_p)

Lemma NKA_θp_NKA_p_rm_perm_apply_perm :
  ∀ p : perm,
    Proper (NKA_θp ==> eq NKA_p)
           (rm_perm ∘ apply_perm p).
Lemma NKA_θtp_NKA_tp_rm_perm_apply_perm :
  ∀ p : perm,
    Proper (NKA_θtp ==> eq NKA_tp)
           (rm_perm ∘ apply_perm p).

Technical lemmas.

Lemma support_or_diff_NKA_p :
  (∀ e f, (Bs ut) e f ∨ ¬ untyped e ∨ ¬ untyped f
               ∨ ¬ (NKA_p ⊢ e ≡f )).
Lemma ty'_or_diff_NKA_tp :
  (∀ e f, ty' e f ∨
               ¬ typed e ∨ ¬ typed f
               ∨ ¬ (NKA_tp ⊢ e ≡f )).
Lemma support_or_diff_NKA_θp :
  (∀ e f, (Bs ut) e f ∨ ¬ untyped e ∨ ¬ untyped f
               ∨ ¬ (NKA_θp ⊢ e ≡f )).
Lemma ty'_or_diff_NKA_θtp :
  (∀ e f, ty' e f ∨ ¬ typed e ∨ ¬ typed f
               ∨ ¬ (NKA_θtp ⊢ e ≡f )).

Good theories.

Definition good (th : TyEq) :=
∀ e f, (snd th) e f →
(fst th) e ↔ (fst th) f.
Lemma goodNKAmpt : good NKAmpt.
Lemma goodNKAspt : good NKAspt.

Lemma goodNKAmpu : good NKAmpu.
Lemma goodNKAspu : good NKAspu.

Lemma goodNKAnmpt : good NKAnmpt.
Lemma goodNKAnspt : good NKAnspt.

Lemma goodNKAnmpu : good NKAnmpu.
Lemma goodNKAnspu : good NKAnspu.