Newer
Older
(** * Proofs for Section 5
everything here is based on the numbering in the extendend report
*)
Require Import GQM.Base.
Require Import GQM.GQM.
Require Import GQM.GQMDeduction.
Require Import GQM.GQMClassicalWithTactics.
Lemma lemma_A_1 : forall A B, |-- A ->> B -> |-- [A]A ->> [A]B.
move => A B HA.
have HB := (gqm_Anec _ HA).
eauto with GQMDB.
Qed.
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
(** *** Lemma A.2 *)
Lemma lemma_A_2_1 : forall A, |-- <E>A <<->> -![A]-!A.
Proof.
move => A.
unfold DiamondExists.
apply: gqm_equiv_id.
Qed.
Lemma lemma_A_2_2 : forall A, |-- <A>A <<->> -![E]-!A.
Proof.
move => A.
rewrite /DiamondAll /SquareExists /Exists.
hSplit.
- apply: gqm_mp; first by apply: gqm_contrap3.
by hAndDestruct (lemma_A_2_1 (|A| -! A)).
- apply: gqm_mp; first by apply: gqm_contrap2.
by hAndDestruct (lemma_A_2_1 (|A| -! A)).
Qed.
(* TODO: this proof is quite long, whereas it is not very difficult. find a way to shorten it *)
Lemma lemma_A_2_3 : forall A, |-- [A]A <<->> -!<E>-!A.
Proof.
move => A.
hSplit.
- apply: gqm_mp; first by apply: gqm_contrap3.
apply: gqm_mp.
+ apply: gqm_mp; first by apply: (gqm_chain _ (-! ([A] -! -! A))).
apply: gqm_mp; first by apply: gqm_contrap.
apply: lemma_A_1.
apply: gqm_dnegI.
+ by hAndDestruct (lemma_A_2_1 (-! A)).
- apply: gqm_mp; first by apply: gqm_contrap2.
apply: gqm_mp.
+ apply: gqm_mp; first by apply: (gqm_chain _ (-! ([A] -! -! A))).
apply: gqm_mp; first by apply: gqm_contrap.
by apply: gqm_id.
+ apply: gqm_mp; first by apply: gqm_contrap.
apply: lemma_A_1.
by apply: gqm_dnegE.
Qed.
Lemma lemma_A_2_4 : forall A, |-- [E]A <<->> -!<A>-!A.
Proof.
move => A.
hSplit.
- apply: gqm_mp.
+ apply: gqm_mp; first by apply: (gqm_chain _ (([E] -! -! A))).
apply: gqm_mp; first by apply: gqm_contrap3.
by hAndDestruct (lemma_A_2_2 (-! A)).
+ rewrite /SquareExists /DiamondExists.
apply: gqm_mp; first by apply: gqm_contrap.
apply: lemma_A_1.
apply: gqm_mp; first by apply: gqm_contrap.
apply: lemma_A_1.
asimpl.
by apply: gqm_appl2.
- apply: gqm_mp; first by apply: gqm_contrap2.
apply: gqm_mp.
+ apply: gqm_mp; first by apply: (gqm_chain _ (-! ([E] -! -! A))).
by hAndDestruct (lemma_A_2_2 (-! A)).
+ apply: gqm_mp; first by apply: gqm_contrap.
rewrite /SquareExists /DiamondExists.
apply: gqm_mp; first by apply: gqm_contrap.
apply: lemma_A_1.
apply: gqm_mp; first by apply: gqm_contrap.
apply: lemma_A_1.
asimpl.
by apply: gqm_dnegE.
Qed.
(** *** Proof of Lemma 5.2 *)
Lemma lemma_5_2 : forall A, (|-- [A]A <<->> [A](A.[change_top (Var 0)])).
Proof.
(* trivial, but need functional extensionality*)
Abort.
(** ** Lemma 5.3 *)