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
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
|
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 | A () ∩ B ≠ ∅ }
lifting_natural {X Y} f
| .box => by simp
| .diamond => by
intro A; ext B
simp only [Set.mem_setOf_eq, Set.preimage_setOf_eq, Set.fmap_eq_image]
rw [← Set.nonempty_iff_ne_empty, ← Set.nonempty_iff_ne_empty]
show (∃ x, x ∈ f ⁻¹' A () ∧ x ∈ B) ↔ (∃ x, x ∈ A () ∧ x ∈ f '' B)
constructor
· intro ⟨x, h₁, h₂⟩
use f x; exact ⟨Set.mem_preimage.mpr h₁, Set.mem_image_of_mem f h₂⟩
· intro ⟨fx, h₁, h₂⟩
rw [Set.mem_image] at h₂
obtain ⟨x, hx₁, hx₂⟩ := h₂
use x; rw [Set.mem_preimage, hx₂]; exact ⟨h₁, hx₁⟩
lifting_monotone {X}
| .box => by
intro A A' h
simp only [Set.setOf_subset_setOf]
intro B hB; trans
· exact hB
· exact h ()
| .diamond => by
intro A A' h
simp only [Set.setOf_subset_setOf, ← Set.nonempty_iff_ne_empty]
intro B ⟨x, hx₁, hx₂⟩; use x
exact ⟨h () hx₁, hx₂⟩
lifting_dual {X}
| .box => by
intro A; ext B
simp only [Set.mem_setOf_eq, Modalities.dualSignature, ← Set.nonempty_iff_ne_empty]
constructor
· intro ⟨x, hx₁, hx₂⟩ hcontra
exact hcontra hx₂ hx₁
· show (¬(∀ x ∈ B, x ∈ (A ()).compl)) → (A () ∩ B).Nonempty
simp only [not_forall]
intro ⟨x, hx₁, hx₂⟩
use x
exact ⟨Set.not_notMem.mp hx₂, hx₁⟩
| .diamond => by
intro A; ext B
simp only [Modalities.dualSignature, Set.mem_setOf_eq, ← Set.nonempty_iff_ne_empty]
show (∀ x ∈ B, x ∈ A ()) ↔ ¬(∃ x, x ∈ (A ()).compl ∩ B)
rw [not_exists]
constructor
· intro h; by_contra
simp only [Set.mem_inter_iff, not_and, not_forall, not_not] at this
obtain ⟨x, hx₁, hx₂⟩ := this
exact hx₁ (h x hx₂)
· intro h x hx; by_contra
simp only [Set.mem_inter_iff, not_and] at h
exact h x this hx
end Relational
|
