Newer
Older
Definition context := Ensemble form.
Definition empty_con : context := Empty_set form.
Definition context_cons (c : context) (o : form) : context :=
Add form c o.
Definition elem (o : form) (c : context) := In form c o.
Notation " '{}' " := empty_con (at level 50).
Notation " c ',,' o " := (context_cons c o)
(at level 45, left associativity).
(** Definition *)
| gqm_in G f1: elem f1 G -> GQMded G f1
| gqm_impI G f1 f2: GQMded (G,,f1) f2 -> GQMded G (f1 ->> f2)
| gqm_impE G f1 f2: GQMded G f1 -> GQMded G (f1 ->> f2) -> GQMded G f2
| gqm_dneg G f: GQMded G (-! (-! f) ->> f)
| gqm_ADist G f1 f2: GQMded G ([A](f1 ->> f2) ->> ([A]f1 ->> [A]f2))
| gqm_AE G f1 f2: GQMded G ([A]f1 ->> (f1.[f2.: ids])).
Infix "|--" := GQMded (at level 80, no associativity).
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
(** Basic facts *)
(** cut elimination *)
Lemma cut_elim : forall G f1 f2, G |-- f1 -> G,,f1 |-- f2 -> G |-- f2.
Proof.
eauto with GQMDB.
Qed.
(** context *)
Lemma context_weakening : forall G G' f, Included form G G' -> G |-- f -> G' |-- f.
Proof.
move => G f1 f2 Hin H.
elim: H f1 Hin; eauto with GQMDB; clear G f2.
- move => G f1 Helem G2 Hinc.
apply: gqm_in.
by apply: Hinc.
- move => G f1 f2 Hi IH G2 Hinc.
apply: gqm_impI.
apply: IH.
unfold Included.
move => _ [x Hx| x Hx].
+ apply: Union_introl.
by eauto.
+ by apply: Union_intror.
Qed.
(** Lemmas for classical tautologies *)
Lemma gqm_botE : forall G f, G |-- (Bot ->> f).
move => G f.
by apply: gqm_AE.
Qed.
Lemma gqm_em : forall G f, G |-- (-! f ||| f).
Proof.
by apply: gqm_dneg.
Qed.
Lemma gqm_andI : forall G f1 f2, G |-- f1 -> G |-- f2 -> G |-- (f1 & f2).
Proof.
move => G f1 f2 Hf1 Hf2.
unfold And.
apply: gqm_impI.
unfold Neg.
have Hn : (G,, (f1 ->> f2 ->> Bot) |-- f2 ->> Bot). {
apply: (gqm_impE _ f1).
- apply: (context_weakening G); eauto.
by apply: Union_introl.
- apply: gqm_in.
by apply: Union_intror.
}
apply: (gqm_impE _ f2).
- apply: (context_weakening G); eauto.
by apply: Union_introl.
- apply: cut_elim.
+ by apply: Hn.
+ apply: gqm_in.
by apply: Union_intror.
Qed.
Lemma gqm_andE1 : forall G f1 f2, G |-- (f1 & f2) -> G |-- f1.
Proof.
move => G f1 f2 Hand.
unfold And in Hand.
Lemma gqm_orI1 : forall G f1 f2, G |-- f1 -> G |-- (f1 ||| f2).
apply: gqm_impI.
apply: gqm_impE; last by apply: gqm_botE.
apply: (gqm_impE _ f1).
- apply: cut_elim.
+ apply: (context_weakening G); try by apply: Union_introl.
by apply: Hf1.
+ apply: gqm_in.
by apply: Union_intror.
- apply: gqm_in.
by apply: Union_intror.
Qed.
Lemma gqm_orI2 : forall G f1 f2, G |-- f2 -> G |-- (f1 ||| f2).
move => G f1 f2 Hf1.
unfold Or.
apply: gqm_impI.
apply: (context_weakening G); eauto.
apply: Union_introl.
Qed.
Lemma gqm_orE : forall G f1 f2 f3, G |-- (f1 ||| f2) -> G,,f1 |-- f3 -> G,,f2 |-- f3 -> G |-- f3.
move => G f1 f2 f3 Hor Hf1 Hf2.
unfold Or in Hor.