diff --git a/theories/GQM.v b/theories/GQM.v
index bfdfa3ebba00ce92ae1cefc624bea1e75dec699b..22b9aee28dae33bdfcbc2e79b2b75421135379a9 100644
--- a/theories/GQM.v
+++ b/theories/GQM.v
@@ -201,13 +201,3 @@ Fixpoint free_in(v: var)(f: form) : bool :=
| Box A => free_in v A
| SquareAll A => free_in (S v) A
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
diff --git a/theories/GQMTactics.v b/theories/GQMTactics.v
index 29952c493a72279fd92d001efb1e9932194480c6..51a8a1039bfdb42adb4e09850e314fb162363822 100644
--- a/theories/GQMTactics.v
+++ b/theories/GQMTactics.v
@@ -275,4 +275,17 @@ Local Example rewrite_test_6' : forall A, |-- |A|-!-!A -> |-- |A|A.
Proof.
move => A Himp.
by hRewrite (gqm_dnegEquiv A) (fun X => |A|X).
-Qed.
\ No newline at end of file
+Qed.
+
+(** ** own asimpl, which folds back definitions *)
+Lemma ids_0_bot : ([A] ids 0) = Bot. done. Qed.
+
+Lemma ids_0_neg : forall A, (A ->> ([A] ids 0)) = -! A. done. Qed.
+
+Tactic Notation "own_asimpl" :=
+ asimpl;
+ rewrite ? ids_0_neg. (*This maybe folds back to much: - ? /(And (_) (_)) - ? /(Or (_) (_)). *)
+
+Tactic Notation "own_asimpl" "in" constr(H) :=
+ asimpl in H;
+ rewrite ? ids_0_neg in H. (*This maybe folds back to much: - ? /(And (_) (_)) - ? /(Or (_) (_)). *)
\ No newline at end of file
diff --git a/theories/Section5.v b/theories/Section5.v
index 29d003e48c72103eefd0919fd3cc0547f4df9d7f..437dc9afe457c17d689a37371b04546bc9b92a29 100644
--- a/theories/Section5.v
+++ b/theories/Section5.v
@@ -144,8 +144,7 @@ Proof.
have H5 := (gqm_univgen _ _ H4).
(* (6) *)
have H6 := (gqm_AE ((-! ([A] Phi._[ren_ (+1)]))._[ren_ (+1)]) (Var 0)).
- asimpl in H6.
- rewrite !ids_0_neg in H6.
+ own_asimpl in H6.
(* (7) *)
have H7 := (lemma_A_1 _ _ H6).
(* (8) *)
@@ -199,9 +198,8 @@ Proof.
*)
have H' := (lemma_A_4_1 (B._[ren_ (0 .: (+3))]) (Var 1)).
rewrite /SquareExists /DiamondExists /All in H'.
- asimpl in H'.
- asimpl.
- rewrite !ids_0_neg.
+ own_asimpl in H'.
+ own_asimpl.
(* now we need to remove r->0 from the naming context *)
have H2' := (gqm_subst _ (ren_ (0 .: id)) H').
by asimpl in H2'.
diff --git a/theories/Section7.v b/theories/Section7.v
index abd33fff147485a11b5ae545e0443b960defac3c..0c137b2ed7275e0f6f249ed4ce9e6f8179bb5944 100644
--- a/theories/Section7.v
+++ b/theories/Section7.v
@@ -9,6 +9,7 @@ Require Import GQM.GQMClassicalWithTactics.
Require Import GQM.Section5.
(** ** Lemma A.8 *)
+
Lemma lemma_A_8_1 : forall A B, |-- (|A| A & [A]B) <<->> [A](A.[ren (+1)] & B).
Proof.
move => A B.
@@ -21,8 +22,8 @@ Proof.
apply (tac_rewrite (fun X => _ ->> X) (lemma_A_7_2_1 _ _)).
(* (2) *)
rewrite /All.
- asimpl.
- rewrite !ids_0_neg -/(And ([A] A._[ren_ (+2)]) ([A] B._[ren_ (0 .: (+2))])).
+ own_asimpl.
+ rewrite - ? /(And (_) (_)).
apply: (tac_rewrite (fun X => X) (gqm_andImpEquiv _ _ _)).
apply: gqm_mp; first by apply: gqm_swap.
apply: (tac_rewrite (fun X => _ ->> _ ->> X) (gqm_andCom _ _)).
@@ -51,4 +52,82 @@ Proof.
apply: gqm_mp; last by apply: H9.
apply: gqm_mp; first by apply: gqm_chain.
by apply: gqm_andI.
-Qed.
\ No newline at end of file
+Qed.
+
+Lemma lemma_A_8_2 : forall A B, |-- (|A| A & [E]B) <<->> [E](A.[ren (+1)] & B).
+Proof.
+ move => A B.
+ hSplit.
+ - (* (16) *)
+ apply: lemma_A_4_2.
+ have ->:((([E] (A.[ren (+1)] & B)).[ren (+1)]) = (([E] (A.[ren (+2)] & B.[ren (0.: (+2))])))) by rewrite /SquareExists /DiamondExists /All; own_asimpl.
+ rewrite -/(All _).
+ have -> :((|A| A).[ren (+1)] = (|A| A.[ren (+1)])) by rewrite /All; asimpl.
+ (* (15)*)
+ apply: gqm_mp.
+ + apply: gqm_mp; first by apply: (gqm_chain _ ([A] (A.[ren (+2)] & B.[ren (+1)]))).
+ (* (14) *)
+ have H:= (lemma_A_4_1 (A._[ren_ (+3)] & B._[ren_ (0 .: (+3))]) (Var 1)).
+ own_asimpl in H; rewrite - ? /(And (_) (_)) in H.
+ (* remove r->0 from the global naming context in H*)
+ have H' := (gqm_subst _ (ren_ (0 .: id)) H).
+ own_asimpl in H'.
+ rewrite - ? /(And (_) (_)) -/(DiamondExists _) in H'.
+ rewrite /SquareExists /All.
+ by own_asimpl.
+ + (* (13) *)
+ have -> :(([A] (A.[ren (+2)] & B.[ren (+1)])) = (|A|(A.[ren (+1)] & B))) by rewrite /All; own_asimpl.
+ by hAndDestruct (lemma_A_7_2_1 (A.[ren (+1)]) B).
+ - (* (17) *)
+ have H17 := gqm_andE1 (A._[ren_ (+1)]) B.
+ (* (18) *)
+ have {H17} H18 := lemma_A_5_1_2 _ _ H17.
+ (* (19) *)
+ have H19 := lemma_A_6_2_1 A.
+ (* (20) *)
+ have H20 := gqm_andE2 (A._[ren_ (+1)]) B.
+ (* (21) *)
+ have {H20} H21 := lemma_A_5_1_2 _ _ H20.
+ (* (22) *)
+ apply: gqm_mp; last by apply: H21.
+ apply: gqm_mp; first by apply: gqm_I2.
+ apply: gqm_mp; last by apply: H18.
+ apply: gqm_mp; first by apply: gqm_chain.
+ apply: gqm_mp; last by apply: H19.
+ apply: gqm_mp; first by apply: gqm_chain.
+ by apply: gqm_andI.
+Qed.
+
+Lemma lemma_A_8_3 : forall A B, |-- (|E| A ||| [A]B) <<->> [A](|E| A.[ren (+1)] ||| B).
+Proof.
+ move => A B.
+ hSplit.
+ - (* (23) *)
+ have H23 := gqm_orI1 (|E| A._[ren_ (+1)]) B.
+ (* (24) *)
+ have Hr :((|E| A.[ren (+1)]) = (|E| A).[ren (+1)]) by rewrite /Exists /All ; own_asimpl.
+ rewrite {1}Hr in H23 => {Hr}.
+ Fail have {H23} H24 := gqm_univgen _ _ H23.
+ (* TODO fix *)
+
+ Unshelve.
+ Focus 2.
+ (* (28) *)
+ have H28 := gqm_ADist (|A|-!(A._[ren_ (+1)])) B.
+ (* (29) *)
+ have H : (|-- (|A| -! A).[ren (+1)] ->> [A] -! A.[ren (+2)]) by own_asimpl; apply: gqm_id.
+ have {H} H29 := gqm_univgen (|A|-!A) (-!(A._[ren_ (+2)])) H.
+ have Hr : (([A] -! A.[ren (+2)]) = (|A| -! A.[ren (+1)])) by rewrite /All; own_asimpl.
+ rewrite Hr in H29 => {Hr}.
+ (* (30) *)
+ have {H28 H29} H30 : (|-- [A] (|A| -! A.[ren (+1)] ->> B) ->> |A| -! A ->> [A] B). {
+ apply: gqm_mp; first by apply: gqm_swap.
+ apply: gqm_mp; last by apply: H29.
+ apply: gqm_mp; first by apply: gqm_chain.
+ by apply: gqm_mp; first by apply: gqm_swap.
+ }
+ (* (31) *)
+ rewrite /Exists /Or.
+ apply: (tac_rewriteR (fun X => [A] (X ->> _) ->> _) (gqm_dnegEquiv _)).
+ by apply: (tac_rewriteR (fun X => [A] _ ->> (X ->> _)) (gqm_dnegEquiv _)).
+Admitted.
\ No newline at end of file