Library sg_to_mlt

Parameter α : Atom.
Parameter λ : Letter.
Axiom τ_λ : τ λ = [α].

Reserved Notation " $ e " (at level 60, no associativity).
Fixpoint single_to_multi exp :=
  match exp with
  | vat a ⇒ ‹[a,α]›var λ
  | e + f ⇒ ($ e) + $ f
  | e · f ⇒ ($ e) · $ f
  | e ^* ⇒ ($ e) ^*
  | ν a e ⇒ ν a ( $ e )
  | ω a e ⇒ ω a ( $ e )
  | ‹ p ›e ⇒ ‹ p ›$ e
  | _ ⇒ exp
  end
where " $ e " := (single_to_multi e).
Lemma size_single_to_multi e : size ($ e) ≤ 2 × size e.
Lemma mlt_single_to_multi e : multi ($ e).
Lemma ut_ut_single_to_multi e :
  untyped e → untyped ($ e).
Lemma ut_single_fresh_single_to_multi e :
  untyped e → single e → ∀ a, a # e ↔ a # ($ e).
Lemma has_type_single_to_multi e A :
  A ⊨ e → A ⊨ ($ e).
Lemma ty_ty_single_to_multi e :
  typed e → typed ($ e).
Lemma poa_poa_single_to_multi e :
  str_positive e → str_positive ($ e).
Lemma po_po_single_to_multi e :
  positive e → positive ($ e).

Fixpoint image exp : Prop :=
  match exp with
  | vat _ ⇒ False
  | var x ⇒ fst (proj1_sig x) = fst (proj1_sig λ)
  | e · f | e + f ⇒ image e ∧ image f
  | e ^* | ν _ e | ‹ _ › e | ω _ e ⇒ image e
  | _ ⇒ True
  end.
Lemma sg_image_single_to_multi e :
  single e → image ($ e).
Lemma image_mlt e : image e → multi e.

Definition get_atom (n : Letter) :=
  match n with
  | exist _ (λ,[a]) _ ⇒ a
  | _ ⇒ α
  end.

Reserved Notation " £ e " (at level 60, no associativity).
Fixpoint multi_to_single exp :=
  match exp with
  | var x ⇒ vat (get_atom x)
  | e + f ⇒ (£ e) + £ f
  | e · f ⇒ (£ e) · £ f
  | e ^* ⇒ (£ e) ^*
  | ν a e ⇒ ν a ( £ e )
  | ω a e ⇒ ω a ( £ e )
  | ‹ p ›e ⇒ ‹ p ›£ e
  | e ⇒ e
  end
where " £ e " := (multi_to_single e).

Lemma ut_multi_to_single e :
   untyped e → untyped (£ e).
Lemma img_sg_multi_to_single e :
  image e → single (£ e).
Lemma img_ut_fresh_multi_to_single e :
  image e → untyped e → ∀ a, a # e ↔ a # (£ e).
Lemma has_type_multi_to_single e A :
  image e → A ⊨ e → A ⊨ (£ e).
Lemma ty_multi_to_single e :
  image e → typed e → typed (£ e).

Lemma ka_eq_u_image :
  Proper (ka_eq_u ==> iff) image.
Lemma ka_eq_t_image :
  Proper (ka_eq_t ==> iff) image.
Lemma eq_ν_smpl_image :
  Proper (eq_ν_smpl ==> iff) image.
Lemma eq_nom_untyped_image :
  Proper (eq_nom_untyped ==> iff) image.
Lemma eq_nom_typed_image :
  Proper (eq_nom_typed ==> iff) image.
Lemma eq_perm_image :
  Proper (eq_perm ==> iff) image.
Lemma eq_perm_elim_image :
  Proper (eq_perm_elim ==> iff) image.
Lemma eq_nom_untyped_p_image :
  Proper (eq_nom_untyped_p ==> iff) image.
Lemma eq_nom_typed_p_image :
  Proper (eq_nom_typed_p ==> iff) image.
Lemma NKA_θp_image :
  Proper (NKA_θp ==> iff) image.
Lemma NKA_θtp_image :
  Proper (NKA_θtp ==> iff) image.
Lemma eq_NKA_θp_image :
  Proper (eq NKA_θp ==> iff) image.
Lemma eq_NKA_θtp_image :
  Proper (eq NKA_θtp ==> iff) image.
Lemma NKA_θp_single :
  Proper (NKA_θp ==> iff) single.
Lemma NKA_θtp_single :
  Proper (NKA_θtp ==> iff) single.
Lemma eq_NKA_θp_single :
  Proper (eq NKA_θp ==> iff) single.
Lemma eq_NKA_θtp_single :
  Proper (eq NKA_θtp ==> iff) single.
Lemma NKA_θp_untyped :
  Proper (NKA_θp ==> iff) untyped.
Lemma eq_NKA_θp_untyped :
  Proper (eq NKA_θp ==> iff) untyped.
Lemma ut_multi_to_single_single_to_multi e :
  untyped e → single e → NKA_θp ⊢ £ $ e ≡ e.
Lemma ty_multi_to_single_single_to_multi e :
  typed e → single e → NKA_θtp ⊢ £ $ e ≡ e.
Lemma Proper_ut_sg_ax :
  Proper ((ut∧sg∧NKA_θp) ==> eq NKA_θp) single_to_multi.
Lemma Proper_ut_sg_eq :
  Proper ((ut ∧ sg ∧ eq NKA_θp) ==> eq NKA_θp) single_to_multi.
Lemma Proper_ty_sg_ax :
  Proper ((ty∧sg∧NKA_θtp) ==> eq NKA_θtp) single_to_multi.
Lemma Proper_ty_sg_eq :
  Proper ((ty ∧ sg ∧ eq NKA_θtp) ==> eq NKA_θtp) single_to_multi.

Definition Img A e f := (image e ∧ image f) ∧ A e f.
Lemma Proper_ut_img_ax :
  Proper (Img (ut ∧ NKA_θp) ==> eq NKA_θp) multi_to_single.
Lemma Proper_ut_img_eq :
  Proper (Img (ut ∧ (eq NKA_θp)) ==> eq NKA_θp) multi_to_single.

Lemma Proper_ty_img_ax :
  Proper (Img (ty∧NKA_θtp) ==> eq NKA_θtp) multi_to_single.

Lemma Proper_ty_img_eq :
  Proper (Img (ty ∧ (eq NKA_θtp)) ==> eq NKA_θtp) multi_to_single.