From b5a1504c80a5ab1bb80de7edb45af13c095909b0 Mon Sep 17 00:00:00 2001
From: Mackie Loeffel <mackie.loeffel@web.de>
Date: Thu, 26 Apr 2018 16:29:00 +0200
Subject: [PATCH] moved classical lemmas to gqmClassical

---
 _CoqProject             |   1 +
 theories/GQMClassical.v | 264 ++++++++++++++++++++++++++++++++++++++++
 theories/GQMDeduction.v | 261 ---------------------------------------
 3 files changed, 265 insertions(+), 261 deletions(-)
 create mode 100644 theories/GQMClassical.v

diff --git a/_CoqProject b/_CoqProject
index 624a5c0..b49dedc 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -3,5 +3,6 @@
 -arg -w -arg -notation-overridden
 theories/Base.v
 theories/GQM.v
+theories/GQMClassical.v
 theories/GQMDeduction.v
 lib/LibTactics.v
\ No newline at end of file
diff --git a/theories/GQMClassical.v b/theories/GQMClassical.v
new file mode 100644
index 0000000..f55195a
--- /dev/null
+++ b/theories/GQMClassical.v
@@ -0,0 +1,264 @@
+Require Import GQM.Base.
+Require Import GQM.GQM.
+Require Import GQM.GQMDeduction.
+
+(** Lemmas for classical tautologies *)
+
+Lemma gqm_negE : forall f, |-- (Bot ->> f).
+  move => f.
+  by apply: gqm_AE.
+Qed.
+
+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.
+
+Lemma gqm_id' : forall A, |-- (A ->> A).
+  eauto with GQMDB.
+  Unshelve.
+  apply: (Var 0).
+  apply: (Var 0).
+Qed.
+
+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.
+
+Lemma gqm_appl : forall A B, |-- ((A ->> B) ->> A ->> B).
+Proof.
+  eauto with GQMDB.
+Qed.
+
+Lemma gqm_appl2 : forall A B, |-- (A ->> (A ->> B) ->> B).
+Proof.
+  eauto with GQMDB.
+  Unshelve.
+  apply: (Var 0).
+  apply: (Var 0).
+Qed.
+
+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 gqm_discard : forall A B C, |-- (A ->> C) ->> (B ->> A ->> C).
+Proof.
+  eauto with GQMDB.
+Qed.
+
+Lemma gqm_discardr : forall A B C, |-- (A ->> C) ->> (A ->> B ->> C).
+Proof.
+  eauto with GQMDB.
+Qed.
+
+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_discardIr : forall A B C, |-- (A ->> B ->> A ->> C) ->> (A ->> B ->> C).
+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.
+  unfold Neg.
+  apply: gqm_mp.
+  - apply: gqm_swap.
+  - apply: gqm_appl.
+Qed.
+
+Lemma gqm_dnegE : forall A, |-- (-! -! A ->> A).
+Proof.
+  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_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.
+  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_andE1 : forall A B, |-- (A & B) ->> A.
+Proof.
+  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 => 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_orI1 : forall A B, |-- A ->> A ||| B.
+Proof.
+  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.
+  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.
diff --git a/theories/GQMDeduction.v b/theories/GQMDeduction.v
index be6f6bc..1d85142 100644
--- a/theories/GQMDeduction.v
+++ b/theories/GQMDeduction.v
@@ -16,264 +16,3 @@ Inductive GQMded: form -> Prop :=
 
 Notation "'|--' A"  := (GQMded A) (at level 80, no associativity).
 Hint Constructors GQMded : GQMDB.
-
-(** Lemmas for classical tautologies *)
-
-Lemma gqm_negE : forall f, |-- (Bot ->> f).
-  move => f.
-  by apply: gqm_AE.
-Qed.
-
-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.
-
-Lemma gqm_id' : forall A, |-- (A ->> A).
-  eauto with GQMDB.
-  Unshelve.
-  apply: (Var 0).
-  apply: (Var 0).
-Qed.
-
-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.
-
-Lemma gqm_appl : forall A B, |-- ((A ->> B) ->> A ->> B).
-Proof.
-  eauto with GQMDB.
-Qed.
-
-Lemma gqm_appl2 : forall A B, |-- (A ->> (A ->> B) ->> B).
-Proof.
-  eauto with GQMDB.
-  Unshelve.
-  apply: (Var 0).
-  apply: (Var 0).
-Qed.
-
-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 gqm_discard : forall A B C, |-- (A ->> C) ->> (B ->> A ->> C).
-Proof.
-  eauto with GQMDB.
-Qed.
-
-Lemma gqm_discardr : forall A B C, |-- (A ->> C) ->> (A ->> B ->> C).
-Proof.
-  eauto with GQMDB.
-Qed.
-
-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_discardIr : forall A B C, |-- (A ->> B ->> A ->> C) ->> (A ->> B ->> C).
-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.
-  unfold Neg.
-  apply: gqm_mp.
-  - apply: gqm_swap.
-  - apply: gqm_appl.
-Qed.
-
-Lemma gqm_dnegE : forall A, |-- (-! -! A ->> A).
-Proof.
-  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_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.
-  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_andE1 : forall A B, |-- (A & B) ->> A.
-Proof.
-  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 => 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_orI1 : forall A B, |-- A ->> A ||| B.
-Proof.
-  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.
-  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.
-- 
GitLab