Automate working with labels

Author: YaZko

theories/Eq/Sbisim.v

@@ -383,20 +383,13 @@ Section sbisim_heterogenous_theory.
         step in Sbisimu; apply Sbisimu in TR; destruct TR as (? & ? & TR & Sbis'' & EQl').
         do 2 eexists; repeat split; eauto.
         eapply INC; eauto.
-        (* todo ltac *)
-        apply Leq_eq in EQl.
-        rewrite flipL_Leq in EQl'.
-        apply Leq_eq in EQl'.
-        subst; auto.
+        now simpL.
       + step in Sbisimu; apply Sbisimu in TR; destruct TR as (? & ? & TR & Sbis & EQl).
         apply bwd in TR; destruct TR as (? & ? & TR & Sbis' & HL).
         step in Sbisimt; apply Sbisimt in TR; destruct TR as (? & ? & TR & Sbis'' & EQl').
         do 2 eexists; repeat split; eauto.
         eapply INC; eauto.
-        apply Leq_eq in EQl.
-        rewrite flipL_Leq in EQl'.
-        apply Leq_eq in EQl'.
-        subst; auto.
+        now simpL.
   Qed.
 
   #[global] Instance seq_chain_ctx {c : Chain (sb L)} :
@@ -458,20 +451,13 @@ Section sbisim_heterogenous_theory.
         step in Sbisimu; apply Sbisimu in TR; destruct TR as (? & ? & TR & Sbis'' & EQl').
         do 2 eexists; repeat split; eauto.
         eapply INC; eauto.
-        (* todo ltac *)
-        apply Leq_eq in EQl'.
-        rewrite flipL_Leq in EQl.
-        apply Leq_eq in EQl.
-        subst; auto.
+        now simpL.
       + step in Sbisimu; apply Sbisimu in TR; destruct TR as (? & ? & TR & Sbis & EQl).
         apply bwd in TR; destruct TR as (? & ? & TR & Sbis' & HL).
         step in Sbisimt; apply Sbisimt in TR; destruct TR as (? & ? & TR & Sbis'' & EQl').
         do 2 eexists; repeat split; eauto.
         eapply INC; eauto.
-        apply Leq_eq in EQl'.
-        rewrite flipL_Leq in EQl.
-        apply Leq_eq in EQl.
-        subst; auto.
+        now simpL.
   Qed.
 
   (*| Subrelations. |*)
@@ -1569,8 +1555,7 @@ Section SBisim_vs_SSim.
         playR in EQ'.
         ex2; split3; eauto.
         eapply IH; eauto.
-        rewrite flipL_Leq in H0.
-        apply Leq_eq in H,H0; subst; auto.
+        now simpL.
     Qed.
 
     #[global] Instance sbisim_ss_chain_ctx {c : Chain (ss L)} :
@@ -1588,8 +1573,7 @@ Section SBisim_vs_SSim.
         playL in EQ'.
         ex2; split3; eauto.
         eapply IH; eauto.
-        rewrite flipL_Leq in H.
-        apply Leq_eq in H,H0; subst; auto.
+        now simpL.
     Qed.
 
     #[global] Instance sbisim_ssim_goal :
@@ -1667,8 +1651,7 @@ Section Two_ss_is_not_sb.
         symmetry in H. apply H.
       - step. split; [apply H |].
         destruct H as [_ ?].
-        (* todo: this should be nicer *)
-        eapply lequiv_ss; [apply flipL_Leq |].
+        simpL.
         cbn; intros.
         apply H in H0 as (? & ? & ? & ? & ?); answer.
         symmetry; auto.

theories/Eq/Trans.v

@@ -2369,10 +2369,24 @@ Proof.
   all: dependent induction H; constructor.
 Qed.
 
+(* This one is a bit ugly: we will have proper instance to
+   lift [lequiv] arguments of (bi)simulations to [weq] result.
+   This instance does the last bit to allow the rewriting by [lequiv]
+   directly.
+ *)
+#[global] Instance weq_body {E B X}:
+  Proper (Coinduction.lattice.weq ==> eq ==> eq ==> eq ==> iff)
+    (@body (rel (S E B X) (S E B X)) _).
+Proof.
+  cbn; intros R L EQ ?? <- ?? <- ?? <-; split; intros H.
+  all:apply EQ; auto.
+Qed.
+
 Ltac simpL :=
   repeat match goal with
     | h : build_rel (flipL _) _ _ |- _ => rewrite flipL_Leq in h
     | h : build_rel Leq _ _ |- _ => apply Leq_eq in h
+    | |- context[flipL Leq] => rewrite flipL_Leq
     end; subst.
 
 (* (*| *)