finished or elimination

theories/GQMDeduction.v

@@ -8,7 +8,7 @@ Inductive GQMded: form -> Prop :=
 | 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_swap A B C: GQMded ((A ->> B ->> C) ->> (B ->> A ->> C))
 (* | gqm_dneg f: GQMded (-! (-! f) ->> f) *)
 
 | gqm_ADist A B: GQMded ([A](A ->> B) ->> ([A]A ->> [A]B))
@@ -102,6 +102,20 @@ Proof.
   eauto with GQMDB.
 Qed.
 
+Lemma gqm_contrap: forall A B, |-- (A ->> B) ->> (-! B ->> -! A).
+Proof.
+  move => A B.
+  rewrite /Neg.
+  have HA : (|-- (A ->> B) ->> A ->> (B ->> Bot) ->> Bot). {
+    apply: gqm_mp; first by apply: gqm_chain.
+    eauto with GQMDB.
+  }
+  eauto with GQMDB.
+  Unshelve.
+  apply: (Var 0).
+  apply: (Var 0).
+Qed.
+
 Lemma gqm_dnegI : forall A, |-- (A ->> -! -! A).
 Proof.
   move => A.
@@ -124,10 +138,54 @@ Proof.
   apply: gqm_dnegE.
 Qed.
 
-(* Lemma gqm_em : forall f, |-- (-! f ||| f). *)
-(* Proof. *)
-  (* unfold Or. *)
-(* Qed. *)
+Lemma gqm_contrap2: forall A B, |-- ((-! A ->> B) ->> (-! B ->> A)).
+Proof.
+  move => A B.
+  have H : (|-- ((-! A ->> B) ->> (-! B ->> -! -! A))) by apply gqm_contrap.
+  apply: gqm_mp; last by apply: H.
+  apply: gqm_mp; first by apply: gqm_chain.
+  apply: gqm_mp; first by apply: gqm_chain.
+  apply: gqm_dnegE.
+Qed.
+
+Lemma gqm_negE2 : forall A B, |-- (A ->> -! B) ->> (A ->> B) ->> -! A.
+Proof.
+  move => A B.
+  unfold Neg.
+  eauto with GQMDB.
+Qed.
+
+
+Lemma gqm_negE3 : forall A B, |-- (A ->> B) ->> (-! A ->> B) ->> B.
+Proof.
+  move => A B.
+  suff HA : (|-- (A ->> B) ->> (-! B ->> A) ->> B). {
+    apply: gqm_mp; last by apply: HA.
+    clear HA.
+    apply: gqm_mp; first by apply: gqm_chain.
+    apply: gqm_mp; last by apply: (gqm_contrap2 A B).
+    apply: gqm_mp.
+    - apply: gqm_mp.
+      + apply: gqm_chain.
+        apply: ((-! A ->> B) ->> ((-! B ->> A) ->> B) ->> B).
+      + eauto with GQMDB.
+    - apply: gqm_mp.
+      + apply: gqm_chain.
+      + eauto with GQMDB.
+  }
+  suff HA : (|-- (-! B ->> -! A) ->> (-! B ->> A) ->> B). {
+    apply: gqm_mp; last by apply: (gqm_contrap A B).
+    apply: gqm_mp; first by apply: gqm_chain.
+    apply: HA.
+  }
+  apply: gqm_mp; last by apply: (gqm_negE2 (-! B) A).
+  apply: gqm_mp; first by apply: gqm_chain.
+  apply: gqm_mp; first by apply: gqm_chain.
+  apply: gqm_dnegE.
+  Unshelve.
+  apply: (Var 0).
+  apply: (Var 0).
+Qed.
 
 Lemma gqm_andI : forall A B, |-- (A ->> B ->> A & B).
 Proof.
@@ -201,7 +259,21 @@ Proof.
   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. *)
+Lemma gqm_orE : forall A B C, |-- (A ->> C) ->> (B ->> C) ->> (A ||| B) ->> C.
+Proof.
+  move => A B C.
+  rewrite /Or.
+  apply: gqm_mp.
+  - apply: gqm_mp; first by apply: (gqm_negE3 A).
+    apply: gqm_mp; first by apply: gqm_swap.
+    apply: gqm_mp; first by apply: gqm_chain.
+    eauto with GQMDB.
+  - apply: gqm_mp; first by apply: gqm_discardr.
+    apply: gqm_mp; first by apply: gqm_swap.
+    apply: gqm_mp.
+    + apply: gqm_mp.
+      * apply: gqm_chain.
+        apply: ((-! A ->> B) ->> -! A ->> C).
+      * apply: gqm_swap.
+    + apply: gqm_chain.
+Qed.