# 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 xbeq_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 pmatch 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 Arestr_list A
| 0 | 1 | var _ | vat _true
| e + f | e · frestr_expr e && restr_expr f
| e ^*restr_expr e
| ν a e | ω a ein_X a && restr_expr e
| p erestr_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 Aid (map f A)
| A (map f A)
| var x(perm_fun_lst f (τ x))•var x
| vat avat (f a)
| e1 + e2apply_fun f e1 + apply_fun f e2
| e1 · e2apply_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 AA
| 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 ea::(all_atoms e)
end.
Lemma φ_lst_incl_mact l m : lm (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 (papply_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 pepf.

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 xx) 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.