blob: 4c9155b81d645fbcf30f1657c614c4abb1e41e36 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
|
import Mathlib
import SymbolicModalLogic.MuCalculus
inductive Relational where
| box
| diamond
namespace Relational
instance : Modalities Relational where
signature _ := Unit
dual
| .box => .diamond
| .diamond => .box
dualSignature
| .box, f => f
| .diamond, f => f
dual_involution := by intro l; cases l <;> simp
instance : Model Relational Set where
lifting
| .box, A => { B | B ⊆ A () }
| .diamond, A => { B | B ∩ A () ≠ ∅ }
@[simp]
lemma lift_box_iff {X : Type} {A : Unit → Set X} {B : Set X} : B ∈ Model.lift Relational.box Set A ↔ ∀ x ∈ B, x ∈ A () := by
show B ∈ { B | B ⊆ A () } ↔ ∀ x ∈ B, x ∈ A ()
exact Set.mem_setOf
@[simp]
lemma lift_diamond_iff {X : Type} {A : Unit → Set X} {B : Set X} : B ∈ Model.lift Relational.diamond Set A ↔ ∃ x ∈ B, x ∈ A () := by
show B ∈ { B | B ∩ A () ≠ ∅ } ↔ ∃ x ∈ B, x ∈ A ()
rw [Set.mem_setOf_eq, ← Set.nonempty_iff_ne_empty]
rfl
instance : LawfulModel Relational Set where
lifting_natural {X Y} f l := by
cases l
all_goals intro A; ext B; simp
lifting_monotone {X} l := by
cases l with
| box =>
intro A A' h B hB
rw [lift_box_iff]; intro x hx
rw [lift_box_iff] at hB
exact h () (hB x hx)
| diamond =>
intro A A' h B hB
rw [lift_diamond_iff] at hB
obtain ⟨x, hx⟩ := hB
rw [lift_diamond_iff]; use x
exact ⟨hx.left, h () hx.right⟩
lifting_dual {X} l := by
cases l
all_goals intro A; ext B; simp [Modalities.dual, Modalities.dualSignature]
end Relational
|
