-
Notifications
You must be signed in to change notification settings - Fork 1
/
Logical_Equivalence.v
112 lines (108 loc) · 2.5 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
108
109
110
111
112
Require Import Modal_Library Classical List.
Theorem implies_to_or_modal :
forall φ ψ,
φ .-> ψ =|= (.~ φ) .\/ ψ .
Proof.
split.
- unfold entails_modal in *.
intros; simpl in *.
destruct H as (?,_).
unfold validate_model in *.
simpl in *; intros.
edestruct classic.
+ exact H0.
+ right; apply H.
apply not_or_and in H0.
destruct H0 as (?, _);
apply NNPP in H0; auto.
- unfold entails_modal in *.
intros; simpl in *.
destruct H as (?, _).
unfold validate_model in *.
simpl in *; intros.
destruct H with w.
+ contradiction.
+ assumption.
Qed.
Theorem double_neg_modal :
forall φ,
(.~ .~ φ) =|= φ.
Proof.
split.
- unfold entails_modal.
simpl in *.
unfold validate_model.
intros.
destruct H as (?, _).
simpl in *.
apply NNPP; auto.
- unfold entails_modal.
simpl in *.
unfold validate_model.
intros; simpl in *.
destruct H as (?, _).
edestruct classic.
+ exact H0.
+ apply NNPP in H0.
exfalso; eauto.
Qed.
Theorem and_to_implies_modal:
forall φ ψ,
φ ./\ ψ =|= .~ (φ .-> .~ ψ).
Proof.
split.
- unfold entails_modal, validate_model.
simpl in *; intros.
unfold validate_model in *.
simpl in *.
destruct H as (?, _).
unfold not; intros; apply H0.
+ destruct H with (w:=w); auto.
+ destruct H with (w:=w); auto.
- unfold entails_modal.
simpl in *; intros.
unfold validate_model in *.
intros; simpl in *.
destruct H as (?, _).
split.
+ edestruct classic.
* exact H0.
* exfalso. unfold not in H.
apply H with (w:=w). intros;
contradiction.
+ edestruct classic.
* exact H0.
* exfalso; unfold not in H;
apply H with (w:=w).
intros; contradiction.
Qed.
Theorem diamond_to_box_modal:
forall φ,
.<> φ =|= .~ .[] .~ φ.
Proof.
split.
- unfold entails_modal, validate_model in *.
simpl in *; intros.
destruct H as (?, _).
unfold validate_model in H; simpl in H.
edestruct classic.
+ exact H0.
+ unfold not; intros.
destruct H with (w:=w).
apply H1 with (w':=x).
destruct H2; auto.
destruct H2; auto.
- intros. unfold entails_modal in *.
simpl in *.
unfold validate_model in *.
simpl in *.
unfold not in *.
intros.
destruct H as (?, _).
edestruct classic.
+ exact H0.
+ exfalso; apply H with (w:=w);
intros.
apply H0; exists w';
split; auto; auto.
Qed.