Skip to content

chore: use grind in CCS.BehaviouralTheory #54

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

Merged
merged 1 commit into from
Sep 3, 2025
Merged

chore: use grind in CCS.BehaviouralTheory #54

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
60 changes: 16 additions & 44 deletions Cslib/Languages/CCS/BehaviouralTheory.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,37 +29,26 @@ open CCS CCS.Process CCS.Act

namespace CCS

@[grind cases]
private inductive ParNil : (Process Name Constant) → (Process Name Constant) → Prop where
| parNil : ParNil (par p nil) p

attribute [grind] ParNil.parNil

/-- P | 𝟎 ~ P -/
@[simp, scoped grind]
theorem bisimilarity_par_nil : (par p nil) ~[@lts Name Constant defs] p := by
unfold lts at *
exists ParNil
constructor; constructor
simp only [Bisimulation]
intro s1 s2 hr μ
constructor
case left =>
intro s1' htr
cases hr
cases htr
case parL p' htr =>
exists p'
apply And.intro htr ParNil.parNil
case parR q' htr =>
cases htr
case com μ p' q' htrp htrq =>
cases htrq
grind [cases Tr]
case right =>
intro s2' htr
cases hr
exists (par s2' nil)
constructor
case left =>
apply Tr.parL htr
case right =>
constructor
grind [Tr.parL]

private inductive ParComm : (Process Name Constant) → (Process Name Constant) → Prop where
| parComm : ParComm (par p q) (par q p)
Expand Down Expand Up @@ -137,33 +126,23 @@ private inductive ChoiceIdem : (Process Name Constant) → (Process Name Constan

/-- P + P ~ P -/
theorem bisimilarity_choice_idem :
(choice p p) ~[@lts Name Constant defs] p := by
(choice p p) ~[lts (defs := defs)] p := by
exists ChoiceIdem
apply And.intro
case left => grind [ChoiceIdem]
case right =>
intro s1 s2 hr μ
apply And.intro <;> cases hr
case left.idem =>
intro s2' htr
exists s2'
apply And.intro
case left =>
cases htr <;> unfold lts <;> grind
case right =>
grind [ChoiceIdem]
unfold lts
grind [cases Tr, ChoiceIdem]
case left.id =>
grind [ChoiceIdem]
case right.idem =>
intro s1' htr
exists s1'
apply And.intro
case left =>
unfold lts
unfold lts at htr
grind [Tr]
case right =>
grind [ChoiceIdem]
unfold lts at *
grind [Tr, ChoiceIdem]
case right.id =>
grind [ChoiceIdem]

Expand All @@ -179,30 +158,23 @@ theorem bisimilarity_choice_comm : (choice p q) ~[@lts Name Constant defs] (choi
intro s1 s2 hr μ
cases hr
case choiceComm =>
unfold lts
rename_i p q
constructor
case left =>
intro s1' htr
exists s1'
constructor
· cases htr
· apply Tr.choiceR
assumption
· apply Tr.choiceL
assumption
· cases htr with grind [Tr.choiceR, Tr.choiceL]
· constructor
apply Bisimilarity.refl (@lts _ _ defs) s1'
grind [Bisimilarity.refl]
case right =>
intro s1' htr
exists s1'
constructor
· cases htr
· apply Tr.choiceR
assumption
· apply Tr.choiceL
assumption
· cases htr with grind [Tr.choiceR, Tr.choiceL]
· constructor
apply Bisimilarity.refl (@lts _ _ defs) s1'
grind [Bisimilarity.refl]
case bisim h =>
constructor
case left =>
Expand Down