Concrete Trace Difference Transformer

This file formalizes the "Concrete Trace Differences" subsection of the note (Definition 2.6 and Proposition 2.7):

• DiffSys: the space of difference systems DS = (CCS × ProcSet) → TraceSet, ordered pointwise by subset inclusion.
• DTr: the concrete predecessor transformer D_Tr : 𝒳 → 𝒳, defined inductively on trace structure:
  • [] ∈ D_Tr(ρ)(p, Q) iff Q = ∅
  • a::tr' ∈ D_Tr(ρ)(p, Q) iff ∃ p' ∈ Der(p, a), tr' ∈ ρ(p', Der(Q, a))
• lfpDTr: the least fixpoint of DTr, defined as the intersection of all pre-fixpoints (Knaster–Tarski / Kleene characterisation).
• traceDifferenceToSet_eq_lfpDTr: the main result, establishing TraceDifferenceToSet env p Q = lfpDTr env p Q.

@[reducible, inline]

abbrev EqCheckingAbstractInterpretation.Trace.DiffSys (Action : Type u) (Name : Type v) : Type (max v u)

A difference system maps each pair (p, Q) to a set of traces (Def 2.6 in the note).

Equations

• One or more equations did not get rendered due to their size.

def EqCheckingAbstractInterpretation.Trace.DiffSysLe {Action : Type u} {Name : Type v} (ρ σ : DiffSys Action Name) : Prop

Pointwise order on difference systems: ρ ≤ σ iff ρ(p,Q) ⊆ σ(p,Q) for all (p,Q).

Equations

• One or more equations did not get rendered due to their size.

def EqCheckingAbstractInterpretation.Trace.DTr {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (ρ : DiffSys Action Name) (p : CCS.CCS Action Name) (Q : CCS.CCS Action Name → Prop) : Trace Action → Prop

The concrete predecessor transformer D_Tr (Definition 2.6).

DTr env ρ p Q tr is defined inductively on the structure of the trace tr:

• tr = [] (the empty observation ⊤): holds iff Q = ∅, because ⊤ is a distinguishing observation from the empty set of competitors.
• tr = a :: tr' (the prefixed observation ⟨a⟩tr'): holds iff there exists a successor p' ∈ Der(p, a) such that tr' ∈ ρ(p', Der(Q, a)), propagating distinguishing observations backward along derivatives.

Equations

• One or more equations did not get rendered due to their size.
• EqCheckingAbstractInterpretation.Trace.DTr env ρ p Q [] = ∀ (q : EqCheckingAbstractInterpretation.CCS.CCS Action Name), ¬Q q

theorem EqCheckingAbstractInterpretation.Trace.dTr_mono {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) {ρ σ : DiffSys Action Name} (hle : DiffSysLe ρ σ) (p : CCS.CCS Action Name) (Q : CCS.CCS Action Name → Prop) (tr : Trace Action) : DTr env ρ p Q tr → DTr env σ p Q tr

DTr env is monotone in ρ with respect to DiffSysLe.

def EqCheckingAbstractInterpretation.Trace.lfpDTr {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) : DiffSys Action Name

The least fixpoint of DTr env, defined proof-theoretically as the intersection of all pre-fixpoints. Equivalently, by Knaster–Tarski, this coincides with the least element ρ satisfying D_Tr(ρ) ⊆ ρ.

Equations

• One or more equations did not get rendered due to their size.

theorem EqCheckingAbstractInterpretation.Trace.lfpDTr_prefixpoint {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (p : CCS.CCS Action Name) (Q : CCS.CCS Action Name → Prop) (tr : Trace Action) : DTr env (lfpDTr env) p Q tr → lfpDTr env p Q tr

lfpDTr env is a pre-fixpoint: DTr env (lfpDTr env) ⊆ lfpDTr env.

theorem EqCheckingAbstractInterpretation.Trace.traceDiff_is_prefixpoint {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (p : CCS.CCS Action Name) (Q : CCS.CCS Action Name → Prop) (tr : Trace Action) : DTr env (TraceDifferenceToSet env) p Q tr → TraceDifferenceToSet env p Q tr

TraceDifferenceToSet env is a pre-fixpoint of DTr env. This is the key step (Part 2, "least among pre-fixpoints") in the proof of Proposition 2.7: any pre-fixpoint contains the concrete difference, so lfpDTr env ≤ TraceDifferenceToSet env.

theorem EqCheckingAbstractInterpretation.Trace.traceDiff_le_lfp {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (p : CCS.CCS Action Name) (Q : CCS.CCS Action Name → Prop) (tr : Trace Action) : TraceDifferenceToSet env p Q tr → lfpDTr env p Q tr

Part 1 of the proof of Proposition 2.7: the concrete trace difference is contained in every pre-fixpoint of DTr env, hence in lfpDTr env.

The proof uses TraceSem.rec with a motive that universally quantifies over Q, so that the induction hypothesis applies to the shifted set DerivSetOf env Q a in the cons case.

theorem EqCheckingAbstractInterpretation.Trace.traceDifferenceToSet_eq_lfpDTr {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (p : CCS.CCS Action Name) (Q : CCS.CCS Action Name → Prop) (tr : Trace Action) : TraceDifferenceToSet env p Q tr ↔ lfpDTr env p Q tr

Proposition 2.7: The concrete trace difference equals the least fixpoint of DTr.

For all p : CCS and Q : ProcSet and tr : Trace:

  tr ∈ TraceDifferenceToSet env p Q  ↔  tr ∈ lfpDTr env p Q

Proof sketch:

• (⊆) TraceDifferenceToSet ⊆ lfpDTr: by induction on the derivation of TraceSem env p tr, with Q universally quantified in the motive so that the IH shifts Q to DerivSetOf env Q a in the cons step.
• (⊇) lfpDTr ⊆ TraceDifferenceToSet: by instantiating the universal quantifier in lfpDTr with TraceDifferenceToSet env and checking that it is a pre-fixpoint of DTr env (traceDiff_is_prefixpoint).

theorem EqCheckingAbstractInterpretation.Trace.tracePreorder_iff_lfp_empty {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (p q : CCS.CCS Action Name) : TracePreorder env p q ↔ ¬∃ (tr : Trace Action), lfpDTr env p {q} tr

Corollary: trace preorder reduces to a fixpoint-emptiness check (Proposition 2.7).

  TracePreorder env p q  ↔  ¬ ∃ tr, lfpDTr env p (· = q) tr