-
Notifications
You must be signed in to change notification settings - Fork 1
/
Logical_Equivalence.v
107 lines (101 loc) · 2.41 KB
/
Logical_Equivalence.v
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
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
Require Import Sets Modal_Library Modal_Notations Classical List.
Context `{X: modal_index_set}.
Lemma singleton_formula:
forall M p,
theory_modal M (Singleton p) -> M |= p.
Proof.
intros.
apply H.
constructor.
Qed.
Theorem implies_to_or_modal:
forall φ ψ,
[! φ -> ψ !] =|= [! ~φ \/ ψ !].
Proof.
split.
- unfold entails_modal, entails, validate_model in *.
intros; simpl in *.
apply singleton_formula in H.
destruct classic with (M ' w ||- φ); firstorder.
- unfold entails_modal, entails in *.
intros; simpl in *.
apply singleton_formula in H.
intro w.
specialize (H w).
simpl in H.
destruct H.
+ simpl; intros.
exfalso; firstorder.
+ simpl; firstorder.
Qed.
Theorem double_neg_modal:
forall φ,
[! ~~φ !] =|= φ.
Proof.
split.
- unfold entails_modal, entails, validate_model; intros.
apply singleton_formula in H.
specialize (H w); simpl in H.
apply NNPP; auto.
- unfold entails_modal, entails, validate_model; intros.
simpl.
apply singleton_formula in H.
edestruct classic.
+ exact H0.
+ apply NNPP in H0.
exfalso; eauto.
Qed.
Theorem and_to_implies_modal:
forall φ ψ,
[! φ /\ ψ !] =|= [! ~(φ -> ~ψ) !].
Proof.
split.
- unfold entails_modal, entails, validate_model.
simpl in *; intros.
unfold validate_model in *.
simpl in *.
apply singleton_formula in H.
unfold not; intros; apply H0.
+ destruct H with (w:=w); auto.
+ destruct H with (w:=w); auto.
- unfold entails_modal, entails.
simpl in *; intros.
unfold validate_model in *.
intros; simpl in *.
apply singleton_formula in H.
specialize (H w); simpl in H.
split.
+ edestruct classic.
* exact H0.
* exfalso.
firstorder.
+ edestruct classic.
* exact H0.
* firstorder.
Qed.
Theorem diamond_to_box_modal:
forall φ idx,
[! <idx>φ !] =|= [! ~[idx]~φ !].
Proof.
split.
- unfold entails_modal, entails, validate_model in *.
simpl in *; intros.
apply singleton_formula in H.
specialize (H w); simpl in H.
edestruct classic.
+ exact H0.
+ firstorder.
- intros.
unfold entails_modal, entails in *.
simpl in *.
unfold validate_model in *.
simpl in *.
unfold not in *.
intros.
apply singleton_formula in H.
specialize (H w); simpl in H.
edestruct classic.
+ exact H0.
+ exfalso.
firstorder.
Qed.