Library morphisms



Coertions between untyped and typed expressions.

Produces an untyped expression by removing all ω.
Fixpoint erase (e : expr) : expr :=
  match e with
    | 0 | ⊥ _ ⇒ 0
    | 1 | id _ ⇒ 1
    | var x ⇒ var x
    | vat x ⇒ vat x
    | e + f ⇒ erase e + erase f
    | e · f ⇒ erase e · erase f
    | e ^* ⇒ (erase e) ^*
    | ‹ p › e ⇒ ‹ p › (erase e)
    | ν a e ⇒ ν a (erase e)
    | ω a e ⇒ erase e
  end.
Notation " ⎣ e ⎦ " := (erase e).
erase perserves no_perm, single, multi, str_positive and positive. An atom is fresh for ⎣e⎦ if it doesn't appear in the type of e.
Lemma fresh_type : ∀ A e, A ⊨ e → ∀ a, ¬ In a A → a # ⎣e⎦.

The support of §e is included in its type.
Lemma support_min_type : ∀ e A, A ⊨ e → support ⎣e⎦ ⊆ A.

W gets obliterated by erase.
Lemma W_erase l e : ⎣W l e⎦ = ⎣e⎦.
Lemma no_perm_erase : ∀ e, no_perm e → no_perm ⎣e⎦.
Lemma single_erase : ∀ e, single e → single ⎣e⎦.
Lemma multi_erase : ∀ e, multi e → multi ⎣e⎦.
Lemma str_positive_erase :
  ∀ e, str_positive e → str_positive ⎣e⎦.
Lemma positive_erase : ∀ e, positive e → positive ⎣e⎦.
The size of ⎣e⎦ is smaller than that of e.
Lemma size_erase : ∀ e, size ⎣e⎦ ≤ size e.
⎣e⎦ is always untyped.
Lemma untyped_erase : ∀ e, untyped ⎣e⎦.
⎣⎦ preserves ==.
Lemma eq_expr_erase : Proper (eq_expr ==> eq_expr) erase.
Produces a typed expression, by using W and support heavily.
Fixpoint typed_vers (e : expr) :=
  match e with
    | 0 ⇒ ⊥ []
    | 1 ⇒ id []
    | var x ⇒ var x
    | vat x ⇒ vat x
    | e + f ⇒
      W (〈support f〉--(support e)) (typed_vers e)
      + W (〈support e〉--(support f)) (typed_vers f)
    | e · f ⇒
      W (〈support f〉--(support e)) (typed_vers e)
      · W (〈support e〉--(support f)) (typed_vers f)
    | e ^* ⇒ (typed_vers e)^*
    | ‹ p › e ⇒ ‹ p › (typed_vers e)
    | ν a e ⇒
      if inb a (support e)
      then ν a (typed_vers e)
      else ν a (ω a (typed_vers e))
    | _ ⇒ e
  end.
Notation " ⎡ e ⎤ " := (typed_vers e).

Section poly.
  Hypothesis K_not_zero : O < K.
  Hypothesis bounded_τ : ∀ x, length (τ x) ≤ K.
  Lemma typed_vers_size e : size (⎡e⎤) ≤ (K*(size e)*(size e))%nat.
End poly.

First half of a bijection between typed and untyped expressions.
Lemma typed_version_erase e : untyped e → ⎣⎡e⎤⎦ = e.

typed_vers perserves no_perm, single, multi, str_positive and positive.
Lemma no_perm_typed_vers : ∀ e, no_perm e → no_perm ⎡e⎤.
Lemma single_typed_vers : ∀ e, single e → single ⎡e⎤.
Lemma multi_typed_vers : ∀ e, multi e → multi ⎡e⎤.
Lemma str_positive_typed_vers :
  ∀ e, str_positive e → str_positive ⎡e⎤.
Lemma positive_typed_vers :
  ∀ e, positive e → positive ⎡e⎤.
The size of ⎡e⎤ is larger than that of e.
Lemma size_typed_vers : ∀ e, size e ≤ size ⎡e⎤.
The support of e can type ⎡e⎤, if e is untyped.
Lemma typed_version_support_type e : untyped e → (support e) ⊨ ⎡e⎤.

rm0 e removes 0 and ⊥ _ from e if it is possible,

and returns 0 or ⊥ _ otherwise.
Fixpoint rm0 e :=
  match e with
    | e + f ⇒
      let e := rm0 e in
      let f := rm0 f in
      if (eq0' e)
      then f
      else if eq0' f
           then e
           else (e + f)
    | e · f ⇒
      let e := rm0 e in
      let f := rm0 f in
      if (eq0' e)
      then e
      else if eq0' f
           then f
           else (e · f)
    | e^* ⇒
      let e := rm0 e in
      match get_bot e with
      | inl false ⇒ 1
      | inr A ⇒ id A
      | inl true ⇒ e^*
      end
    | ν a e ⇒
      let e := rm0 e in
      match get_bot e with
      | inl false ⇒ 0
      | inr A ⇒ ⊥ (rm a A)
      | inl true ⇒ ν a e
      end
    | ‹ p › e ⇒
      let e := rm0 e in
      match get_bot e with
      | inl false ⇒ 0
      | inr A ⇒ ⊥ (p⧓ A)
      | inl true ⇒ ‹ p › e
      end
    | ω a e ⇒
      let e := rm0 e in
      match get_bot e with
      | inl false ⇒ 0
      | inr A ⇒ ⊥ (a :: A)
      | inl true ⇒ ω a e
      end
    | e ⇒ e
  end.
rm0 perserves no_perm,single,multi and str_positive.
Lemma no_perm_rm0 : ∀ e, no_perm e → no_perm (rm0 e).
Lemma single_rm0 : ∀ e, single e → single (rm0 e).
Lemma multi_rm0 : ∀ e, multi e → multi (rm0 e).
Lemma str_positive_rm0 : ∀ e, str_positive e →
                                   str_positive (rm0 e).
rm0 preserves untypedness.
Lemma untyped_rm0 : ∀ e, untyped e → untyped (rm0 e).
rm0 reduces the size of the expression.
Lemma size_rm0 : ∀ e, size (rm0 e) ≤ size e.
rm0 preserves types.
Lemma typed_rm0 : ∀ e A, A ⊨ e → A ⊨ (rm0 e).

rm0 and eq0 agree on untyped expressions.
Lemma eq0_rm0_u : ∀ e, eq0 e = eq0' (rm0 e).
rm0 e is either syntactically null or str_positive.
Lemma positive_or_nul_rm0 e : eq0' (rm0 e) = true ∨
                              (str_positive (rm0 e)).
rm0 e is always positive.
Lemma positive_rm0 e : positive (rm0 e).
rm0 is the identity over str_positive expressions.
Lemma str_positive_rm0_id : ∀ e, str_positive e → rm0 e = e.
positive expressions compose the kernel of rm0.
Lemma positive_rm0_id : ∀ e, positive e ↔ rm0 e = e.
rm0 is involutive.
Lemma rm0_involutive : ∀ e, rm0 (rm0 e) = rm0 e.
rm0 preserves freshness for untyped expressions.
Lemma fresh_rm0 a e : untyped e → fresh a e → fresh a (rm0 e).
rm0 preserves ==.
Lemma eq_expr_rm0 : Proper (eq_expr ==> eq_expr) rm0.

Applying permutations.

Reserved Notation " p • e " (at level 19).
Lemma apply_perm_var_bis : ∀ p x l, is_perm_bool (x,l) = true →
    is_perm_bool (x,p ⧓ l) = true.

Definition apply_perm_var (p : perm) (n : Letter) : Letter :=
  match n with
  | exist _ (x,l) h ⇒ (exist (fun x ⇒ is_perm_bool x = true) (x,p⧓l)
                              (@apply_perm_var_bis p x l h))
  end.

Lemma apply_perm_var_τ (p : perm) (n : Letter) :
  τ (apply_perm_var p n) = p ⧓ (τ n).
Lemma apply_perm_var_app (p q : perm) (n : Letter) :
  (apply_perm_var q (apply_perm_var p n)) ≃ apply_perm_var (q++p) n.
Lemma apply_perm_var_equiv_perm n :
  Proper (equiv_perm ==> eq_letter) (Basics.flip apply_perm_var n).
Lemma apply_perm_var_eq_letter p :
  Proper (eq_letter ==> eq_letter) (apply_perm_var p).
Lemma apply_perm_var_equiv_perm_eq_letter :
  Proper (equiv_perm ==> eq_letter ==> eq_letter) apply_perm_var.

Fixpoint apply_perm p e :=
  match e with
  | id A ⇒ id (p⧓A)
  | ⊥ A ⇒ ⊥ (p⧓A)
  | 0 ⇒ 0
  | 1 ⇒ 1
  | var x ⇒ var (apply_perm_var p x)
  | vat a ⇒ vat (p⋈a)
  | e + f ⇒ p • e + p • f
  | e · f ⇒ p • e · p • f
  | e^* ⇒ p • e ^*
  | ‹ q › e ⇒ ‹ [] › (p++q) • e
  | ν a e ⇒ ν (p⋈a) (p • e)
  | ω a e ⇒ ω (p⋈a) (p • e)
  end
where " p • e " := (apply_perm p e).
Global Instance apply_perm_equiv_perm :
  Proper (equiv_perm ==> eq_expr ==> eq_expr) apply_perm.

p•e is not bigger than twice the size of e.
Lemma apply_perm_size e p : size (p•e) ≤ 2 × size e.

apply_perm perserves single, multi and eq0.
Lemma multi_apply_perm : ∀ e p, multi e ↔ multi (p•e).

Lemma single_apply_perm : ∀ e p, single e ↔ single (p•e).

Lemma eq0_apply_perm : ∀ e p, eq0 (p•e) = eq0 e.

apply_perm doesn't change no_perm.
Lemma no_perm_apply_perm :
  ∀ e p, (no_perm e ↔ no_perm (p•e)).

apply_perm isn't a problem for typing.
Lemma has_type_apply_perm : ∀ e A p, (p⋆⧓A) ⊨ e → A ⊨ p • e.
Lemma apply_perm_has_type {e A} :
  ∀ p, (p⧓A) ⊨ (p • e) → A ⊨ e.

apply_perm doesn't change untypedness.
Lemma untyped_apply_perm : ∀ e p, untyped e ↔ untyped (p•e).

apply_perm works well with freshness.
Lemma fresh_apply_perm : ∀ e a p, a # e ↔ (p⋈a) # p • e.

The support of p•e is p applied to the support of e.
Lemma support_apply_perm : ∀ e p, support (p•e) = p ⧓ (support e).
apply_perm commutes with erase,typed_vers and W.
Lemma erase_apply_perm : ∀ e p, p • ⎣e⎦ = ⎣p•e⎦.

Lemma W_apply_perm : ∀ e l p, p • (W l e) = W (p⧓l) (p•e).

Lemma typed_vers_apply_perm : ∀ e p, p • ⎡e⎤ = ⎡p•e⎤.

apply_perm preserves positive and str_positive.
Lemma str_positive_apply_perm e p :
  str_positive e ↔ str_positive (p•e).

Lemma positive_apply_perm e p :
  positive e ↔ positive (p•e).
Lemma rm0_inv_apply_perm : ∀ e p, rm0 e = e → rm0 (p•e) = p•e.

Simplification lemma.
Lemma eq0'_rm0_apply_perm : ∀ e p, eq0' (rm0 (p•e)) = eq0' (rm0 e).

Technical lemma.
Lemma rm0_eq0_get_bot : ∀ e p,
    rm0 e = e → reflect3 (e = 0)
                          (fun B ⇒ e = ⊥ (p⋆⧓B))
                          (get_bot e = inl true)
                          (get_bot (p • e)).

apply_perm commutes wiht rm0.
Lemma rm0_apply_perm : ∀ e p, rm0 (p•e) = p•rm0 e.

If e doesn't contain any θ constructors, then applying the permutations [(a,a)] or [] doesn't change the expression.
Lemma apply_perm_nil (e : expr) :
  no_perm e → [] • e == e.
Lemma apply_perm_id e a :
  no_perm e → [a,a] • e == e.

Removing permutations

Fixpoint rm_perm e :=
  match e with
  | e + f ⇒ rm_perm e + rm_perm f
  | e · f ⇒ rm_perm e · rm_perm f
  | e ^* ⇒ (rm_perm e)^*
  | ν a e ⇒ ν a (rm_perm e)
  | ω a e ⇒ ω a (rm_perm e)
  | ‹ _ › e ⇒ rm_perm e
  | e ⇒ e
  end.
rm_perm reduces the size of expressions.
Lemma rm_perm_size e : size (rm_perm e) ≤ size e.
rm_perm doesn't change untypedness, single or str_positive.
Lemma untyped_rm_perm e : untyped e ↔ untyped (rm_perm e).
Lemma single_rm_perm e : single e ↔ single (rm_perm e).
Lemma multi_rm_perm e : multi e ↔ multi (rm_perm e).
Lemma str_positive_rm_perm : ∀ e, str_positive e ↔
                                   str_positive (rm_perm e).
rm_perm preserves positive.
Lemma positive_rm_perm : ∀ e, positive e → positive (rm_perm e).
The kernel of rm_perm is no_perm.
Lemma no_perm_rm_perm_id e : no_perm e ↔ rm_perm e = e.
rm_perm produces expressions statisfying no_perm.
Lemma no_perm_rm_perm e : no_perm (rm_perm e).
rm_perm and apply_perm commute partially.
Lemma rm_perm_apply_perm_swap p q e :
  rm_perm ((p++q)•e) == p•(rm_perm (q•e)).

rm_perm preserves ==.
Lemma eq_expr_rm_perm : Proper (eq_expr ==> eq_expr) rm_perm.

fresh and has_type behave well with rm_perm and apply_perm.
Lemma fresh_rm_perm p a e : (a # e ↔ p ⋈ a # rm_perm (p • e)).

Lemma has_type_rm_perm_apply_perm e p A :
  A ⊨ (p•e) → A ⊨ rm_perm (p•e).