changed ren_, subst_... to notation

theories/GQM.v

@@ -12,22 +12,22 @@ Instance Subst_form : Subst form. derive. Defined.
 Instance SubstLemmas_form : SubstLemmas form. derive. Qed.
 
 (* the implicit parameters cause trouble sometimes, because they cannot be infered in all contexts *)
-Definition subst_ := @subst _ Subst_form.
-Definition ren_ := @ren _ Ids_form.
-Definition up_ := @up _ Ids_form Rename_form.
-Definition ids_ := @ids _ Ids_form.
+Notation subst_ := (@subst _ Subst_form) (only parsing).
+Notation ren_ := (@ren _ Ids_form) (only parsing).
+Notation up_ := (@up _ Ids_form Rename_form) (only parsing).
+Notation ids_ := (@ids _ Ids_form) (only parsing).
 
 (* see https://github.com/uds-psl/autosubst/blob/1c3bb3bbf5477e3b33533a0fc090399f45fe3034/theories/Autosubst_Classes.v#L54 *)
 Notation "s ._[ sigma ]" := (subst_ sigma s)
   (at level 2, sigma at level 200, left associativity,
-   format "s ._[ sigma ]" ) : subst_scope.
+   format "s ._[ sigma ]", only parsing) : subst_scope.
 Notation "s ._[ t /]" := (subst_ (t .: ids_) s)
   (at level 2, t at level 200, left associativity,
-   format "s ._[ t /]") : subst_scope.
+   format "s ._[ t /]", only parsing) : subst_scope.
 Notation "s ._[ t1 , t2 , .. , tn /]" :=
   (subst_ (scons t1 (scons t2 .. (scons tn ids_) .. )) s)
   (at level 2, left associativity,
-format "s '[ ' ._[ t1 , '/' t2 , '/' .. , '/' tn /] ']'") : subst_scope.
+format "s '[ ' ._[ t1 , '/' t2 , '/' .. , '/' tn /] ']'", only parsing) : subst_scope.
 
 Notation "'[A]' B"   := (SquareAll B) (at level 74, right associativity).
 Notation "|[]| A"   := (Box A) (at level 74, right associativity).

theories/GQMDedSubst.v

@@ -13,7 +13,7 @@ Proof.
     rewrite (subst_end _ _ ids_).
     rewrite -Hmaxv.
     (* Set Printing All. *)
-    suff ->: ((switch_at O f ids_) = ids_) by [rewrite/ids_;asimpl].
+    suff ->: ((switch_at O f ids_) = ids_) by [asimpl].
     rewrite /switch_at.
     apply: functional_extensionality => n.
     suff ->: (n <? 0 = false) by [].
@@ -33,6 +33,4 @@ Proof.
     suff <-: (f 0 .: (fun k : var => f (S k)) = f) by [].
     apply: functional_extensionality => m.
     by case: m.
-Qed.
-
-(* Lemma gqm_free_ren : forall A f, free_in 0 A -> A  *)
\ No newline at end of file
+Qed.
\ No newline at end of file

theories/Section5.v

@@ -71,7 +71,6 @@ Proof.
   hSplit; first by apply: gqm_id.
   (* (1) *)
   have H1 := (gqm_Aglob (A._[ren_ (0 .: (+2))]) (Var 0)).
-  rewrite /subst_ /ren_ in H1.
   asimpl in H1.
   (* (2) *)
   have Hr : (([A] A.[ren (0 .: (+2))]) = ([A]A).[ren (+1)]) by asimpl.
@@ -80,7 +79,6 @@ Proof.
   asimpl in H2.
   (* (3) *)
   have H3 := (gqm_AE (A._[ren_ (+1)]) Bot).
-  rewrite /subst_ /ren_ in H3.
   asimpl in H3.
   (* (4) *)
   have H4 := (lemma_A_1 _ _ H3).
@@ -110,13 +108,11 @@ Proof.
   (* (2) is a noop as well*)
   (* (3) *)
   have H3 := (gqm_AE (-![A](A._[ren_ (+1)])) B).
-  rewrite /subst_ /ren_ in H3.
   (* (4) *)
   asimpl in H3.
   (* (5) *)
   (* ._[ren (0 .: (+2))] to express the fact, that the global r does not occur in phi^p_psi, because it is shadowed by the r in the binder *)
-  have H5 := (gqm_Aglob (A._[B/]._[ren (0 .: (+2))]) (Var 0)).
-  rewrite /subst_ /ren_ /ids_ in H5.
+  have H5 := (gqm_Aglob (A._[B/]._[ren_ (0 .: (+2))]) (Var 0)).
   (* 6 *)
   apply: gqm_mp; last by apply: H5.
   asimpl.
@@ -136,6 +132,7 @@ Proof.
   (* (2) *)
   have H2 : (|-- (X.[ren (+1)] & -! A.[ren (+1)]) ->> -![A](Phi.[ren (+1)])) by apply: gqm_mp; first by apply: gqm_contrapAndR.
   (* (3) *)
+  have H3 := (gqm_Q5 (Phi.[ren (+1)])).
   Fail have H3 : (|-- (X & -! A) ->> [A](-![A](Phi.[ren (+1)]))) by apply: gqm_univgen.
   (* TODO: fix *)
 Admitted.
@@ -175,13 +172,12 @@ Proof.
      * 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'.
+    rewrite /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'.
   }
   (* (4) *)
@@ -234,7 +230,6 @@ Proof.
   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.
@@ -273,7 +268,6 @@ Proof.
   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.
 
@@ -339,7 +333,6 @@ Lemma lemma_A_7_4 : forall A, |-- |A|A ->> A.
 Proof.
   move => A.
   have H := (gqm_AE (A._[ren_ (+1)]) (Var 0)).
-  rewrite /subst_ /ren_ in H.
   by asimpl in H.
 Qed.