lemma a.5 (i)

theories/GQM.v

@@ -192,4 +192,14 @@ Fixpoint free_in(v: var)(f: form) : bool :=
   | Imp A B => free_in v A || free_in v B
   | Box A => free_in v A
   | SquareAll A => free_in (S v) A
-  end.
\ No newline at end of file
+  end.
+
+Lemma ids_0_bot : ([A] ids 0) = Bot.
+Proof.
+    by [].
+Qed.
+
+Lemma ids_0_neg : forall A, (A ->> ([A] ids 0)) = -! A.
+Proof.
+    by [].
+Qed.
\ No newline at end of file

theories/Section5.v

@@ -96,8 +96,8 @@ Definition lemma_5_2 := lemma_A_3.
 
 (** *** Lemma A.4 *)
 (*
-  phi/A: 0->p, 1 -> r
-  psi/B: 0->r
+  phi/A: 0->p, 1 -> r, 2 -> next element of global naming context after r
+  psi/B: 0->(local)r, 1 -> first element of global naming context after r
   Global Naming Context: 0 -> r
   .[ren (+1)] to express, that the global r cannot occur in the left term, because it is shadowed by the r in the binder
  *)
@@ -125,33 +125,69 @@ Proof.
   by apply: H3.
 Qed.
 
-Lemma lemma_A_4_2 : forall X Phi A, |-- (X & [A](Phi.[ren (+1)])) ->> A -> |-- (X & [E]Phi) ->> A.
+(*
+  Global Naming Context antecedent: 0 -> q,...
+  Global Naming Context consequent: ...
+*)
+Lemma lemma_A_4_2 : forall X Phi A, |-- (X.[ren (+1)] & [A](Phi.[ren (+1)])) ->> A.[ren (+1)] -> |-- (X & [E]Phi) ->> A.
 Proof.
   move => X Phi A H.
-  have H2 : (|-- (X & -! A) ->> -![A](Phi.[ren (+1)])) by apply: gqm_mp; first by apply: gqm_contrapAndR.
-  Fail have H3 : (|-- (X & -! A) ->> [A](-![A](Phi.[ren (+1)])).[ren(+1)]) by apply: gqm_univgen.
+  (* (1) *)
+  (* (2) *)
+  have H2 : (|-- (X.[ren (+1)] & -! A.[ren (+1)]) ->> -![A](Phi.[ren (+1)])) by apply: gqm_mp; first by apply: gqm_contrapAndR.
+  (* (3) *)
+  Fail have H3 : (|-- (X & -! A) ->> [A](-![A](Phi.[ren (+1)]))) by apply: gqm_univgen.
   (* TODO: fix *)
 Admitted.
 
 (** *** 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.
 Proof.
     by apply: lemma_A_1.
 Qed.
 
+(* p is shifted out of the Global Naming Context *)
 Lemma lemma_A_5_1_2 : forall A B, |-- A ->> B -> |-- [E]A ->> [E]B.
 Proof.
   move => A B Himp.
+  (* (1) *)
+  (* (2) *)
   have H2 : (|-- [A](A.[ren (+1)]) ->> [A](B.[ren (+1)])). {
     apply: lemma_A_5_1_1.
-    have H := (gqm_subst _ (@ren _ Ids_form (+1)) Himp).
+    have H := (gqm_subst _ (ren_ (+1)) Himp).
     by asimpl in H.
   }
-  have H3 : (|-- [A](B.[ren (+1)]) ->> [E]B). {
-    suff ->:(@ren _ Ids_form (+1) = change_top (Var 0)) by apply: lemma_A_4_1.
-    apply: functional_extensionality => n.
-    case: n => // /=.
+  (* (3) *)
+  (* second ren (+1), because the second part does not refer to the global p*)
+  have H3 : (|-- [A](B.[ren (+1)]) ->> ([E]B).[ren (+1)]). {
+    (* Naming context for lemma_A_4_1:
+     * r -> 0, p -> 1, (Var 1) refers to p in global context
+     *)
+    have H' := (lemma_A_4_1 (B._[ren_ (0 .: (+3))]) (Var 1)).
+    rewrite /ren_ /subst_ /SquareExists /DiamondExists /All in H'.
+    asimpl in H'.
+    asimpl.
+    rewrite !ids_0_neg.
+    (* now we need to remove r->0 from the naming context *)
+    have H2' := (gqm_subst _ (ren_ (0 .: id)) H').
+    rewrite /ren_ in H2'.
+    by asimpl in H2'.
   }
-
-  (* TODO*)
-Abort.
+  (* (4) *)
+  have H4 : (|-- [A](A.[ren (+1)]) ->> ([E]B).[ren (+1)]). {
+    apply: gqm_mp; last by apply: H2.
+    apply: gqm_mp; last by apply: H3.
+    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.
+Qed.