Hilbert style until or elim

theories/GQMDeduction.v

 Require Import GQM.Base.
 Require Import GQM.GQM.
 
-Definition context := Ensemble form.
-
-Definition empty_con : context := Empty_set form.
-
-Definition context_cons (c : context) (o : form) : context :=
- Add form c o.
+(** Definition *)
 
-Definition elem (o : form) (c : context) := In form c o.
+Inductive GQMded: form -> Prop :=
+| gqm_mp A B: GQMded (A ->> B) -> GQMded A -> GQMded B
+| gqm_I1 A B: GQMded (A ->> B ->> A)
+| gqm_I2 A B C: GQMded ((A ->> B ->> C) ->> (A ->> B) ->> A ->> C)
+| gqm_I3 A B: GQMded ((-! A ->> -! B) ->> B ->> A)
+| gqm_swap A B C: GQMded ((A ->> B ->> C) ->> (B ->> A ->> C)) (* TODO prove that this follows from the rest *)
+(* | gqm_dneg f: GQMded (-! (-! f) ->> f) *)
 
-Notation " '{}' " := empty_con (at level 50).
-Notation " c ',,' o " := (context_cons c o)
-  (at level 45, left associativity).
+| gqm_ADist A B: GQMded ([A](A ->> B) ->> ([A]A ->> [A]B))
+| gqm_AE A B: GQMded ([A]A ->> (A.[B.: ids])).
 
+Notation "'|--' A"  := (GQMded A) (at level 80, no associativity).
+Hint Constructors GQMded : GQMDB.
 
-(** Definition *)
+(** Lemmas for classical tautologies *)
 
-Inductive GQMded: context -> form -> Prop :=
-| 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
+Lemma gqm_negE : forall f, |-- (Bot ->> f).
+  move => f.
+  by apply: gqm_AE.
+Qed.
 
-| gqm_dneg G f: GQMded G (-! (-! f) ->> f)
+Lemma gqm_id : forall A, |-- (A ->> A).
+  move => A.
+  have H1 : (|-- A ->> (A ->> A) ->> A) by apply: gqm_I1.
+  have H2 : (|-- (A ->> (A ->> A) ->> A) ->> (A ->> A ->> A) ->> A ->> A) by apply: gqm_I2.
+  have H3 : (|-- (A ->> A ->> A) ->> A ->> A) by apply: gqm_mp; eauto.
+  have H4 : (|-- A ->> A ->> A) by apply: gqm_I1.
+  apply: gqm_mp.
+  - by apply: H3.
+  - by eauto.
+Qed.
 
-| 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])).
+Lemma gqm_id' : forall A, |-- (A ->> A).
+  eauto with GQMDB.
+  Unshelve.
+  apply: (Var 0).
+  apply: (Var 0).
+Qed.
 
-Infix "|--"  := GQMded (at level 80, no associativity).
-Hint Constructors GQMded : GQMDB.
+Lemma gqm_id'' : forall A, |-- (A ->> A).
+  move => A.
+  apply: (gqm_mp (A ->> A ->> A)); last by apply: gqm_I1.
+  apply: (gqm_mp (A ->> (A ->> A) ->> A)); last by apply: gqm_I1.
+  by apply: gqm_I2.
+Qed.
 
-(** Basic facts *)
-(** cut elimination *)
+Lemma gqm_appl : forall A B, |-- ((A ->> B) ->> A ->> B).
+Proof.
+  eauto with GQMDB.
+Qed.
 
-Lemma cut_elim : forall G f1 f2, G |-- f1 -> G,,f1 |-- f2 -> G |-- f2.
+Lemma gqm_appl2 : forall A B, |-- (A ->> (A ->> B) ->> B).
 Proof.
   eauto with GQMDB.
+  Unshelve.
+  apply: (Var 0).
+  apply: (Var 0).
 Qed.
 
-(** context *)
+Lemma gqm_chain : forall A B C, |-- (B ->> C) ->> (A ->> B) ->> (A ->> C).
+Proof.
+  move => A B C.
+  apply: gqm_mp.
+  - apply: gqm_mp.
+    + apply: (gqm_I2 (B ->> C) (A ->> B ->> C) ((A ->> B) ->> A ->> C)).
+    + apply: gqm_mp.
+      * apply: (gqm_I1 ((A ->> B ->> C) ->> (A ->> B) ->> A ->> C) (B ->> C)).
+      * apply: (gqm_I2 A B C).
+  - apply: (gqm_I1 (B ->> C) A).
+Qed.
 
-Lemma context_weakening : forall G G' f, Included form G G' -> G |-- f -> G' |-- f.
+Lemma gqm_discard : forall A B C, |-- (A ->> C) ->> (B ->> A ->> C).
 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.
+  eauto with GQMDB.
 Qed.
 
-(** Lemmas for classical tautologies *)
+Lemma gqm_discardr : forall A B C, |-- (A ->> C) ->> (A ->> B ->> C).
+Proof.
+  eauto with GQMDB.
+Qed.
 
-Lemma gqm_botE : forall G f, G |-- (Bot ->> f).
-  move => G f.
-  by apply: gqm_AE.
+Lemma gqm_discardI : forall A B, |-- (A ->> A ->> B) ->> (A ->> B).
+Proof.
+  move => A B.
+  apply: gqm_mp.
+  - apply: gqm_mp.
+    + apply: gqm_I2.
+      apply: (A ->> A).
+    + apply: gqm_I2.
+  - apply: gqm_mp.
+    + apply: gqm_discard.
+    + apply: gqm_id.
 Qed.
 
-Lemma gqm_em : forall G f, G |-- (-! f ||| f).
+Lemma gqm_discardIr : forall A B C, |-- (A ->> B ->> A ->> C) ->> (A ->> B ->> C).
 Proof.
-  by apply: gqm_dneg.
+  eauto with GQMDB.
 Qed.
 
-Lemma gqm_andI : forall G f1 f2, G |-- f1 -> G |-- f2 -> G |-- (f1 & f2).
+Lemma gqm_dnegI : forall A, |-- (A ->> -! -! A).
 Proof.
-  move => G f1 f2 Hf1 Hf2.
-  unfold And.
-  apply: gqm_impI.
+  move => A.
   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.
+  apply: gqm_mp.
+  - apply: gqm_swap.
+  - apply: gqm_appl.
+Qed.
+
+Lemma gqm_dnegE : forall A, |-- (-! -! A ->> A).
 Proof.
-  move => G f1 f2 Hand.
-  unfold And in Hand.
+  move => A.
+  apply: gqm_mp.
+  - apply: gqm_I3.
+  - apply: gqm_dnegI.
+Qed.
 
+Lemma gqm_em : forall A, |-- (-! A ||| A).
+Proof.
+  apply: gqm_dnegE.
+Qed.
 
+(* Lemma gqm_em : forall f, |-- (-! f ||| f). *)
+(* Proof. *)
+  (* unfold Or. *)
+(* Qed. *)
 
+Lemma gqm_andI : forall A B, |-- (A ->> B ->> A & B).
+Proof.
+  move => A B.
+  unfold And.
+  unfold Neg.
+  apply: gqm_mp.
+  - apply: gqm_mp.
+    + apply: gqm_chain.
+      apply: ((A ->> B ->> Bot) ->> B ->> Bot).
+    + apply: gqm_swap.
+  - apply: gqm_mp.
+    + apply: gqm_swap.
+    + apply: gqm_id.
+Qed.
 
-Lemma gqm_orI1 : forall G f1 f2, G |-- f1 -> G |-- (f1 ||| f2).
+Lemma gqm_andE1 : forall A B, |-- (A & B) ->> A.
 Proof.
-  move => G f1 f2 Hf1.
-  unfold Or.
-  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 => A B.
+  unfold And.
+  unfold Neg.
+  apply: gqm_mp.
+  - apply: gqm_mp.
+    + apply: gqm_chain.
+      apply: (-! -! A).
+    + apply: gqm_dnegE.
+  - unfold Neg.
+    apply: gqm_mp.
+    + apply: gqm_swap.
+    + apply: gqm_mp.
+      * apply: gqm_mp.
+        -- apply: gqm_chain.
+           apply: (A ->> B ->> Bot).
+        -- apply: gqm_appl2.
+      * eauto with GQMDB.
+Qed.
+
+Lemma gqm_andE2 : forall A B, |-- (A & B) ->> B.
 Proof.
-  move => G f1 f2 Hf1.
-  unfold Or.
-  apply: gqm_impI.
-  apply: (context_weakening G); eauto.
-  apply: Union_introl.
+  move => A B.
+  unfold And.
+  unfold Neg.
+  apply: gqm_mp.
+  - apply: gqm_mp.
+    + apply: gqm_chain.
+      apply: (-! -! B).
+    + apply: gqm_dnegE.
+  - unfold Neg.
+    apply: gqm_mp; first by apply: gqm_swap.
+    apply: gqm_mp.
+    + apply: gqm_mp.
+      * apply: gqm_chain.
+           apply: (A ->> B ->> Bot).
+      * apply: gqm_appl2.
+    + apply: gqm_I1.
 Qed.
 
-Lemma gqm_orE : forall G f1 f2 f3, G |-- (f1 ||| f2) -> G,,f1 |-- f3 -> G,,f2 |-- f3 -> G |-- f3.
+Lemma gqm_orI1 : forall A B, |-- A ->> A ||| B.
 Proof.
-  move => G f1 f2 f3 Hor Hf1 Hf2.
-  unfold Or in Hor.
+  move => A B.
+  rewrite /Or /Neg.
+  apply: gqm_mp; first by apply: gqm_swap.
+  apply: gqm_mp; first by apply: gqm_chain.
+  apply: gqm_negE.
+Qed.
+
+Lemma gqm_orI2 : forall A B, |-- B ->> A ||| B.
+Proof.
+  move => A B.
+  rewrite /Or.
+  apply: gqm_I1.
+Qed.
+
+(* Lemma gqm_orE : forall A B C, |-- (A ->> C) ->> (B ->> C) ->> (A ||| B) ->> C. *)
+(* Proof. *)
+  (* move => A B C. *)
+  (* rewrite /Or. *)