lemma A.6

theories/Section5.v

@@ -140,6 +140,16 @@ Proof.
   (* TODO: fix *)
 Admitted.
 
+Lemma lemma_A_4_2_simple : forall Phi A, |-- [A](Phi.[ren (+1)]) ->> A.[ren (+1)] -> |-- [E]Phi ->> A.
+Proof.
+  move => Phi A H.
+  apply: gqm_mp; last by apply: gqm_topI.
+  apply (tac_rewrite (fun X => X) _ _ (gqm_equiv_comm (gqm_andImpEquiv _ _ _))).
+  apply: lemma_A_4_2.
+  apply (tac_rewrite (fun X => X) _ _ (gqm_andImpEquiv _ _ _)).
+  by apply: gqm_mp; first by apply: gqm_discard.
+Qed.
+
 (** *** Lemma A.5 *)
 (* p is shifted out of the Global Naming Context *)
 Lemma lemma_A_5_1_1 : forall A B, |-- A ->> B -> |-- [A]A ->> [A]B.
@@ -181,13 +191,98 @@ Proof.
     by apply: gqm_chain.
   }
   (* (5) *)
-  have H5 : (|-- [E] A ->> [E] B). {
-    apply: gqm_mp; last by apply: gqm_topI.
-    apply (tac_rewrite (fun X => X) _ _ (gqm_equiv_comm (gqm_andImpEquiv _ _ _))).
-    apply: lemma_A_4_2.
-    apply (tac_rewrite (fun X => X) _ _ (gqm_andImpEquiv _ _ _)).
-    apply: gqm_mp; first by apply: gqm_discard.
-    done.
-  }
-  done.
+  by apply: lemma_A_4_2_simple.
+Qed.
+
+Lemma lemma_A_5_2_1 : forall A B, |-- A ->> B -> |-- <A>A ->> <A>B.
+Proof.
+  move => A B Himp.
+  apply: (tac_rewrite (fun X => X ->> _) _ _ (lemma_A_2_2 _)).
+  apply: (tac_rewrite (fun X => _ ->> X) _ _ (lemma_A_2_2 _)).
+  apply: gqm_mp; first by apply: gqm_contrap.
+  apply: lemma_A_5_1_2.
+    by apply: gqm_mp; first by apply: gqm_contrap.
+Qed.
+
+Lemma lemma_A_5_2_2 : forall A B, |-- A ->> B -> |-- <E>A ->> <E>B.
+Proof.
+  move => A B Himp.
+  apply: (tac_rewrite (fun X => X ->> _) _ _ (lemma_A_2_1 _)).
+  apply: (tac_rewrite (fun X => _ ->> X) _ _ (lemma_A_2_1 _)).
+  apply: gqm_mp; first by apply: gqm_contrap.
+  apply: lemma_A_5_1_1.
+    by apply: gqm_mp; first by apply: gqm_contrap.
+Qed.
+
+(** *** Lemma 5.3 *)
+
+Lemma lemma_5_3 : forall Q A B, |-- A ->> B -> |-- (quant_to_form Q)A ->> (quant_to_form Q)B.
+Proof.
+  case => /=.
+  - apply: lemma_A_5_1_1.
+  - apply: lemma_A_5_2_1.
+  - apply: lemma_A_5_1_2.
+  - apply: lemma_A_5_2_2.
+Qed.
+
+(** ** Lemma A.6 *)
+
+Lemma lemma_A_6_1_1 : forall A, |-- [A]A ->> [E] A.
+Proof.
+  move => A.
+  (* A with skipped global r *)
+  have H := (lemma_A_4_1 (A._[ren_ (0.: (+2)) ]) (Var 0)).
+  (* remove global r*)
+  have H2 := (gqm_subst _ (ren_ (0 .: id)) H).
+  rewrite /subst_ /ren_ in H2.
+  asimpl in H2.
+  by [].
+Qed.
+
+Lemma lemma_A_6_1_2 : forall A, |-- <A>A ->> <E> A.
+Proof.
+  move => A.
+  apply: (tac_rewrite (fun X => X ->> _) _ _ (lemma_A_2_2 _)).
+  apply: (tac_rewrite (fun X => _ ->> X) _ _ (lemma_A_2_1 _)).
+  apply: gqm_mp; first by apply: gqm_contrap.
+  by apply: lemma_A_6_1_1.
+Qed.
+
+Lemma lemma_A_6_2_1 : forall A, |-- [E](A.[ren (+1)]) ->> [A](A.[ren (+1)]).
+Proof.
+  move => A.
+  apply: lemma_A_4_2_simple.
+  asimpl.
+    by apply: gqm_id.
+Qed.
+
+Lemma lemma_A_6_2_2 : forall A, |-- <E>(A.[ren (+1)]) ->> <A>(A.[ren (+1)]).
+Proof.
+  move => A.
+  apply: (tac_rewrite (fun X => X ->> _) _ _ (lemma_A_2_1 _)).
+  apply: (tac_rewrite (fun X => _ ->> X) _ _ (lemma_A_2_2 _)).
+  apply: gqm_mp; first by apply: gqm_contrap.
+  have H := (lemma_A_6_2_1 (-! A)).
+  by asimpl in H.
 Qed.
+
+Lemma lemma_A_6_3_1 : forall A, |-- [A]A ->> <A>A.
+Proof.
+  move => A.
+  rewrite /DiamondAll /Exists.
+  apply: lemma_A_1.
+  apply: gqm_mp; first by apply: gqm_contrap3.
+  have H := (gqm_AE (-! A._[ren_ (+1)]) (Var 0)).
+  rewrite /subst_ /ren_ in H.
+  by asimpl in H.
+Qed.
+
+Lemma lemma_A_6_3_2 : forall A, |-- [E]A ->> <E>A.
+Proof.
+  move => A.
+  rewrite /SquareExists /DiamondExists.
+  (* other proof than in the paper *)
+  apply: gqm_mp; first by apply: gqm_contrap.
+  apply: (tac_rewrite (fun X => [A] -! A ->> [A] -! (|A| X)) _ _ (gqm_dnegEquiv _)).
+  by apply: lemma_A_6_3_1.
+Qed.
\ No newline at end of file