# Library predicates

Equality of expressions modulo equivalence of letters.
Reserved Notation " e == f " (at level 100).
Fixpoint eq_expr e f : Prop :=
match (e,f) with
| (0,0) | (1,1)True
| (var x,var y)x y
| (vat a,vat b)a = b
| ( l, m) | (id l,id m)l m
| (e^*,f^* ) ⇒ (e == f)
| (e+e',f+f') | (e·e',f·f')(e == f)/\(e' == f')
| (ν a e,ν b f) | (ω a e,ω b f)(e == f)/\(a = b)
| (pe,qf)(e == f)/\(p q)
| _False
end
where " e == f " := (eq_expr e f).
Global Instance eq_expr_Equivalence : Equivalence eq_expr.

Lemma eq_expr_W l : Proper (eq_expr ==> eq_expr) (W l).
Lemma eq_expr_size : Proper (eq_expr ==> Logic.eq) size.
Lemma eq_expr_support : Proper (eq_expr ==> equiv_lst) support.
Lemma eq_expr_stage : Proper (eq_expr ==> equiv_lst) stage.
Lemma eq_expr_eq0 : Proper (eq_expr ==> Logic.eq) eq0.
Lemma eq_expr_eq0' : Proper (eq_expr ==> Logic.eq) eq0'.
Lemma eq_expr_get_bot e f :
(e == f)
(get_bot e = get_bot f)
a b, get_bot e = inr a get_bot f = inr b ab.
Boolean equality.
Fixpoint beq_expr e f : bool :=
match (e,f) with
| (0,0) | (1,1)true
| (var x,var y)beq_letter x y
| (vat a,vat b)beq_atom a b
| ( l, m) | (id l,id m)equiv_lst_b l m
| (e^*,f^* )beq_expr e f
| (e+e',f+f') | (e·e',f·f')(beq_expr e f)&&(beq_expr e' f')
| (ν a e,ν b f) | (ω a e,ω b f)(beq_expr e f)&&(beq_atom a b)
| (pe,qf)(beq_expr e f)&&(bequiv_perm p q)
| _false
end.
Lemma beq_expr_spec e f : reflect (e==f) (beq_expr e f).

# Typing jugements

Reserved Notation "A ⊨ e" (at level 30).
Fixpoint has_type A e : Prop :=
match e with
| B | id BA B
| var aA (τ a)
| vat aA [a]
| (e + f) | (e · f) ⇒ A e A f
| (e^* ) ⇒ A e
| (p e) ⇒ (p A)⊨ e
| (ν a e) ⇒ ¬ In a A (a::A) e
| (ω a e) ⇒ In a A (rm a A)⊨ e
| 0 | 1False
end
where "A ⊨ e" := (has_type A e).
Definition typed e := ( A, A e).
Definition ty' e f := ( A, A e A f).
Definition ty := typed^2.
Fixpoint typedb e :=
match e with
| B | id Btrue
| var atrue
| vat atrue
| (e + f) | (e · f) ⇒
typedb e && typedb f && (equiv_lst_b (stage e) (stage f))
| (e^* ) | (_ e) ⇒ typedb e
| (ν a e) ⇒ inb a (stage e) && typedb e
| (ω a e) ⇒ negb (inb a (stage e)) && typedb e
| 0 | 1false
end.

Key lemma for simplification.
Lemma ht_convert A B e :
(A B) A e B e.
Global Instance ht_equiv e :
Proper (equiv_lst ==> iff) (Basics.flip has_type e).
Global Instance ht_equiv_iff :
Proper (equiv_lst ==> Logic.eq ==> iff) has_type.
Global Instance ht_bot_eq A :
Proper (equiv_lst ==> iff) (fun lA (bot l)).
Global Instance ht_id_eq A :
Proper (equiv_lst ==> iff) (fun lA (id l)).
If an expression can be typed, then its type is equivalent to its stage.

# Untyped expressions

Fixpoint untyped e : Prop :=
match e with
| var _ | vat _ | 1 | 0True
| _ | id _ | ω _ _False
| ν _ e | _ e | e ^*untyped e
| e + f | e · funtyped e untyped f
end.
Definition ut := untyped^2.
Fixpoint untypedb e : bool :=
match e with
| var _ | vat _ | 1 | 0true
| _ | id _ | ω _ _false
| ν _ e | _ e | e ^*untypedb e
| e + f | e · funtypedb e && untypedb f
end.
Lemma untypedb_spec e : reflect (untyped e) (untypedb e).
Lemma decidable_untyped e : untyped e ¬ untyped e.

# Strictly positive expressions

str_positive expressions do not contain 0 or constructors.
Fixpoint str_positive e : Prop :=
match e with
| var _ | vat _ | 1 | id _True
| _ | 0False
| ω _ e | ν _ e | _ e | e ^*str_positive e
| e + f | e · fstr_positive e str_positive f
end.
Fixpoint str_positiveb e : bool :=
match e with
| var _ | vat _ | 1 | id _true
| _ | 0false
| ω _ e | ν _ e | _ e | e ^*str_positiveb e
| e + f | e · fstr_positiveb e && str_positiveb f
end.
Definition sp := str_positive^2.
Lemma str_positiveb_spec e : reflect (str_positive e) (str_positiveb e).
Lemma decidable_str_positive :
e, str_positive e ¬ str_positive e.

positive expressions are either equal to 0 or , or are str_positive.
Definition positive e : Prop :=
match e with
| _ | 0True
| _str_positive e
end.
Definition positiveb e : bool :=
match e with
| _ | 0true
| _str_positiveb e
end.
positiveb is a boolean function testing the predicate positive.
This entails the decidability of the predicate positive.
Lemma decidable_positive :
e, positive e ¬ positive e.
Definition po := positive^2.
str_positive entails positive.
An expression is positive if and only if it is either strictly positive or equal to 0 or some A.

# Freshness

Reserved Notation "a # e" (at level 75).
Reserved Notation "a #' e" (at level 75).
Fixpoint fresh a e :=
match e with
| var x¬ In a (τ x)
| vat xa x
| 0 | 1 | _ | id _True
| e + f | e · fa # e a # f
| e ^* | ω _ ea # e
| ν b ea = b a # e
| p e(pa) # e
end
where "a # e" := (fresh a e).
Fixpoint freshb a e :=
match e with
| var xnegb (inb a (τ x))
| vat xnegb (beq_atom a x)
| 0 | 1 | _ | id _true
| e + f | e · f(a #' e) && (a #' f)
| e ^* | ω _ ea #' e
| ν b e(beq_atom a b) || (a #' e)
| p e(pa) #' e
end
where "a #' e" := (freshb a e).
Lemma freshb_spec a e : reflect (a # e) (a #' e).

# Expressions with variables over Letters.

Fixpoint multi e : Prop :=
match e with
| var _ | un | zero | id _ | bot _True
| plus e f | times e fmulti e multi f
| star e | ν _ e | ω _ e | θ _ emulti e
| vat _False
end.
Definition mlt := multi^2.
Fixpoint multib e :=
match e with
| var _ | un | zero | id _ | bot _true
| plus e f | times e fmultib e && multib f
| star e | ν _ e | ω _ e | θ _ emultib e
| vat _false
end.
Lemma multib_spec e : reflect (multi e) (multib e).
Lemma decidable_multi : e, multi e ¬ multi e.

# Expressions with variables over Atoms

Fixpoint single e : Prop :=
match e with
| vat _ | un | zero | id _ | bot _True
| plus e f | times e fsingle e single f
| star e | ν _ e | ω _ e | θ _ esingle e
| var _False
end.
Definition sg := single^2.
Fixpoint singleb e :=
match e with
| vat _ | un | zero | id _ | bot _true
| plus e f | times e fsingleb e && singleb f
| star e | ν _ e | ω _ e | θ _ esingleb e
| var _false
end.
Lemma singleb_spec e : reflect (single e) (singleb e).
Lemma decidable_single : e, single e ¬ single e.

Atomic expressions have a support smaller than their size.

# Expressions not using permutations

Fixpoint no_perm e : Prop :=
match e with
| var _ | vat _ | un | zero | id _ | bot _True
| _ _False
| plus e f | times e fno_perm e no_perm f
| star e | ν _ e | ω _ eno_perm e
end.
Definition np := no_perm^2.
Fixpoint no_permb e :=
match e with
| var _ | vat _ | un | zero | id _ | bot _true
| _ _false
| plus e f | times e fno_permb e && no_permb f
| star e | ν _ e | ω _ eno_permb e
end.
Lemma no_permb_spec e : reflect (no_perm e) (no_permb e).
Lemma decidable_no_perm : e, no_perm e ¬ no_perm e.

lemmas about eq0' and get_bot when the argument is untyped
Lemma eq0'_u_spec {e} : untyped e reflect (e = 0) (eq0' e).
Lemma get_bot_u_spec {e} :
untyped e
reflect3 (e = 0) (fun BFalse) (e0) (get_bot e).
Lemma eq0'_get_bot_positiveu e :
untyped e ¬ (e = 0)
eq0' e = false get_bot e = inl true.
lemmas about eq0' and get_bot when the argument is typed
Lemma eq0'_t_spec {e A} : A e
reflect ( B, e= B) (eq0' e).
Lemma get_bot_t_spec {e A} : A e
reflect3 (False) (fun Be = B) (eq0' e = false) (get_bot e).
Lemma eq0'_get_bot_positivet e A :
A e
¬ ( B : list Atom, e = B)
eq0' e = false get_bot e = inl true.

# Facts about expressions.

All types associated with a given expression are equivalent.
Lemma type_unicity e :
A B, A e B e (A B).
Technical lemma about types.
Lemma type_eq_cons :
e a A B, (a::A) e (a::B) e
¬ In a A ¬ In a B A B.

An atom is fresh for e if and only if it is not free in e.
Lemma fresh_support a e : a # e (¬ (In a (support e))).

# Properties of W

If l is without duplication and if e can be typed by a list disjoint from l, then W l e can be typed.
Lemma W_type :
l A e, (A -- l) e l A NoDup l A W l e.

If W l e can be typed, then so can e.
Lemma type_W' : l A e, A W l e (A -- l) e.
W perserves no_perm,single,multi and str_positive.
Lemma no_perm_W : e l, no_perm e no_perm (W l e).
Lemma single_W : e l, single e single (W l e).
Lemma multi_W : e l, multi e multi (W l e).
Lemma str_positive_W :
e l, str_positive e str_positive (W l e).