Tactics for discharging StrongRefinement obligations.

• A refinement obligation is a disjunction over two different shapes. Terminating concludes either "the source takes a matching step" (a source state, a source trace, the post-relation, Rτ, and membership) or "the source aborted having emitted a sequentially consistent prefix" (a source trace, ≼[Rτ], membership); Diverging has its own two. refines_match / refines_abort / refines_diverge make that choice, with the witness supplied and every remaining side condition left as a numbered goal.
• Traces are related by Rτ, not equal, and prefixes are ≼[Rτ], not <+:. trace_rel and trace_pfx close the two shapes at a Rτ that relates a trace to itself, which is the common case for a pass that preserves traces exactly — including Guarded2Network, since reception is unobservable there.

Every tactic here leaves goals rather than searching: the leaf discharge is sem_side's job, and a search tactic runs terminally or not at all.

def StrongRefinement.«tacticRefines_match_,_» : Lean.ParserDescr

The source matches the target's step: supply the source state it steps to, and — with the two-argument form — the source trace it emits. Leaves the post-relation, the Rτ obligation and the source-membership obligation, in that order.

The trace is a witness, not a goal, so it cannot be left as _: an existential's witness has to be a term by the time the body elaborates. The one-argument form therefore leaves it as the first goal, ahead of the three obligations; prefer the two-argument form wherever the emitted trace is already known, which for a trace-preserving pass is everywhere.

Equations

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

def StrongRefinement.tacticRefines_abort_ : Lean.ParserDescr

The source aborted instead, having emitted ε. Leaves the ≼[Rτ] obligation and membership in the source's aborting semantics. Covers both Terminating's right disjunct and the whole of Aborting, which is the same shape without the Or.

Equations

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

def StrongRefinement.tacticRefines_diverge_ : Lean.ParserDescr

The source diverges too, emitting ε — Diverging's left disjunct. Its right disjunct is an abort, which refines_abort already covers.

Equations

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

def StrongRefinement.tacticTrace_rel : Lean.ParserDescr

Close a Rτ ε' ε goal when the two traces are literally the same and Rτ is reflexive at it — the shape a trace-preserving pass produces at every leaf. Falls back to an assumption, for a pass carrying the relatedness as a hypothesis.

Equations

• StrongRefinement.tacticTrace_rel = Lean.ParserDescr.node `StrongRefinement.tacticTrace_rel 1024 (Lean.ParserDescr.nonReservedSymbol "trace_rel" false)

def StrongRefinement.tacticTrace_pfx : Lean.ParserDescr

Close a ε' ≼[Rτ] ε goal the same way: ≼[·] is extensive with no hypotheses on the relation, so a related pair is a prefix pair (Trace.scPrefix_of).

Equations

• StrongRefinement.tacticTrace_pfx = Lean.ParserDescr.node `StrongRefinement.tacticTrace_pfx 1024 (Lean.ParserDescr.nonReservedSymbol "trace_pfx" false)

Validation

Two examples, one per disjunct, against the identity refinement — enough to catch the failure mode these macros exist to prevent: a refine whose ?_ count or order drifts from the definition it targets. They are cheap and they break loudly if Terminating/Aborting change shape.