Top.SystemC.CaptureSets

The source of this file can be found on Github.

This file implements Capture Sets, a.k.a a record of free and bound variables, captured by a particular value.

Definition of Capture Sets

A captureset -- a record of:

• free variables (atoms)
• bound variables (nats)
• and runtime labels (labels)

Inductive cap : Type :=
  | cset_set : atoms → nats → labels → cap.

Smart Constructors

Definition empty_cset := cset_set {} {}N {}L.

The empty set may be written similarly to informal practice.

Notation "{}C" := empty_cset : metatheory_scope.

Singleton Sets

Definition cset_fvar (a : atom) :=
  (cset_set (AtomSet.F.singleton a) NatSet.F.empty LabelSet.F.empty).

Definition cset_bvar (k : nat) :=
  (cset_set AtomSet.F.empty (NatSet.F.singleton k) LabelSet.F.empty).

Definition cset_lvar (a : label) :=
  (cset_set AtomSet.F.empty NatSet.F.empty (LabelSet.F.singleton a)).

Definition from_labels (ls : labels) :=
  (cset_set AtomSet.F.empty NatSet.F.empty ls).

Selectors

Definition cset_fvars (c : cap) : atoms :=
  match c with
  | cset_set A N R ⇒ A
  end.

Definition cset_bvars (c : cap) : nats :=
  match c with
  | cset_set A N R ⇒ N
  end.

Definition cset_lvars (c : cap) : labels :=
  match c with
  | cset_set A N R ⇒ R
  end.

Operations

Predicates for determining if a capture set explicity references a variable -- used for determining if a capture set is well formed. Don't use these predicates for determining if a capture set captures a variable, as one needs to also test cset_universal.

Definition cset_references_bvar (k : nat) (c : cap) :=
  NatSet.F.In k (cset_bvars c).

Definition cset_references_fvar (a : atom) (c : cap) :=
  AtomSet.F.In a (cset_fvars c).

Definition cset_references_lvar (a : label) (c : cap) :=
  LabelSet.F.In a (cset_lvars c).

Definition cset_references_bvar_dec (k : nat) (c : cap) :=
  NatSet.F.mem k (cset_bvars c).

Definition cset_references_fvar_dec (a : atom) (c : cap) :=
  AtomSet.F.mem a (cset_fvars c).

Definition cset_references_lvar_dec (a : label) (c : cap) :=
  LabelSet.F.mem a (cset_lvars c).

Definition cset_remove_bvar (k : nat) (c : cap) : cap :=
  cset_set (cset_fvars c) (NatSet.F.remove k (cset_bvars c)) (cset_lvars c).

Definition cset_remove_fvar (a : atom) (c : cap) : cap :=
  cset_set (AtomSet.F.remove a (cset_fvars c)) (cset_bvars c) (cset_lvars c).

Capture set unions are what you'd expect.

Definition cset_union (c1 c2 : cap) : cap :=
  cset_set
    (AtomSet.F.union (cset_fvars c1) (cset_fvars c2))
    (NatSet.F.union (cset_bvars c1) (cset_bvars c2))
    (LabelSet.F.union (cset_lvars c1) (cset_lvars c2)).

Definition cset_subset_dec (C D : cap) :=
  AtomSet.F.subset (cset_fvars C) (cset_fvars D)
    && NatSet.F.subset (cset_bvars C) (cset_bvars D)
    && LabelSet.F.subset (cset_lvars C) (cset_lvars D).

Logical Predicates

Definition cset_empty (c : cap) : Prop :=
  AtomSet.F.Empty (cset_fvars c) ∧ NatSet.F.Empty (cset_bvars c) ∧ LabelSet.F.Empty (cset_lvars c).

Definition cset_subset_prop (c : cap) (d : cap) : Prop :=
  AtomSet.F.Subset (cset_fvars c) (cset_fvars d)
    ∧ NatSet.F.Subset (cset_bvars c) (cset_bvars d)
    ∧ LabelSet.F.Subset (cset_lvars c) (cset_lvars d).

Properties

Section Props.

  Variable x y a f : atom.
  Variable l m : label.
  Variable A A1 A2 : atoms.
  Variable R R1 R2 : labels.
  Variable k n : nat.
  Variable N N1 N2 : nats.
  Variable C D C1 C2 C3 : cap.

  Lemma cset_bvar_mem_iff :
    cset_references_bvar k C ↔ cset_references_bvar_dec k C = true.

  Lemma cset_fvar_mem_iff :
    cset_references_fvar a C ↔ cset_references_fvar_dec a C = true.

  Lemma cset_lvar_mem_iff :
    cset_references_lvar l C ↔ cset_references_lvar_dec l C = true.

  Lemma cset_bvar_not_mem_iff :
    ¬ cset_references_bvar k C ↔ cset_references_bvar_dec k C = false.

  Lemma cset_fvar_not_mem_iff :
    ¬ cset_references_fvar a C ↔ cset_references_fvar_dec a C = false.

  Lemma cset_lvar_not_mem_iff :
    ¬ cset_references_lvar l C ↔ cset_references_lvar_dec l C = false.

  Lemma fvars_1 : cset_fvars (cset_set A N R) = A.

  Lemma bvars_1 : cset_bvars (cset_set A N R) = N.

  Lemma lvars_1 : cset_lvars (cset_set A N R) = R.

  Lemma fvars_union_1 : cset_fvars (cset_union C D) = AtomSet.F.union (cset_fvars C) (cset_fvars D).

  Lemma bvars_union_1 : cset_bvars (cset_union C D) = NatSet.F.union (cset_bvars C) (cset_bvars D).

  Lemma lvars_union_1 : cset_lvars (cset_union C D) = LabelSet.F.union (cset_lvars C) (cset_lvars D).

  Lemma remove_fvar_1 : cset_remove_fvar x (cset_set A N R) = (cset_set (AtomSet.F.remove x A) N R).

  Lemma remove_bvar_1 : cset_remove_bvar k (cset_set A N R) = (cset_set A (NatSet.F.remove k N) R).

  Lemma mem_bvar_1 : cset_references_bvar k C → cset_references_bvar_dec k C = true.

  Lemma mem_bvar_2 : cset_references_bvar_dec k C = true → cset_references_bvar k C.

  Lemma mem_fvar_1 : cset_references_fvar a C → cset_references_fvar_dec a C = true.

  Lemma mem_fvar_2 : cset_references_fvar_dec a C = true → cset_references_fvar a C.

  Lemma mem_lvar_1 : cset_references_lvar l C → cset_references_lvar_dec l C = true.

  Lemma mem_lvar_2 : cset_references_lvar_dec l C = true → cset_references_lvar l C.

  Lemma In_bvar_1 : k = n → cset_references_bvar k C → cset_references_bvar n C.

  Lemma In_fvar_1 : a = f → cset_references_fvar a C → cset_references_fvar f C.

  Lemma In_lvar_1 : l = m → cset_references_lvar l C → cset_references_lvar m C.

  Lemma Is_empty : cset_empty empty_cset.

  Lemma union_fvar_1 : cset_references_fvar x (cset_union C D) → cset_references_fvar x C ∨ cset_references_fvar x D.

  Lemma union_fvar_2 : cset_references_fvar x C → cset_references_fvar x (cset_union C D).

  Lemma union_fvar_3 : cset_references_fvar x D → cset_references_fvar x (cset_union C D).

  Lemma union_bvar_1 : cset_references_bvar k (cset_union C D) → cset_references_bvar k C ∨ cset_references_bvar k D.

  Lemma union_bvar_2 : cset_references_bvar k C → cset_references_bvar k (cset_union C D).

  Lemma union_bvar_3 : cset_references_bvar k D → cset_references_bvar k (cset_union C D).

  Lemma union_lvar_1 : cset_references_lvar l (cset_union C D) → cset_references_lvar l C ∨ cset_references_lvar l D.

  Lemma union_lvar_2 : cset_references_lvar l C → cset_references_lvar l (cset_union C D).

  Lemma union_lvar_3 : cset_references_lvar l D → cset_references_lvar l (cset_union C D).

  Lemma union_sub_1 : cset_subset_prop C D → cset_union D C = D.

  Lemma union_sub_2 : cset_subset_prop C D → D = cset_union D C.

  Lemma union_subset_distribute_1 : cset_subset_prop C1 C2 → cset_subset_prop (cset_union C1 D) (cset_union C2 D).

End Props.

(* TODO defined here to avoid all the implicit arguments *)
Lemma subset_lvar_1 : ∀ R C l,
  cset_subset_prop R C → cset_references_lvar l R → cset_references_lvar l C.

Lemma from_empty_labels_is_empty :
  (from_labels {}L) = {}C.




(* *** Some subset properties *)
Lemma subset_refl : ∀ C,
  cset_subset_prop C C.

Lemma subset_union_left : ∀ C1 C2,
  cset_subset_prop C1 (cset_union C1 C2).

Lemma subset_union_right : ∀ C1 C2,
  cset_subset_prop C2 (cset_union C1 C2).

Lemma subset_trans : ∀ A B C,
  cset_subset_prop A B → cset_subset_prop B C → cset_subset_prop A C.

Locally Namelesss

Definition capt (c : cap) : Prop := NatSet.F.Empty (cset_bvars c).

Lemma singleton_closed : ∀ f,
  capt (cset_fvar f).

Lemma capt_empty_bvar : ∀ A N R,
  capt (cset_set A N R) →
  N = {}N.

Opening a capture set with a bound variable dk → c

Definition open_cset (k : nat) (c : cap) (d : cap) : cap :=
  if cset_references_bvar_dec k d then
    cset_union c (cset_remove_bvar k d)
  else
    d.

Substituting a capture set with a free variable da → c

Definition subst_cset (a : atom) (c : cap) (d: cap) : cap :=
  if cset_references_fvar_dec a d then
    cset_union c (cset_remove_fvar a d)
  else
    d.

Lemma subst_over_subset : ∀ C1 C2 D x,
  cset_subset_prop C1 C2 →
  cset_subset_prop (subst_cset x D C1) (subst_cset x D C2).

Lemma subst_subset_intro : ∀ C1 C2 x,
  (* C1 is closed *)
  capt C1 →
  cset_subset_prop (cset_fvar x) C2 →
  cset_subset_prop C1 (subst_cset x C1 C2).

Lemma subst_cset_union : ∀ x D C1 C2,
  subst_cset x D (cset_union C1 C2) = (cset_union (subst_cset x D C1) (subst_cset x D C2)).

Lemma subst_cset_singleton : ∀ x C,
  subst_cset x C (cset_fvar x) = C.

Lemma subst_cset_fresh : ∀ x C1 C2,
  x `notin` (cset_fvars C1) →
  C1 = subst_cset x C2 C1.

Lemma singleton_lvar : ∀ l,
  cset_references_lvar l (cset_lvar l).

Lemma subst_cset_fresh_id : ∀ x X C,
  x ≠ X →
  (subst_cset X C (cset_fvar x)) = (cset_fvar x).

Lemma subst_cset_union_id : ∀ x y D C1,
  x ≠ y →
  subst_cset x D (cset_union C1 (cset_fvar y)) = (cset_union (subst_cset x D C1) (cset_fvar y)).

Lemma subst_cset_lvar : ∀ x C l R,
  cset_references_lvar l R →
  cset_references_lvar l (subst_cset x C R).

Lemma subst_cset_lvar_idempotent : ∀ x C l,
  (subst_cset x C (cset_lvar l)) = (cset_lvar l).

Lemma open_cset_capt : ∀ i C c,
  capt C →
  C = open_cset i c C.

Lemma subst_cc_intro_rec : ∀ X (C : cap) U k,
  X `notin` (cset_fvars C) →
  open_cset k U C = subst_cset X U (open_cset k (cset_fvar X) C).


Lemma open_cset_rec_capt_aux : ∀ c j V i U,
  i ≠ j →
  capt V →
  (cset_fvars V) `disjoint` (cset_fvars U) →
  labels_disjoint (cset_lvars V) (cset_lvars U) →
  open_cset j V c = open_cset i U (open_cset j V c) →
  c = open_cset i U c.

Lemma subst_cset_open_cset_rec : ∀ x k C1 C2 D,
  capt C1 →
  subst_cset x C1 (open_cset k C2 D) = open_cset k (subst_cset x C1 C2) (subst_cset x C1 D).