Skip to content

feat: tauSTr (restart) #444

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
PieterCuijpers wants to merge 1 commit into
base: main
Choose a base branch
from
Open

feat: tauSTr (restart) #444

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
175 changes: 62 additions & 113 deletions Cslib/Foundations/Semantics/LTS/Basic.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -747,10 +747,14 @@ class HasTau (Label : Type v) where
/-- The internal transition label, also known as τ. -/
τ : Label

/-- Saturated τ-transition relation. -/
def LTS.τSTr [HasTau Label] (lts : LTS State Label) : State → State → Prop :=
Relation.ReflTransGen (Tr.toRelation lts HasTau.τ)

/-- Saturated transition relation. -/
inductive LTS.STr [HasTau Label] (lts : LTS State Label) : State → Label → State → Prop where
| refl : lts.STr s HasTau.τ s
| tr : lts.STr s1 HasTau.τ s2 → lts.Tr s2 μ s3 → lts.STr s3 HasTau.τ s4 → lts.STr s1 μ s4
| tr : lts.τSTr s1 s2 → lts.Tr s2 μ s3 → lts.τSTr s3 s4 → lts.STr s1 μ s4

/-- The `LTS` obtained by saturating the transition relation in `lts`. -/
@[scoped grind =]
Expand All @@ -765,135 +769,81 @@ theorem LTS.saturate_tr_sTr [HasTau Label] {lts : LTS State Label} :
theorem LTS.STr.single [HasTau Label] (lts : LTS State Label) :
lts.Tr s μ s' → lts.STr s μ s' := by
intro h
apply LTS.STr.tr LTS.STr.refl h LTS.STr.refl
apply LTS.STr.tr .refl h .refl

/-- As `LTS.str`, but counts the number of `τ`-transitions. This is convenient as induction
metric. -/
@[scoped grind]
inductive LTS.STrN [HasTau Label] (lts : LTS State Label) :
ℕ → State → Label → State → Prop where
| refl : lts.STrN 0 s HasTau.τ s
| tr :
lts.STrN n s1 HasTau.τ s2 →
lts.Tr s2 μ s3 →
lts.STrN m s3 HasTau.τ s4 →
lts.STrN (n + m + 1) s1 μ s4

/-- `LTS.str` and `LTS.strN` are equivalent. -/
@[scoped grind =]
theorem LTS.sTr_sTrN [HasTau Label] (lts : LTS State Label) :
lts.STr s1 μ s2 ↔ ∃ n, lts.STrN n s1 μ s2 := by
/-- STr transitions labeled by HasTau.τ are exactly the τSTr transitions. -/
theorem LTS.sTr_τSTr [HasTau Label] (lts : LTS State Label) :
lts.STr s HasTau.τ s' ↔ lts.τSTr s s' := by
apply Iff.intro <;> intro h
case mp =>
induction h
case refl =>
exists 0
exact LTS.STrN.refl
case tr s1 sb μ sb' s2 hstr1 htr hstr2 ih1 ih2 =>
obtain ⟨n1, ih1⟩ := ih1
obtain ⟨n2, ih2⟩ := ih2
exists (n1 + n2 + 1)
apply LTS.STrN.tr ih1 htr ih2
cases h
case refl => exact .refl
case tr _ _ h1 h2 h3 =>
exact (.trans h1 (.head h2 h3))
case mpr =>
obtain ⟨n, h⟩ := h
induction h
case refl =>
constructor
case tr n s1 sb μ sb' m s2 hstr1 htr hstr2 ih1 ih2 =>
apply LTS.STr.tr ih1 htr ih2
cases h
case refl => exact LTS.STr.refl
case tail _ h1 h2 => exact LTS.STr.tr h1 h2 .refl

/-- Saturated transitions labelled by τ can be composed (weighted version). -/
@[scoped grind →]
theorem LTS.STrN.trans_τ
[HasTau Label] (lts : LTS State Label)
(h1 : lts.STrN n s1 HasTau.τ s2) (h2 : lts.STrN m s2 HasTau.τ s3) :
lts.STrN (n + m) s1 HasTau.τ s3 := by
cases h1
case refl => grind
case tr n1 sb sb' n2 hstr1 htr hstr2 =>
have ih := LTS.STrN.trans_τ lts hstr2 h2
have conc := LTS.STrN.tr hstr1 htr ih
grind
/-- In a saturated LTS, the transition and saturated transition relations are the same. -/
theorem LTS.saturate_τSTr_τSTr [hHasTau : HasTau Label] (lts : LTS State Label)
: lts.saturate.τSTr s = lts.τSTr s := by
ext s''
apply Iff.intro <;> intro h
case mp =>
induction h
case refl => constructor
case tail _ _ _ h2 h3 => exact Relation.ReflTransGen.trans h3 ((LTS.sTr_τSTr _).mp h2)
case mpr =>
cases h
case refl => constructor
case tail s' h2 h3 =>
have h4 := LTS.STr.tr h2 h3 Relation.ReflTransGen.refl
exact Relation.ReflTransGen.single h4

/-- Saturated transitions labelled by τ can be composed. -/
@[scoped grind →]
@[scoped grind .]
theorem LTS.STr.trans_τ
[HasTau Label] (lts : LTS State Label)
(h1 : lts.STr s1 HasTau.τ s2) (h2 : lts.STr s2 HasTau.τ s3) :
lts.STr s1 HasTau.τ s3 := by
obtain ⟨n, h1N⟩ := (LTS.sTr_sTrN lts).1 h1
obtain ⟨m, h2N⟩ := (LTS.sTr_sTrN lts).1 h2
have concN := LTS.STrN.trans_τ lts h1N h2N
apply (LTS.sTr_sTrN lts).2 ⟨n + m, concN⟩

/-- Saturated transitions can be appended with τ-transitions (weighted version). -/
@[scoped grind <=]
theorem LTS.STrN.append
[HasTau Label] (lts : LTS State Label)
(h1 : lts.STrN n1 s1 μ s2)
(h2 : lts.STrN n2 s2 HasTau.τ s3) :
lts.STrN (n1 + n2) s1 μ s3 := by
cases h1
case refl => grind
case tr n11 sb sb' n12 hstr1 htr hstr2 =>
have hsuffix := LTS.STrN.trans_τ lts hstr2 h2
have n_eq : n11 + (n12 + n2) + 1 = (n11 + n12 + 1 + n2) := by omega
rw [← n_eq]
apply LTS.STrN.tr hstr1 htr hsuffix

/-- Saturated transitions can be composed (weighted version). -/
@[scoped grind <=]
theorem LTS.STrN.comp
[HasTau Label] (lts : LTS State Label)
(h1 : lts.STrN n1 s1 HasTau.τ s2)
(h2 : lts.STrN n2 s2 μ s3)
(h3 : lts.STrN n3 s3 HasTau.τ s4) :
lts.STrN (n1 + n2 + n3) s1 μ s4 := by
cases h2
case refl =>
apply LTS.STrN.trans_τ lts h1 h3
case tr n21 sb sb' n22 hstr1 htr hstr2 =>
have hprefix_τ := LTS.STrN.trans_τ lts h1 hstr1
have hprefix := LTS.STrN.tr hprefix_τ htr hstr2
have conc := LTS.STrN.append lts hprefix h3
grind
[HasTau Label] (lts : LTS State Label)
Copy link
Collaborator

@fmontesi fmontesi Mar 19, 2026 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Needs double indentation per Mathlib style. In general, all lines after the first and before the := are doubly-indented. Please apply also to your other modifications. :-)

(h1 : lts.STr s1 HasTau.τ s2) (h2 : lts.STr s2 HasTau.τ s3) :
lts.STr s1 HasTau.τ s3 := by
rw [LTS.sTr_τSTr _] at h1 h2
rw [LTS.sTr_τSTr _]
apply Relation.ReflTransGen.trans h1 h2

/-- Saturated transitions can be composed. -/
@[scoped grind <=]
theorem LTS.STr.comp
[HasTau Label] (lts : LTS State Label)
(h1 : lts.STr s1 HasTau.τ s2)
(h2 : lts.STr s2 μ s3)
(h3 : lts.STr s3 HasTau.τ s4) :
lts.STr s1 μ s4 := by
obtain ⟨n1, h1N⟩ := (LTS.sTr_sTrN lts).1 h1
obtain ⟨n2, h2N⟩ := (LTS.sTr_sTrN lts).1 h2
obtain ⟨n3, h3N⟩ := (LTS.sTr_sTrN lts).1 h3
have concN := LTS.STrN.comp lts h1N h2N h3N
apply (LTS.sTr_sTrN lts).2 ⟨n1 + n2 + n3, concN⟩

open scoped LTS.STr in
[HasTau Label] (lts : LTS State Label)
(h1 : lts.STr s1 HasTau.τ s2)
(h2 : lts.STr s2 μ s3)
(h3 : lts.STr s3 HasTau.τ s4) :
lts.STr s1 μ s4 := by
rw [LTS.sTr_τSTr _] at h1 h3
cases h2
case refl =>
rw [LTS.sTr_τSTr _]
apply Relation.ReflTransGen.trans h1 h3
case tr _ _ hτ1 htr hτ2 =>
exact LTS.STr.tr (Relation.ReflTransGen.trans h1 hτ1) htr (Relation.ReflTransGen.trans hτ2 h3)

/-- In a saturated LTS, the transition and saturated transition relations are the same. -/
@[scoped grind _=_]
theorem LTS.saturate_sTr_tr [hHasTau : HasTau Label] (lts : LTS State Label)
(hμ : μ = hHasTau.τ) : lts.saturate.Tr s μ = lts.saturate.STr s μ := by
theorem LTS.saturate_tr_saturate_sTr [hHasTau : HasTau Label] (lts : LTS State Label)
(hμ : μ = hHasTau.τ) : lts.saturate.Tr s μ = lts.saturate.STr s μ := by
ext s'
apply Iff.intro <;> intro h
case mp =>
induction h
cases h
case refl => constructor
case tr s1 sb μ sb' s2 hstr1 htr hstr2 ih1 ih2 =>
rw [hμ] at htr
apply LTS.STr.single at htr
rw [← LTS.saturate_tr_sTr] at htr
grind [LTS.STr.tr]
case tr hstr1 htr hstr2 =>
apply LTS.STr.single
exact LTS.STr.tr hstr1 htr hstr2
case mpr =>
induction h
cases h
case refl => constructor
case tr s1 sb μ sb' s2 hstr1 htr hstr2 ih1 ih2 =>
simp only [LTS.saturate] at ih1 htr ih2
simp only [LTS.saturate]
grind
case tr hstr1 htr hstr2 =>
rw [LTS.saturate_τSTr_τSTr lts] at hstr1 hstr2
rw [←LTS.sTr_τSTr lts] at hstr1 hstr2
exact LTS.STr.comp lts hstr1 htr hstr2

/-- In a saturated LTS, every state is in its τ-image. -/
@[scoped grind .]
Expand All @@ -902,7 +852,6 @@ theorem LTS.mem_saturate_image_τ [HasTau Label] (lts : LTS State Label) :

/-- The `τ`-closure of a set of states `S` is the set of states reachable by any state in `S`
by performing only `τ`-transitions. -/
@[scoped grind =]
def LTS.τClosure [HasTau Label] (lts : LTS State Label) (S : Set State) : Set State :=
lts.saturate.setImage S HasTau.τ

Expand Down
117 changes: 47 additions & 70 deletions Cslib/Foundations/Semantics/LTS/Bisimulation.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -808,77 +808,48 @@ def LTS.IsSWBisimulation [HasTau Label] (lts : LTS State Label) (r : State → S
(∀ s2', lts.Tr s2 μ s2' → ∃ s1', lts.STr s1 μ s1' ∧ r s1' s2')
)

/-- Utility theorem for 'following' internal transitions using an `SWBisimulation`
(first component, weighted version). -/
theorem SWBisimulation.follow_internal_fst_n
[HasTau Label] {lts : LTS State Label}
(hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstrN : lts.STrN n s1 HasTau.τ s1') :
∃ s2', lts.STr s2 HasTau.τ s2' ∧ r s1' s2' := by
cases n
case zero =>
cases hstrN
exists s2
constructor; constructor
exact hr
case succ n ih =>
cases hstrN
rename_i n1 sb sb' n2 hstrN1 htr hstrN2
let hswb_m := hswb
have ih1 := SWBisimulation.follow_internal_fst_n hswb hr hstrN1
obtain ⟨sb2, hstrs2, hrsb⟩ := ih1
have h := (hswb hrsb HasTau.τ).1 sb' htr
obtain ⟨sb2', hstrsb2, hrsb2⟩ := h
have ih2 := SWBisimulation.follow_internal_fst_n hswb hrsb2 hstrN2
obtain ⟨s2', hstrs2', hrs2⟩ := ih2
exists s2'
constructor
· apply LTS.STr.trans_τ lts (LTS.STr.trans_τ lts hstrs2 hstrsb2) hstrs2'
· exact hrs2

/-- Utility theorem for 'following' internal transitions using an `SWBisimulation`
(second component, weighted version). -/
theorem SWBisimulation.follow_internal_snd_n
[HasTau Label] {lts : LTS State Label}
(hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstrN : lts.STrN n s2 HasTau.τ s2') :
∃ s1', lts.STr s1 HasTau.τ s1' ∧ r s1' s2' := by
cases n
case zero =>
cases hstrN
exists s1
constructor; constructor
exact hr
case succ n ih =>
cases hstrN
rename_i n1 sb sb' n2 hstrN1 htr hstrN2
let hswb_m := hswb
have ih1 := SWBisimulation.follow_internal_snd_n hswb hr hstrN1
obtain ⟨sb1, hstrs1, hrsb⟩ := ih1
have h := (hswb hrsb HasTau.τ).2 sb' htr
obtain ⟨sb2', hstrsb2, hrsb2⟩ := h
have ih2 := SWBisimulation.follow_internal_snd_n hswb hrsb2 hstrN2
obtain ⟨s2', hstrs2', hrs2⟩ := ih2
exists s2'
constructor
· apply LTS.STr.trans_τ lts (LTS.STr.trans_τ lts hstrs1 hstrsb2) hstrs2'
· exact hrs2

/-- Utility theorem for 'following' internal transitions using an `SWBisimulation`
(first component). -/
theorem SWBisimulation.follow_internal_fst
[HasTau Label] {lts : LTS State Label}
(hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstr : lts.STr s1 HasTau.τ s1') :
∃ s2', lts.STr s2 HasTau.τ s2' ∧ r s1' s2' := by
obtain ⟨n, hstrN⟩ := (LTS.sTr_sTrN lts).1 hstr
apply SWBisimulation.follow_internal_fst_n hswb hr hstrN
[HasTau Label] {lts : LTS State Label}
(hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstr : lts.τSTr s1 s1') :
∃ s2', lts.τSTr s2 s2' ∧ r s1' s2' := by
induction hstr
case refl =>
exists s2
constructor; constructor
exact hr
case tail sb hrsb htrsb ih1 ih2 =>
obtain ⟨sb2, htrsb2, hrb⟩ := ih2
have h := (hswb hrb HasTau.τ).left _ ih1
obtain ⟨sb2', htrsb2', hrb'⟩ := h
exists sb2'
constructor
· simp only [LTS.sTr_τSTr] at htrsb htrsb2'
exact Relation.ReflTransGen.trans htrsb2 htrsb2'
· exact hrb'

/-- Utility theorem for 'following' internal transitions using an `SWBisimulation`
(second component). -/
theorem SWBisimulation.follow_internal_snd
[HasTau Label] {lts : LTS State Label}
(hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstr : lts.STr s2 HasTau.τ s2') :
∃ s1', lts.STr s1 HasTau.τ s1' ∧ r s1' s2' := by
obtain ⟨n, hstrN⟩ := (LTS.sTr_sTrN lts).1 hstr
apply SWBisimulation.follow_internal_snd_n hswb hr hstrN
[HasTau Label] {lts : LTS State Label}
(hswb : lts.IsSWBisimulation r) (hr : r s1 s2) (hstr : lts.τSTr s2 s2') :
∃ s1', lts.τSTr s1 s1' ∧ r s1' s2' := by
induction hstr
case refl =>
exists s1
constructor; constructor
exact hr
case tail sb hrsb htrsb ih1 ih2 =>
obtain ⟨sb2, htrsb2, hrb⟩ := ih2
have h := (hswb hrb HasTau.τ).right _ ih1
obtain ⟨sb2', htrsb2', hrb'⟩ := h
exists sb2'
constructor
· simp only [LTS.sTr_τSTr] at htrsb htrsb2'
exact Relation.ReflTransGen.trans htrsb2 htrsb2'
· exact hrb'


/-- We can now prove that any relation is a `WeakBisimulation` iff it is an `SWBisimulation`.
This formalises lemma 4.2.10 in [Sangiorgi2011]. -/
Expand Down Expand Up @@ -912,12 +883,15 @@ theorem LTS.isWeakBisimulation_iff_isSWBisimulation
constructor; constructor
exact hr
case tr sb sb' hstr1 htr hstr2 =>
obtain ⟨sb2, hstr2b, hrb⟩ := SWBisimulation.follow_internal_fst h hr hstr1
obtain ⟨sb2', hstr2b', hrb'⟩ := (h hrb μ).1 _ htr
obtain ⟨s2', hstr2', hrb2⟩ := SWBisimulation.follow_internal_fst h hrb' hstr2
exists s2'
rw [←LTS.sTr_τSTr] at hstr1 hstr2
simp only [sTr_τSTr] at hstr1 hstr2
obtain ⟨sb1, hstr1b, hrb⟩ := SWBisimulation.follow_internal_fst h hr hstr1
obtain ⟨sb2', hstr1b', hrb'⟩ := (h hrb μ).left _ htr
obtain ⟨s1', hstr1', hrb2⟩ := SWBisimulation.follow_internal_fst h hrb' hstr2
rw [←LTS.sTr_τSTr] at hstr1' hstr1b
exists s1'
constructor
· exact LTS.STr.comp lts hstr2b hstr2b' hstr2'
· exact LTS.STr.comp lts hstr1b hstr1b' hstr1'
· exact hrb2
case right =>
intro s2' hstr
Expand All @@ -927,9 +901,12 @@ theorem LTS.isWeakBisimulation_iff_isSWBisimulation
constructor; constructor
exact hr
case tr sb sb' hstr1 htr hstr2 =>
rw [←LTS.sTr_τSTr] at hstr1 hstr2
simp only [sTr_τSTr] at hstr1 hstr2
obtain ⟨sb1, hstr1b, hrb⟩ := SWBisimulation.follow_internal_snd h hr hstr1
obtain ⟨sb2', hstr1b', hrb'⟩ := (h hrb μ).2 _ htr
obtain ⟨sb2', hstr1b', hrb'⟩ := (h hrb μ).right _ htr
obtain ⟨s1', hstr1', hrb2⟩ := SWBisimulation.follow_internal_snd h hrb' hstr2
rw [←LTS.sTr_τSTr] at hstr1' hstr1b
exists s1'
constructor
· exact LTS.STr.comp lts hstr1b hstr1b' hstr1'
Expand Down
Loading