Library theories

Equationnal theories.

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

Definition NKA_θtp :=
Definition NKAmpt : TyEq := (multistr_positivetyped,NKA_θtp).
Definition NKAspt : TyEq := (singlestr_positivetyped,NKA_θtp).

Definition NKA_θt :=NKA_θtpzero_eq_t.
Definition NKAmt : TyEq := (multityped,NKA_θt).
Definition NKAst : TyEq := (singletyped,NKA_θt).

Definition NKA_θp :=
Definition NKAmpu : TyEq := (multistr_positiveuntyped,NKA_θp).
Definition NKAspu : TyEq := (singlestr_positiveuntyped,NKA_θp).

Definition NKA_θ := NKA_θpzero_eq_u.
Definition NKAmu : TyEq := (multiuntyped,NKA_θ).
Definition NKAsu : TyEq := (singleuntyped,NKA_θ).

Definition NKA_tp :=
Definition NKAnspt : TyEq := (no_permsinglestr_positivetyped,NKA_tp).
Definition NKAnmpt : TyEq := (no_permmultistr_positivetyped,NKA_tp).

Definition NKA_t := NKA_tpzero_eq_t.
Definition NKAnst : TyEq := (no_permsingletyped,NKA_t).
Definition NKAnmt : TyEq := (no_permmultityped,NKA_t).

Definition NKA_p :=
Definition NKAnspu : TyEq :=
Definition NKAnmpu : TyEq := (no_permmultistr_positiveuntyped,NKA_p).

Definition NKA := NKA_pzero_eq_u.
Definition NKAnsu : TyEq := (no_permsingleuntyped,NKA).
Definition NKAnmu : TyEq := (no_permmultiuntyped,NKA).

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

Simple Properties of these theories.

Preservation of single.

Preservation of multi.

Preservation of str_positive.

Type preservation.

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.

Preservation of rm0.

support preservation.

Preservation of erase.

Preservation of 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.

Zero is different than One.

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' ef NKA_tp ef).

NKA_p' is equivalent to NKA_p for untyped expressions without permutation over single variables.
Lemma NKA_p'_NKA_p_eq :
   e f,(nput) e f
             (NKA_p' ef NKA_p ef).
For positive untyped expressions, eq NKA' entails eq NKA_θp.
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 ef)).
Lemma ty'_or_diff_NKA_tp :
  ( e f, ty' e f
               ¬ typed e ¬ typed f
                ¬ (NKA_tp ef)).
Lemma support_or_diff_NKA_θp :
  ( e f, (Bs ut) e f ¬ untyped e ¬ untyped f
                ¬ (NKA_θp ef)).
Lemma ty'_or_diff_NKA_θtp :
  ( e f, ty' e f ¬ typed e ¬ typed f
                ¬ (NKA_θtp ef)).

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.