Library restr_atoms

Variable φ : Atom → Atom.
Variable ψ : Atom → Atom.
Variable ψ_φ_id : ∀ x, ψ (φ x) = x.

Lemma φ_inj : ∀ x y, φ x = φ y → x = y.

Definition X x := ∃ y, x = φ y.
Definition in_X : Atom → bool := fun x ⇒ beq_atom x (φ (ψ x)).

Lemma in_X_spec x : reflect (X x) (in_X x).
Lemma in_X_X x : (X x) ↔ (in_X x = true).

Lemma φ_X : ∀ x, X (φ x).

Lemma φ_in_X : ∀ x, in_X (φ x) = true.

Lemma φ_inv x y : x = y ↔ φ x = φ y.

Definition restr_perm θ :=
  forallb (fun p ⇒ match p with (a,b) ⇒ in_X a && in_X b end) θ.
Lemma restr_perm_act θ a : restr_perm θ = true → X a → X (θ⋈a).
Definition restr_list := forallb in_X.
Lemma restr_perm_mact θ l :
  restr_perm θ=true → restr_list l=true → restr_list (θ⧓l)=true.

Fixpoint restr_expr e :=
  match e with
  | id A | bot A ⇒ restr_list A
  | 0 | 1 | var _ | vat _ ⇒ true
  | e + f | e · f ⇒ restr_expr e && restr_expr f
  | e ^* ⇒ restr_expr e
  | ν a e | ω a e ⇒ in_X a && restr_expr e
  | ‹ p › e ⇒ restr_perm p && restr_expr e
  end.

Definition is_restr e := restr_expr e = true.

Definition map_pair (f : Atom → Atom) :=
  map (fun x ⇒ (f (fst x),f (snd x))).
Lemma map_pair_inv f p : (map_pair f p)⋆ = map_pair f (p⋆).
Lemma map_φ_act p a : (map_pair φ p) ⋈ φ a = φ (p ⋈ a).
Lemma restr_perm_map_φ p :
  restr_perm p = true → p = map_pair φ (map_pair ψ p).

Lemma map_ψ_map_φ_act_φ p a :
  (map_pair ψ (map_pair φ p)) ⋈ a = ψ ((map_pair φ p) ⋈ (φ a)).
Lemma map_ψ_act_φ p a :
  restr_perm p = true → (map_pair ψ p) ⋈ a = ψ (p ⋈ (φ a)).
Lemma map_φ_mact p A : map φ (p ⧓ A) = (map_pair φ p) ⧓ map φ A.

Lemma map_φ_rm a A : map φ (rm a A) = rm (φ a) (map φ A).

Definition perm_fun_lst f l := transfer_perm 〈l〉 (map f 〈l〉).
Lemma perm_fun_lst_mact f : ∀ l,
    NoDup (map f 〈l〉) →
    (perm_fun_lst f l) ⧓ l = map f l.

Fixpoint apply_fun f e :=
  match e with
  | id A ⇒ id (map f A)
  | ⊥ A ⇒ ⊥ (map f A)
  | var x ⇒ (perm_fun_lst f (τ x))•var x
  | vat a ⇒ vat (f a)
  | e1 + e2 ⇒ apply_fun f e1 + apply_fun f e2
  | e1 · e2 ⇒ apply_fun f e1 · apply_fun f e2
  | e^* ⇒ (apply_fun f e)^*
  | ν a e ⇒ ν (f a) (apply_fun f e)
  | ω a e ⇒ ω (f a) (apply_fun f e)
  | ‹ p › e ⇒ ‹ map_pair f p › apply_fun f e
  | _ ⇒ e
  end.

Lemma apply_φ_restr e : is_restr (apply_fun φ e).

Lemma map_φ_inj l m : l ≈ m ↔ map φ l ≈ map φ m.
Lemma NoDup_map_φ l : NoDup (map φ l) ↔ NoDup l.
Lemma apply_φ_no_perm e : no_perm e ↔ no_perm (apply_fun φ e).
Lemma apply_φ_multi e : multi e ↔ multi (apply_fun φ e).
Lemma apply_φ_single e : single e ↔ single (apply_fun φ e).
Lemma apply_φ_untyped e : untyped e ↔ untyped (apply_fun φ e).
Lemma apply_φ_has_type e A : A ⊨ e ↔ map φ A ⊨ (apply_fun φ e).

Lemma apply_φ_str_positive e :
  str_positive e ↔ str_positive (apply_fun φ e).
Lemma apply_φ_positive e :
  positive e ↔ positive (apply_fun φ e).
Lemma elements_map_pair f p :
  elements (map_pair f p) ≈ map f (elements p).
Lemma equiv_perm_map_φ p q : p ≌ q ↔ map_pair φ p ≌ map_pair φ q.

Lemma apply_φ_eq_expr e f :
  (e == f) ↔ (apply_fun φ e == apply_fun φ f).

Lemma apply_φ_support e : support (apply_fun φ e) ≈ map φ (support e).

Lemma apply_φ_stage e : stage (apply_fun φ e) ≈ map φ (stage e).

Lemma apply_φ_fresh e a : a # e ↔ φ a # (apply_fun φ e).

Lemma app_length_eq A :
  ∀ (l m n o: list A),
    l++m=n++o ∧ length l = length n → l = n ∧ m = o.
Lemma φ_lst_act l a : In a l → perm_fun_lst φ l ⋈ a = φ a.

Fixpoint all_atoms e :=
  match e with
  | 0 | 1 ⇒ []
  | bot A | id A ⇒ A
  | var x ⇒ τ x
  | vat a ⇒ [a]
  | e + f | e · f ⇒ (all_atoms e) ++ (all_atoms f)
  | e ^* ⇒ (all_atoms e)
  | ‹ p › e ⇒ (elements p)++(all_atoms e)
  | ν a e | ω a e ⇒ a::(all_atoms e)
  end.
Lemma φ_lst_incl_mact l m : l⊆m → (perm_fun_lst φ m) ⧓ l = map φ l.
Lemma apply_φ_apply_perm e l : (all_atoms e) ⊆ l → no_perm e →
                apply_fun φ e == (perm_fun_lst φ l) • e.
Lemma apply_perm_app p q e : (p++q)•e == p • (q • e).

Lemma aux e l : (all_atoms e) ⊆ l → no_perm e →
                FFalse ⊢ apply_fun φ e ≡ (perm_fun_lst φ l) • e.
Lemma aux2 e l : (all_atoms e) ⊆ l → no_perm e →
                 FFalse ⊢ e ≡(perm_fun_lst φ l)⋆ • apply_fun φ e.

Lemma apply_φ_eq_ax (ax : relation expr) :
  (∀ e f, ax e f → ax ⊢ apply_fun φ e ≡ apply_fun φ f) →
  ∀ e f, ax ⊢ e ≡ f → ax ⊢ apply_fun φ e ≡ apply_fun φ f.

Definition restr_ax ax := fun e f ⇒
                            ax e f ∧ is_restr e ∧ is_restr f.

Lemma restr_ax_eq_ax_eq ax e f :
  restr_ax ax ⊢ e ≡ f → ax ⊢ e ≡ f.

Definition ex_ax_eq ax : relation expr :=
  fun e f ⇒ ∃ g, ax e g ∧ (g==f) ∧ (is_restr g ↔ is_restr f).
Lemma proper_ex_ax_eq ax ψ :
  Proper (ax ==> ax) ψ →
  Proper (ax ==> ex_ax_eq ax) ψ.
Lemma ax_eq_restr_ax_eq ax :
  Proper (ax ==> ex_ax_eq ax) (apply_fun φ) →
  Proper (eq ax ==> eq (restr_ax ax)) (apply_fun φ).

Lemma zero_ka_u_apply_φ : Proper (zero_ka_u ==> zero_ka_u) (apply_fun φ).

Lemma zero_ka_t_apply_φ : Proper (zero_ka_t ==> zero_ka_t) (apply_fun φ).

Lemma zero_perm_u_apply_φ :
  Proper (zero_perm_u ==> zero_perm_u) (apply_fun φ).

Lemma zero_perm_t_apply_φ :
  Proper (zero_perm_t ==> zero_perm_t) (apply_fun φ).

Lemma zero_nom_u_apply_φ : Proper (zero_nom_u ==> zero_nom_u) (apply_fun φ).

Lemma zero_nom_t_apply_φ : Proper (zero_nom_t ==> zero_nom_t) (apply_fun φ).

Lemma eq_perm_apply_φ : Proper (eq_perm ==> eq_perm) (apply_fun φ).

Lemma eq_perm_ω_apply_φ : Proper (eq_perm_ω ==> eq_perm_ω) (apply_fun φ).

Lemma eq_perm_elim_apply_φ :
  Proper (eq_perm_elim ==> ex_ax_eq eq_perm_elim) (apply_fun φ).

Lemma eq_ν_smpl_apply_φ : Proper (eq_ν_smpl ==> eq_ν_smpl) (apply_fun φ).
Lemma eq_ω_smpl_apply_φ : Proper (eq_ω_smpl ==> eq_ω_smpl) (apply_fun φ).

Lemma eq_nom_untyped_p_apply_φ :
  Proper (eq_nom_untyped_p ==> eq_nom_untyped_p) (apply_fun φ).
Lemma apply_φ_apply_perm_p p e :
  apply_fun φ (p • e) == (map_pair φ p) • (apply_fun φ e).

Lemma restr_perm_is_restr :
  (∀ p e, restr_perm p = true → is_restr (p•apply_fun φ e)).
Lemma eq_nom_untyped_np_apply_φ :
  Proper (eq_nom_untyped_np ==> ex_ax_eq eq_nom_untyped_np) (apply_fun φ).
Lemma eq_nom_untyped_apply_φ :
  Proper (eq_nom_untyped ==> eq_nom_untyped) (apply_fun φ).
Lemma eq_nom_typed_p_apply_φ :
  Proper (eq_nom_typed_p ==> eq_nom_typed_p) (apply_fun φ).

Lemma eq_nom_typed_np_apply_φ :
  Proper (eq_nom_typed_np ==> ex_ax_eq eq_nom_typed_np) (apply_fun φ).

Lemma eq_nom_typed_apply_φ :
  Proper (eq_nom_typed ==> eq_nom_typed) (apply_fun φ).

Lemma is_restr_stable ax e f :
  no_perm e → no_perm f →
  Proper (ax ==> iff) no_perm →
  restr_ax ax ⊢ e ≡ f → is_restr e ↔ is_restr f.

Lemma apply_perm_eq ax e f p:
  (∀ p, Proper (ax ==> eq ax) (apply_perm p))
  → ax ⊢ e ≡ f → ax ⊢ p•e≡p•f.

Lemma apply_fun_comp f g e :
  (∀ l, NoDup l → NoDup (map g l)) →
  (∀ l, NoDup l → NoDup (map f (map g l))) →
  apply_fun f (apply_fun g e) == apply_fun (f ∘ g) e.

Lemma apply_fun_id e : apply_fun (fun x ⇒ x) e == e.
Lemma apply_fun_ext f g e : (∀ x, f x = g x) →
                            apply_fun f e = apply_fun g e.
Lemma apply_ψ_φ_id e : apply_fun ψ (apply_fun φ e) == e.
Lemma elements_In :
  ∀ p x,
    In x (elements p) ↔ ∃ y, In y p ∧ (x=fst y ∨ x = snd y).
Lemma equiv_perm_map_ψ p q :
  restr_perm p = true →restr_perm q = true →
  p ≌ q ↔ map_pair ψ p ≌ map_pair ψ q.

Lemma apply_fun_morph : Proper (restr_ax eq_expr ==> eq_expr)
                               (apply_fun ψ).

Lemma ψ_surj : ∀ x, ∃ y, ψ y = x.
Lemma ψ_inj_implies_φ_surj : (∀ x y, ψ x = ψ y → x = y)
                             → ∀ x, X x.