Skip to content
Snippets Groups Projects
Commit b5a1504c authored by Mackie Loeffel's avatar Mackie Loeffel
Browse files

moved classical lemmas to gqmClassical

parent 376ff567
No related branches found
No related tags found
No related merge requests found
Pipeline #
Hide whitespace changes
Inline Side-by-side
_CoqProject
+ 1
− 0
View file @ b5a1504c
......@@ -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
theories/GQMClassical.v 0 → 100644
+ 264
− 0
View file @ b5a1504c
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.
theories/GQMDeduction.v
+ 0
− 261
View file @ b5a1504c
......@@ -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.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment