Library Labels

Require Import SfLib.
Require Import LibTactics.
Require Import NameSet.

Inductive label : Set :=
  | l_tau: label
  | l_in: name→label
  | l_out: name→label
  .

Delimit Scope label_scope with label.
Bind Scope label_scope with label.

Module Notation.
  Notation "'τ'" := (l_tau) (no associativity) : label_scope.
  Notation "a !" := (l_out a) (no associativity, at level 20, p at level 21, format "a !") : label_scope.
  Notation "a ?" := (l_in a) (no associativity, at level 20, p at level 21, format "a ?") : label_scope.
End Notation.

Definition fnl l : nameset := match l with
  | l_tau ⇒ NameSet.empty
  | l_in a ⇒ NameSet.singleton a
  | l_out a ⇒ NameSet.singleton a
  end.

Definition bnl l := match l with
  | l_tau ⇒ NameSet.empty
  | l_in a ⇒ NameSet.empty
  | l_out a ⇒ NameSet.empty
  end.

Definition nl l := NameSet.union (fnl l) (bnl l).

  Lemma label_eq_dec: ∀ (l1 l2: label) , {l1=l2}+{l1≠l2}.
  Proof. repeat decide equality. Qed.

  Lemma label_tau_deq: ∀ l, {l=l_tau}+{l≠l_tau}.
  Proof. intros; eapply label_eq_dec; eauto. Qed.

  Lemma label_eq (l1 l2: label): {l1=l2}+{l1≠l2}.
  Proof. decide equality; apply name_eq. Qed.

  Fixpoint interleaving {A:Type} (part: list (sum unit unit)) (l1 l2: list A) := match part with
  | inl tt::part ⇒ match l1 with
    | a::l1 ⇒ a::interleaving part l1 l2
    | _ ⇒ l2
    end
  | inr tt::part ⇒ match l2 with
    | a::l2 ⇒ a::interleaving part l1 l2
    | _ ⇒ l1
    end
  | _ ⇒ l1++l2
  end.

  Lemma interleaving_r_nil: ∀ {A:Type} lp la1,
    interleaving lp la1 (@nil A) = la1.
  Proof.
    induction lp; simpl; intros; auto.
    apply app_nil_r.
    destruct a; destruct u; auto. destruct la1; auto.
    congruence.
  Qed.

  Lemma interleaving_l_nil: ∀ {A:Type} lp l2,
    @interleaving A lp nil l2 = l2.
  Proof.
    induction lp; intros; simpl; auto.
    destruct a; destruct u; auto; destruct l2; auto; congruence.
  Qed.

  Lemma interleaving_com: ∀ {A:Type} lp l1 l2,
    (length lp = length l1 + length l2)%nat →
    @interleaving A (map (fun p ⇒ match p with inl tt ⇒ inr tt | inr tt ⇒ inl tt end) lp) l1 l2 = interleaving lp l2 l1.
  Proof.
    induction lp; intros; auto.
    destruct l1; destruct l2; simpl; auto; try solve [false; simpl in H; omega].
    destruct a; destruct u.
    destruct l1; destruct l2; simpl in *; auto.
    rewrite interleaving_l_nil; rewrite interleaving_r_nil; auto.
    rewrite IHlp; auto. simpl in ×. omega.
    destruct l1; destruct l2; simpl in *; auto.
    rewrite IHlp; auto.
    rewrite IHlp; auto.
  Qed.

  Lemma interleaving_app: ∀ {A:Type} l1 l2,
    @interleaving A (map (fun _⇒ inl tt) l1 ++ map (fun _⇒ inr tt) l2) l1 l2 = l1++l2.
  Proof. induction l1; simpl; intros; auto; f_equal; auto; apply interleaving_l_nil. Qed.