# Definitions, notations and simplification tactics.

Type of expressions
Inductive expr : Type :=
| bot : (list Atom) expr
| id : (list Atom) expr
| zero : expr
| un : expr
| var : Letter expr
| vat : Atom expr
| plus : expr expr expr
| times : expr expr expr
| star : expr expr
| ν : Atom expr expr
| ω : Atom expr expr
| θ : perm expr expr.
Notation " ⊥ A " := (bot A) (at level 20).
Notation " 0 " := zero (at level 20).
Notation " 1 " := un (at level 20).
Notation "x + y" := (plus x y) (left associativity, at level 50).
Notation "x · y" := (times x y) (left associativity, at level 40).
Notation "x ^*" := (star x) (at level 20).
Notation " ‹ p › x" := (θ p x) (at level 20).

The size of an expression is its number of constructors.
Fixpoint size e : nat :=
match e with
| 0 | 1 | var _ | vat _ | bot _ | id _ ⇒ (S O)%nat
| e + f | e · fS (size e + size f)
| e ^* | ν _ e | _ e | ω _ eS (size e)
end.

Lemma size_non_zero : e, O < size e.

It is convenient to write weakennings in bulk.
Definition W l e := fold_right (fun a eω a e) e l.
Compositions of W may be factored with list concatenation.
Lemma W_app : l1 l2 e, W l1 (W l2 e) = W (l1++l2)e.
The size of W l e is the sum of the size of e and the length of l.
Lemma size_W : e l, size (W l e) = (length l + size e)%nat.

# The support of an expression computes the set of

its free variables.
Fixpoint support e :=
match e with
| 0 | 1[]
| bot _ | id _[]
| var xτ x
| vat a[a]
| e + f | e · f(support e) ++ (support f)
| e ^* ⇒ (support e)
| p ep (support e)
| ν a erm a (support e)
| ω a e ⇒ (support e)
end.
Definition Bs A e f := (support e support f) A e f.

Section poly.
Parameter K : nat.
Hypothesis K_not_zero : O < K.
Hypothesis bounded_τ : x, length (τ x) K.
Lemma length_support_size e : length (support e) (K × size e)%nat.
End poly.

# The stage of an expression computes its sheaf.

Fixpoint stage e :=
match e with
| 0 | 1[]
| bot A | id AA
| var xτ x
| vat a[a]
| e + f | e · f(stage e) ++ (stage f)
| e ^* ⇒ (stage e)
| p ep (stage e)
| ν a erm a (stage e)
| ω a ea::(stage e)
end.

# eq0 tests if an expression is equivalent to 0 or ⊥_.

Fixpoint eq0 e : bool :=
match e with
| 0 | bot _true
| _^* | 1 | id _ | var _ | vat _false
| e + feq0 e && eq0 f
| e · feq0 e || eq0 f
| ν _ e | _ e | ω _ eeq0 e
end.

# eq0' tests if an expression is equal to 0 or ⊥_.

Definition eq0' e : bool :=
match e with
| 0 | bot _true
| _false
end.
Lemma eq0'_spec e : reflect (e = 0 ( B, e = B)) (eq0' e).

Definition get_bot e :=
match e with
| Ainr A
| 0inl false
| _inl true
end.

Lemma get_bot_spec e : reflect3 (e = 0) (fun Be = B)
(eq0' e = false) (get_bot e).

Lemma eq0'_get_bot_positive e :
¬ (e = 0 ( B : list Atom, e = B))
eq0' e = false get_bot e = inl true.