Library expr



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 · f ⇒ S (size e + size f)
    | e ^* | ν _ e | ‹ _ › e | ω _ e ⇒ S (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 › e ⇒ p ⧓ (support e)
  | ν a e ⇒ rm 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 A ⇒ A
  | var x ⇒ τ x
  | vat a ⇒ [a]
  | e + f | e · f ⇒ (stage e) ++ (stage f)
  | e ^* ⇒ (stage e)
  | ‹p› e ⇒ p ⧓ (stage e)
  | ν a e ⇒ rm a (stage e)
  | ω a e ⇒ a::(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 + f ⇒ eq0 e && eq0 f
    | e · f ⇒ eq0 e || eq0 f
    | ν _ e | ‹_› e | ω _ e ⇒ eq0 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
  | ⊥ A ⇒ inr A
  | 0 ⇒ inl false
  | _ ⇒ inl true
  end.

Lemma get_bot_spec e : reflect3 (e = 0) (fun B ⇒ e = ⊥ 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.