Denotational RS Difference via Finite Certificates

This module provides an independent denotational characterization of RS differences using finite witness certificates. This avoids direct recursion on multi-parameter types that triggers Lean's termination checker.

Key idea:

• RSDenotationalCert o is a structural inductive datatype indexed by RSObs o (no recursion issues—just inductive structure)
• isValidCert is a validation predicate (can be recursive, but simpler than full denotation)
• rsDifferenceDenotational is defined as exists valid certificate (no recursion)
• Equivalence to lfpDRS is then proven by relating valid certificates to lfp membership

This mirrors the paper's denotational definition while sidestepping Lean's termination constraints.

inductive EqCheckingAbstractInterpretation.Ready.RSDenotationalCert {Action : Type u} : RSObs Action → Type (u + 1)

Finite certificate witnessing that an RS observation is in the concrete difference.

This is an inductive datatype (not recursive definition), indexed by the observation it certifies. The recursion on observation structure is purely structural, so the Lean kernel accepts it immediately.

• tt_cert {Action : Type u} : RSDenotationalCert RSObs.tt
• node_cert {Action : Type u} {pos : List (Action × RSObs Action)} {neg : List Action} : ((i : Fin pos.length) → RSDenotationalCert (pos.get i).snd) → RSDenotationalCert (RSObs.node pos neg)

def EqCheckingAbstractInterpretation.Ready.isValidRSCert {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) {o : RSObs Action} (cert : RSDenotationalCert o) : Prop

Validation predicate: check if a certificate is valid at pair (p, Q) under environment.

This is the recursive validation function (separate from the structural certificate). It checks three conditions:

1. A cover of the right-hand states by local failure reasons: each q ∈ Q is assigned either to the negative tests or to some positive branch
2. For each positive branch (a, o): exists p' ∈ Der(p,a) with valid cert for o at (p', Der(Q_a, a)) for the states assigned to that branch
3. For each negative test b: ¬Enabled(env, p, b)
4. For each q assigned to the negative tests: some b ∈ neg is enabled at q

This recursion is over the certificate structure, which is well-founded.

Equations

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

def EqCheckingAbstractInterpretation.Ready.rsDifferenceDenotational {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) : DiffSysRS Action Name (RSObs Action)

Denotational RS difference using finite certificates: an observation is distinguishing iff a valid certificate exists.

Equations

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

theorem EqCheckingAbstractInterpretation.Ready.isValidCert_implies_lfp {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) {o : RSObs Action} (cert : RSDenotationalCert o) (hValid : isValidRSCert env p Q cert) : lfpDRS env p Q o

Soundness: any valid certificate gives an element of the concrete lfp.

For any certificate of observation o that is valid at (p, Q), we show that o is in lfpDRS env p Q by induction on the certificate structure. The induction hypothesis ensures that at each step, the DRS conditions are met.

theorem EqCheckingAbstractInterpretation.Ready.lfp_implies_isValidCert {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) (o : RSObs Action) (h_lfp : lfpDRS env p Q o) : ∃ (cert : RSDenotationalCert o), isValidRSCert env p Q cert

Completeness: any element of the concrete lfp admits a valid certificate.

For any observation in lfpDRS env p Q, we construct a valid certificate by induction on the observation structure, extracting the certificate structure from the DRS conditions.

theorem EqCheckingAbstractInterpretation.Ready.rsDifferenceDenotational_eq_lfpDRS {Action : Type u} {Name : Type v} (env : CCS.Env Action Name) (p : CCS.CCS Action Name) (Q : ProcSet Action Name) (o : RSObs Action) : rsDifferenceDenotational env p Q o ↔ lfpDRS env p Q o

Main theorem: the denotational and lfp characterizations are equivalent.