forked from leanprover/lean4
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
William Sørensen
committed
Aug 21, 2024
1 parent
409b3aa
commit 6fb6f9b
Showing
3 changed files
with
95 additions
and
1 deletion.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,87 @@ | ||
structure FSM where | ||
S : Type | ||
d : S → Nat → S | ||
A : S → Prop | ||
|
||
-- Example of a coinductive predicate defined over FSMs | ||
|
||
coinductive Bisim (fsm : FSM) : fsm.S → fsm.S → Prop := | ||
| step {s t : fsm.S} : | ||
(fsm.A s ↔ fsm.A t) | ||
→ (∀ c, Bisim (fsm.d s c) (fsm.d t c)) | ||
→ Bisim fsm s t | ||
|
||
/-- | ||
info: inductive Bisim.Invariant : (fsm : FSM) → (fsm.S → fsm.S → Prop) → fsm.S → fsm.S → Prop | ||
number of parameters: 4 | ||
constructors: | ||
Bisim.Invariant.step : ∀ {fsm : FSM} {Bisim : fsm.S → fsm.S → Prop} {x x_1 : fsm.S}, | ||
(fsm.A x ↔ fsm.A x_1) → (∀ (c : Nat), Bisim (fsm.d x c) (fsm.d x_1 c)) → Bisim.Invariant fsm Bisim x x_1 | ||
-/ | ||
#guard_msgs in | ||
#print Bisim.Invariant | ||
|
||
/-- | ||
info: @[reducible] def Bisim.Is : (fsm : FSM) → (fsm.S → fsm.S → Prop) → Prop := | ||
fun fsm R => ∀ {x x_1 : fsm.S}, R x x_1 → Bisim.Invariant fsm R x x_1 | ||
-/ | ||
#guard_msgs in | ||
#print Bisim.Is | ||
|
||
/-- | ||
info: def Bisim : (fsm : FSM) → fsm.S → fsm.S → Prop := | ||
fun fsm x x_1 => ∃ R, Bisim.Is fsm R ∧ R x x_1 | ||
-/ | ||
#guard_msgs in | ||
#print Bisim | ||
|
||
/-- info: 'Bisim' does not depend on any axioms -/ | ||
#guard_msgs in | ||
#print axioms Bisim | ||
|
||
theorem bisim_refl : Bisim f a a := by | ||
exists fun a b => a = b | ||
simp only [and_true] | ||
intro s t seqt | ||
constructor <;> simp_all | ||
|
||
theorem bisim_symm (h : Bisim f a b): Bisim f b a := by | ||
rcases h with ⟨rel, relIsBisim, rab⟩ | ||
exists fun a b => rel b a | ||
simp_all | ||
intro a b holds | ||
specialize relIsBisim holds | ||
rcases relIsBisim with ⟨imp, z⟩ | ||
constructor <;> simp_all only [implies_true, and_self] | ||
|
||
theorem Bisim.unfold {f} : Bisim.Is f (Bisim f) := by | ||
rintro s t ⟨R, h_is, h_Rst⟩ | ||
constructor | ||
· exact (h_is h_Rst).1 | ||
· intro c; exact ⟨R, h_is, (h_is h_Rst).2 c⟩ | ||
|
||
theorem bisim_trans (h_ab : Bisim f a b) (h_bc : Bisim f b c) : | ||
Bisim f a c := by | ||
exists (fun s t => ∃ u, Bisim f s u ∧ Bisim f u t) | ||
constructor | ||
intro s t h_Rst | ||
· rcases h_Rst with ⟨u, h_su, h_ut⟩ | ||
have ⟨h_su₁, h_su₂⟩ := h_su.unfold | ||
have ⟨h_ut₁, h_ut₂⟩ := h_ut.unfold | ||
refine ⟨?_, ?_⟩ | ||
· rw [h_su₁, h_ut₁] | ||
· intro c; exact ⟨_, h_su₂ c, h_ut₂ c⟩ | ||
· exact ⟨b, h_ab, h_bc⟩ | ||
|
||
/-- info: 'bisim_refl' depends on axioms: [propext, Quot.sound] -/ | ||
#guard_msgs in | ||
#print axioms bisim_refl | ||
|
||
/-- info: 'bisim_symm' depends on axioms: [propext, Quot.sound] -/ | ||
#guard_msgs in | ||
#print axioms bisim_symm | ||
|
||
/-- info: 'bisim_trans' depends on axioms: [propext] -/ | ||
#guard_msgs in | ||
#print axioms bisim_trans | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,7 @@ | ||
-- Coinductive currently does only work on Prop | ||
|
||
/-- error: Expected return type to be a Prop -/ | ||
#guard_msgs in | ||
coinductive S (α : Type) : Type := | ||
| cons (hd : α) (tl : S α) | ||
|