LTS and calc

Stream: computer science

[Fabrizio Montesi]

I made calc work for transitions in LTSs by defining

def LTS.Tr.toRelation (lts : LTS State Label) (μ : Label) : State → State → Prop :=
  fun s1 s2 => lts.Tr s1 μ s2

and then appropriate Trans instances like

/-- Transitions can be chained with multi-step transitions. -/
instance (lts : LTS State Label) : Trans (LTS.Tr.toRelation lts μ) (LTS.MTr.toRelation lts μs) (LTS.MTr.toRelation lts (μ :: μs)) where

But to use calc with our notation, I had to change the definition of the notation to invoke LTS.Tr.toRelation instead of just LTS.Tr, which is a bit weird in proofs (no complication whatsoever, but I think people will be surprised by the goal).

So now we can write

example : p [[Act.τ, Act.name 1]]↠ₙ nil :=
  calc
    (p [Act.τ]⭢ₙ (pre (Act.name 1) nil)) := by [...]
    _ [Act.name 1]⭢ₙ nil := by constructor

but in that [...] I get the goal

⊢ LTS.Tr.toRelation ltsNat Act.τ p (pre (Act.name 1) nil)

instead of what I'd like (the simplest):

⊢ ltsNat.Tr p Act.τ (pre (Act.name 1) nil)

So in order to enable calc, I made the notation surprising (because it goes through toRelation instead of invoking Tr directly).

Any ideas on how to get the cake and eat it? :-)