finished lemma A.2 and started with some tactics

.gitignore

@@ -8,3 +8,5 @@
 *.aux
 Makefile.coq
 Makefile.coq.conf
+all.pdf
+all-gal.pdf
\ No newline at end of file

README

+This project was built with coq version 8.7.2.
+
+To build the project run
+$ make
+
+There are several ways to build a documentation.
+- HTML with proofs:     $ make html
+- HTML without proofs:  $ make gallinahtml
+- pdf with proofs:      $ make all.pdf
+- pdf without proofs:   $ make all-gal.pdf
+HTML documentation can be found in the html subfolder, pdf documentation is created in the main folder as all.pdf or all-gal.pdf.

_CoqProject

@@ -4,6 +4,8 @@
 theories/Base.v
 theories/GQM.v
 theories/GQMClassical.v
+theories/GQMClassicalWithTactics.v
 theories/GQMDeduction.v
+theories/GQMTactics.v
 theories/Section5.v
 lib/LibTactics.v
\ No newline at end of file

theories/GQM.v

@@ -14,14 +14,30 @@ Instance SubstLemmas_form : SubstLemmas form. derive. Qed.
 Notation "'[A]' B"   := (SquareAll B) (at level 74, right associativity).
 Notation "|[]| A"   := (Box A) (at level 74, right associativity).
 Notation "A '->>' B" := (Imp A B) (at level 77, right associativity).
+
 Definition Bot := [A] (Var 0).
 Definition Neg A := A ->> Bot.
 Notation "'-!' A" := (Neg A) (at level 73, right associativity).
+
 Definition Or A B := (-! A ->> B).
-Notation "A '|||' B" := (Or A B) (at level 76, right associativity).
 Definition And A B := -! ( A ->> -! B).
+
+Notation "A '|||' B" := (Or A B) (at level 76, right associativity).
 Infix "&" :=  And (at level 75, right associativity).
-Notation "A '<<->>' B" := ((A ->> B) & (B ->> A)) (at level 78).
+Definition Equiv A B := ((A ->> B) & (B ->> A)).
+Notation "A '<<->>' B" := (Equiv A B) (at level 78).
+
+Definition All A := [A](A.[ren(+1)]).
+Notation "'|A|' B" := (All B) (at level 74, right associativity).
+Definition Exists A := -!|A|-!A.
+Notation "'|E|' B" := (Exists B) (at level 74, right associativity).
+
+Definition DiamondAll A := [A]|E|A.
+Notation "'<A>' B" := (DiamondAll B) (at level 74, right associativity).
+Definition DiamondExists A := -![A]-!A.
+Notation "'<E>' B" := (DiamondExists B) (at level 74, right associativity).
+Definition SquareExists A := <E>|A|A.
+Notation "'[E]' B" := (SquareExists B) (at level 74, right associativity).
 
 (** ** Decidable Equality *)
 

theories/GQMClassical.v

@@ -133,6 +133,12 @@ Proof.
   apply: gqm_dnegE.
 Qed.
 
+Lemma gqm_contrap3: forall A B, |-- ((A ->> -! B) ->> (B ->> -! A)).
+Proof.
+  move => A B.
+  apply: gqm_swap.
+Qed.
+
 Lemma gqm_negE2 : forall A B, |-- (A ->> -! B) ->> (A ->> B) ->> -! A.
 Proof.
   move => A B.

theories/GQMClassicalWithTactics.v

+(** * Classical Lemmas, where the Proofs use tactics *)
+
+Require Import GQM.Base.
+Require Import GQM.GQM.
+Require Import GQM.GQMDeduction.
+Require Export GQM.GQMClassical.
+Require Export GQM.GQMTactics.
+
+Lemma gqm_equiv_id : forall A, |-- A <<->> A.
+Proof.
+  hSplit; apply: gqm_id.
+Qed.
\ No newline at end of file

theories/GQMDeduction.v

@@ -24,7 +24,10 @@ Inductive GQMded: form -> Prop :=
 | gqm_BoxCon A B: GQMded ([A](A <<->> B) ->> (|[]|A <<->> |[]| B))
 
 | gqm_mp A B: GQMded (A ->> B) -> GQMded A -> GQMded B
-| gqm_Anec A: GQMded A -> GQMded ([A]A.[ren (+1)])
+ (* no [ren (+1)] here, because p does not have to be fresh
+   TODO: think, whether this makes sense
+*)
+| gqm_Anec A: GQMded A -> GQMded ([A]A)
 | gqm_univgen A B: GQMded (A ->> [A]B) -> GQMded (A ->> [A][A](B.[ren(+1)]))
 .
 

theories/GQMTactics.v

+(** * Different Tactics to make working with GQM easier *)
+
+Require Import GQM.Base.
+Require Import GQM.GQM.
+Require Import GQM.GQMDeduction.
+Require Import GQM.GQMClassical.
+
+(** ** hSplit
+ inspired from iSplit in https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/theories/proofmode/tactics.v#L739
+ *)
+
+Lemma tac_and_split : forall A B, |-- A -> |-- B -> |-- A & B.
+Proof.
+  move => A B HA HB.
+  apply: gqm_mp.
+  - by apply: gqm_mp; first by apply: gqm_andI.
+  - done.
+Qed.
+
+Tactic Notation "hSplit" := move => *; apply: tac_and_split.
+
+(** ** hAndDestruct *)
+
+Lemma tac_and_destruct_lemma : forall A B, |-- A & B -> |-- A /\ |-- B.
+Proof.
+  move => A B.
+  split.
+  - by apply: gqm_mp; first by apply: (gqm_andE1 A B).
+  - by apply: gqm_mp; first by apply: (gqm_andE2 A B).
+Qed.
+
+Tactic Notation "hAndDestruct" constr(H) := case: (tac_and_destruct_lemma _ _ H).
\ No newline at end of file

theories/Section5.v

+(** * Proofs for Section 5
+everything here is based on the numbering in the extendend report
+*)
+
 Require Import GQM.Base.
 Require Import GQM.GQM.
 Require Import GQM.GQMDeduction.
-Require Import GQM.GQMClassical.
+Require Import GQM.GQMClassicalWithTactics.
 
-Lemma lemma_5_2 : forall A, (|-- [A]A <<->> [A](A.[change_top (Var 0)])).
-Proof.
-  (* trivial, but need functional extensionality*)
-Abort.
+(** ** Lemma 5.2 *)
 
-Lemma lemma_A_1 : forall A B, |-- A ->> B -> |-- [A](A.[ren(+1)]) ->> [A](B.[ren(+1)]).
+Lemma lemma_A_1 : forall A B, |-- A ->> B -> |-- [A]A ->> [A]B.
   move => A B HA.
   have HB := (gqm_Anec _ HA).
   eauto with GQMDB.
 Qed.
+
+(** *** Lemma A.2 *)
+
+Lemma lemma_A_2_1 : forall A, |-- <E>A <<->> -![A]-!A.
+Proof.
+  move => A.
+  unfold DiamondExists.
+  apply: gqm_equiv_id.
+Qed.
+
+Lemma lemma_A_2_2 : forall A, |-- <A>A <<->> -![E]-!A.
+Proof.
+  move => A.
+  rewrite /DiamondAll /SquareExists /Exists.
+  hSplit.
+  - apply: gqm_mp; first by apply: gqm_contrap3.
+    by hAndDestruct (lemma_A_2_1 (|A| -! A)).
+  - apply: gqm_mp; first by apply: gqm_contrap2.
+    by hAndDestruct (lemma_A_2_1 (|A| -! A)).
+Qed.
+
+(* TODO: this proof is quite long, whereas it is not very difficult. find a way to shorten it *)
+Lemma lemma_A_2_3 : forall A, |-- [A]A <<->> -!<E>-!A.
+Proof.
+  move => A.
+  hSplit.
+  - apply: gqm_mp; first by apply: gqm_contrap3.
+    apply: gqm_mp.
+    + apply: gqm_mp; first by apply: (gqm_chain _ (-! ([A] -! -! A))).
+      apply: gqm_mp; first by apply: gqm_contrap.
+      apply: lemma_A_1.
+      apply: gqm_dnegI.
+    + by hAndDestruct (lemma_A_2_1 (-! A)).
+  - apply: gqm_mp; first by apply: gqm_contrap2.
+    apply: gqm_mp.
+    + apply: gqm_mp; first by apply: (gqm_chain _ (-! ([A] -! -! A))).
+      apply: gqm_mp; first by apply: gqm_contrap.
+        by apply: gqm_id.
+    + apply: gqm_mp; first by apply: gqm_contrap.
+      apply: lemma_A_1.
+      by apply: gqm_dnegE.
+Qed.
+
+Lemma lemma_A_2_4 : forall A, |-- [E]A <<->> -!<A>-!A.
+Proof.
+  move => A.
+  hSplit.
+  - apply: gqm_mp.
+    + apply: gqm_mp; first by apply: (gqm_chain _ (([E] -! -! A))).
+      apply: gqm_mp; first by apply: gqm_contrap3.
+        by hAndDestruct (lemma_A_2_2 (-! A)).
+    + rewrite /SquareExists /DiamondExists.
+      apply: gqm_mp; first by apply: gqm_contrap.
+      apply: lemma_A_1.
+      apply: gqm_mp; first by apply: gqm_contrap.
+      apply: lemma_A_1.
+      asimpl.
+      by apply: gqm_appl2.
+  - apply: gqm_mp; first by apply: gqm_contrap2.
+    apply: gqm_mp.
+    + apply: gqm_mp; first by apply: (gqm_chain _ (-! ([E] -! -! A))).
+        by hAndDestruct (lemma_A_2_2 (-! A)).
+    + apply: gqm_mp; first by apply: gqm_contrap.
+      rewrite /SquareExists /DiamondExists.
+      apply: gqm_mp; first by apply: gqm_contrap.
+      apply: lemma_A_1.
+      apply: gqm_mp; first by apply: gqm_contrap.
+      apply: lemma_A_1.
+      asimpl.
+      by apply: gqm_dnegE.
+Qed.
+
+(** *** Proof of Lemma 5.2 *)
+
+Lemma lemma_5_2 : forall A, (|-- [A]A <<->> [A](A.[change_top (Var 0)])).
+Proof.
+  (* trivial, but need functional extensionality*)
+Abort.
+
+(** ** Lemma 5.3 *)