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)
  | (‹p›e,‹q›f) ⇒ (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 ∧ a≈b.
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)
  | (‹p›e,‹q›f) ⇒ (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 B ⇒ A ≈ B
  | var a ⇒ A ≈ (τ a)
  | vat a ⇒ A ≈ [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 | 1 ⇒ False
  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 B ⇒ true
  | var a ⇒ true
  | vat a ⇒ true
  | (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 | 1 ⇒ false
  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 l ⇒ A ⊨ (bot l)).
Global Instance ht_id_eq A :
  Proper (equiv_lst ==> iff) (fun l ⇒ A ⊨ (id l)).
If an expression can be typed, then its type is equivalent to its stage.

Lemma stage_has_type e A : A ⊨ e → A ≈ stage e.
Lemma typed_stage_has_type e : typed e → stage e ⊨ e.

Lemma typedb_spec e : reflect (typed e) (typedb e).
Lemma decidable_typed e : typed e ∨ ¬ typed e.


Untyped expressions

Fixpoint untyped e : Prop :=
  match e with
  | var _ | vat _ | 1 | 0 ⇒ True
  | ⊥ _ | id _ | ω _ _ ⇒ False
  | ν _ e | ‹_› e | e ^* ⇒ untyped e
  | e + f | e · f ⇒ untyped e ∧ untyped f
  end.
Definition ut := untyped^2.
Fixpoint untypedb e : bool :=
  match e with
  | var _ | vat _ | 1 | 0 ⇒ true
  | ⊥ _ | id _ | ω _ _ ⇒ false
  | ν _ e | ‹_› e | e ^* ⇒ untypedb e
  | e + f | e · f ⇒ untypedb 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
  | ⊥ _ | 0 ⇒ False
  | ω _ e | ν _ e |‹ _ › e | e ^* ⇒ str_positive e
  | e + f | e · f ⇒ str_positive e ∧ str_positive f
  end.
Fixpoint str_positiveb e : bool :=
  match e with
  | var _ | vat _ | 1 | id _ ⇒ true
  | ⊥ _ | 0 ⇒ false
  | ω _ e | ν _ e |‹ _ › e | e ^* ⇒ str_positiveb e
  | e + f | e · f ⇒ str_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
  | ⊥ _ | 0 ⇒ True
  | _ ⇒ str_positive e
  end.
Definition positiveb e : bool :=
  match e with
  | ⊥ _ | 0 ⇒ true
  | _ ⇒ str_positiveb e
  end.
positiveb is a boolean function testing the predicate positive.
Lemma positiveb_spec e : reflect (positive e) (positiveb e).
This entails the decidability of the predicate positive.
Lemma decidable_positive :
  ∀ e, positive e ∨ ¬ positive e.
Definition po := positive^2.
str_positive entails positive.
Lemma str_positive_positive e : str_positive e → positive e.

An expression is positive if and only if it is either strictly positive or equal to 0 or some ⊥ A.
Lemma pos_disj e :
  positive e ↔ (str_positive e ∨ e = 0 ∨ (∃ A, e = ⊥ 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 x ⇒ a ≠ x
  | 0 | 1 | ⊥ _ | id _ ⇒ True
  | e + f | e · f ⇒ a # e ∧ a # f
  | e ^* | ω _ e ⇒ a # e
  | ν b e ⇒ a = b ∨ a # e
  |‹ p › e ⇒ (p⋆⋈a) # e
  end
where "a # e" := (fresh a e).
Fixpoint freshb a e :=
  match e with
  | var x ⇒ negb (inb a (τ x))
  | vat x ⇒ negb (beq_atom a x)
  | 0 | 1 | ⊥ _ | id _ ⇒ true
  | e + f | e · f ⇒ (a #' e) && (a #' f)
  | e ^* | ω _ e ⇒ a #' e
  | ν b e ⇒ (beq_atom a b) || (a #' e)
  |‹ p › e ⇒ (p⋆⋈a) #' 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 f ⇒ multi e ∧ multi f
  | star e | ν _ e | ω _ e | θ _ e ⇒ multi 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 f ⇒ multib e && multib f
  | star e | ν _ e | ω _ e | θ _ e ⇒ multib 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 f ⇒ single e ∧ single f
  | star e | ν _ e | ω _ e | θ _ e ⇒ single 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 f ⇒ singleb e && singleb f
  | star e | ν _ e | ω _ e | θ _ e ⇒ singleb 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.
Lemma single_support_le_size e : single e → length (support e) ≤ size e.

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 f ⇒ no_perm e ∧ no_perm f
  | star e | ν _ e | ω _ e ⇒ no_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 f ⇒ no_permb e && no_permb f
  | star e | ν _ e | ω _ e ⇒ no_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 B ⇒ False) (e≠0) (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 B ⇒ e = ⊥ 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).