Structural laws under π-calculus observers

InductiveOne-hole lexical process contexts#✓fully proved

One-hole lexical contexts, including guards, choice and replication.

inductive Context where
  | hole
  | out (a b : Name) (c : Context)
  | inp (a : Name) (c : Context)
  | parL (c : Context) (p : Proc)
  | parR (p : Proc) (c : Context)
  | nu (c : Context)
  | repl (c : Context)
  | sumL (c : Context) (p : Proc)
  | sumR (p : Proc) (c : Context)

Uses 2 · Used by 11

Statement usesChannel name in the π-calculus · Processes of the π-calculus

Used byContextual barbed equivalence implies barbed bisimilarity · Composition of process contexts · Contextual strong barbed equivalence · Structural congruence implies contextual barbed equivalence · Lexical filling of a process context · Structural congruence is closed under contexts · Contextual barbed equivalence is closed under contexts · Capture-avoiding filling of a process context · Structural laws are barbed sound in capture-avoiding contexts · Capture-avoiding and lexical filling agree on locally closed holes · Filling a composed context is iterated filling

DefinitionLexical filling of a process context#✓fully proved

Fill the lexical hole. Free constants are never captured; locally closed hole processes have no references into surrounding binders.

def Context.fill : Context → Proc → Proc
  | .hole, p => p
  | .out a b c, p => .out a b (c.fill p)
  | .inp a c, p => .inp a (c.fill p)
  | .parL c q, p => .par (c.fill p) q
  | .parR q c, p => .par q (c.fill p)
  | .nu c, p => .nu (c.fill p)
  | .repl c, p => .repl (c.fill p)
  | .sumL c q, p => .sum (c.fill p) q
  | .sumR q c, p => .sum q (c.fill p)

Uses 3 · Used by 7

Statement usesOne-hole lexical process contexts · Channel name in the π-calculus · Processes of the π-calculus

Used byContextual strong barbed equivalence · Structural congruence implies contextual barbed equivalence · Structural congruence is closed under contexts · Contextual barbed equivalence is closed under contexts · Structural laws are barbed sound in capture-avoiding contexts · Capture-avoiding and lexical filling agree on locally closed holes · Filling a composed context is iterated filling

TheoremStructural congruence is closed under contexts#✓fully proved

Structural congruence survives every one-hole lexical context.

theorem Cong.fill {p q : Proc} (h : Cong p q) (c : Context) :
    Cong (c.fill p) (c.fill q)

Uses 5 · Used by 1

Statement usesStructural congruence of π-calculus processes · One-hole lexical process contexts · Lexical filling of a process context · Processes of the π-calculus

Proof usesChannel name in the π-calculus

Used byStructural congruence implies contextual barbed equivalence

DefinitionComposition of process contexts#✓fully proved

Substitute a context into the hole of another context.

def Context.comp : Context → Context → Context
  | .hole, d => d
  | .out a b c, d => .out a b (c.comp d)
  | .inp a c, d => .inp a (c.comp d)
  | .parL c p, d => .parL (c.comp d) p
  | .parR p c, d => .parR p (c.comp d)
  | .nu c, d => .nu (c.comp d)
  | .repl c, d => .repl (c.comp d)
  | .sumL c p, d => .sumL (c.comp d) p
  | .sumR p c, d => .sumR p (c.comp d)

Uses 3 · Used by 2

Statement usesOne-hole lexical process contexts · Channel name in the π-calculus · Processes of the π-calculus

Used byContextual barbed equivalence is closed under contexts · Filling a composed context is iterated filling

TheoremFilling a composed context is iterated filling#✓fully proved

Context composition agrees with iterated filling.

@[simp] theorem Context.fill_comp (c d : Context) (p : Proc) :
    (c.comp d).fill p = c.fill (d.fill p)

Uses 5 · Used by 1

Statement usesOne-hole lexical process contexts · Composition of process contexts · Lexical filling of a process context · Processes of the π-calculus

Proof usesChannel name in the π-calculus

Used byContextual barbed equivalence is closed under contexts

DefinitionContextual strong barbed equivalence#✓fully proved

Strong barbed equivalence in every lexical process context. For capture-avoiding use, both hole processes must satisfy Proc.ClosedAt 0.

def ContextualBarbedEquiv (p q : Proc) : Prop :=
  ∀ c : Context, BarbedBisimilar (c.fill p) (c.fill q)

Uses 4 · Used by 3

Statement usesStrong barbed bisimilarity · One-hole lexical process contexts · Lexical filling of a process context · Processes of the π-calculus

Used byContextual barbed equivalence implies barbed bisimilarity · Structural congruence implies contextual barbed equivalence · Contextual barbed equivalence is closed under contexts

TheoremStructural congruence implies contextual barbed equivalence#✓fully proved

Structural congruence is sound under every observer context, with one-for-one reduction matching and immediate input/output barbs.

theorem Cong.contextualBarbedEquiv {p q : Proc} (h : Cong p q) :
    ContextualBarbedEquiv p q

Uses 7 · Used by 1

Statement usesStructural congruence of π-calculus processes · Contextual strong barbed equivalence · Processes of the π-calculus

Proof usesStructurally congruent processes are barbed bisimilar · Structural congruence is closed under contexts · One-hole lexical process contexts · Lexical filling of a process context

Used byStructural laws are barbed sound in capture-avoiding contexts

TheoremContextual barbed equivalence is closed under contexts#✓fully proved

Contextual barbed equivalence survives filling a context.

theorem ContextualBarbedEquiv.fill {p q : Proc}
    (h : ContextualBarbedEquiv p q) (d : Context) :
    ContextualBarbedEquiv (d.fill p) (d.fill q)

Uses 7

Statement usesOne-hole lexical process contexts · Lexical filling of a process context · Contextual strong barbed equivalence · Processes of the π-calculus

Proof usesStrong barbed bisimilarity · Composition of process contexts · Filling a composed context is iterated filling

TheoremContextual barbed equivalence implies barbed bisimilarity#✓fully proved

Contextual barbed equivalence implies standalone barbed bisimilarity.

theorem ContextualBarbedEquiv.barbedBisimilar {p q : Proc}
    (h : ContextualBarbedEquiv p q) : BarbedBisimilar p q

Uses 4

Statement usesStrong barbed bisimilarity · Contextual strong barbed equivalence · Processes of the π-calculus

Proof usesOne-hole lexical process contexts

DefinitionCapture-avoiding filling of a process context#✓fully proved

Capture-avoiding filling: each context binder shifts dangling names of the hole, while binders internal to the hole remain untouched.

def Context.fillAvoiding : Context → Proc → Proc
  | .hole, p => p
  | .out a b c, p => .out a b (c.fillAvoiding p)
  | .inp a c, p => .inp a (c.fillAvoiding (liftProc 0 p))
  | .parL c q, p => .par (c.fillAvoiding p) q
  | .parR q c, p => .par q (c.fillAvoiding p)
  | .nu c, p => .nu (c.fillAvoiding (liftProc 0 p))
  | .repl c, p => .repl (c.fillAvoiding p)
  | .sumL c q, p => .sum (c.fillAvoiding p) q
  | .sumR q c, p => .sum q (c.fillAvoiding p)

Uses 4 · Used by 2

Statement usesOne-hole lexical process contexts · Channel name in the π-calculus · Processes of the π-calculus · Lifting free de Bruijn indices of a π-calculus process

Used byStructural laws are barbed sound in capture-avoiding contexts · Capture-avoiding and lexical filling agree on locally closed holes

TheoremCapture-avoiding and lexical filling agree on locally closed holes#✓fully proved

Lexical and capture-avoiding filling agree for locally closed holes. This is the explicit admissibility condition for the contextual theorem.

theorem Context.fillAvoiding_eq {p : Proc} (h : Proc.ClosedAt 0 p)
    (c : Context) : c.fillAvoiding p = c.fill p

Uses 8 · Used by 1

Statement usesOne-hole lexical process contexts · Lexical filling of a process context · Capture-avoiding filling of a process context · Processes of the π-calculus · Locally closed processes at a binder depth

Proof usesChannel name in the π-calculus · Lifting free de Bruijn indices of a π-calculus process · Lifting fixes a locally closed process

Used byStructural laws are barbed sound in capture-avoiding contexts

TheoremStructural laws are barbed sound in capture-avoiding contexts#✓fully proved

Every structural law is strongly barbed sound under capture-avoiding contexts, for locally closed hole processes.

theorem Cong.fillAvoiding_barbedBisimilar {p q : Proc} (h : Cong p q)
    (hp : Proc.ClosedAt 0 p) (hq : Proc.ClosedAt 0 q) (c : Context) :
    BarbedBisimilar (c.fillAvoiding p) (c.fillAvoiding q)

Uses 9

Statement usesStrong barbed bisimilarity · Structural congruence of π-calculus processes · One-hole lexical process contexts · Capture-avoiding filling of a process context · Processes of the π-calculus · Locally closed processes at a binder depth

Proof usesStructural congruence implies contextual barbed equivalence · Lexical filling of a process context · Capture-avoiding and lexical filling agree on locally closed holes

12 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.