provie some automation for establishing validity

iris_core.v

@@ -9,7 +9,7 @@ Module IrisRes (RL : RA_T) (C : CORE_LANG) <: RA_T.
   Instance res_op   : RA_op res := _.
   Instance res_unit : RA_unit res := _.
   Instance res_valid: RA_valid res := _.
-  Instance res_ra  : RA res := _.
+  Instance res_ra   : RA res := _.
 
   (* The order on (ra_pos res) is inferred correctly, but this one is not *)
   Instance res_pord: preoType res := ra_preo res.
@@ -188,8 +188,8 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
     Proof.
       intros w n r; split; [intros Hut | intros [r1 [r2 [EQr [Hu Ht] ] ] ] ].
       - destruct Hut as [s Heq]. rewrite assoc in Heq.
-        exists✓ (s · u). { eapply ra_op_pos_valid. eassumption. }
-        exists✓ t. { eapply ra_op_pos_valid2. eassumption. }
+        exists✓ (s · u) by auto_valid.
+        exists✓ t by auto_valid.
         split; [|split].
         + rewrite <-Heq. reflexivity.
         + exists s. reflexivity.

lib/ModuRes/BI.v

@@ -170,7 +170,7 @@ Section UPredBI.
     intros n m r1 r2 HLe HSub HImp k r3 HLe' HSub' HP.
     apply HImp; try (etransitivity; eassumption); assumption.
   Qed.
-
+  
   (* BI connectives. *)
   Global Program Instance sc_up : scBI (UPred pres) :=
     fun P Q =>
@@ -178,8 +178,7 @@ Section UPredBI.
   Next Obligation.
     intros n m r1 r2 HLe [rd HEq] [r11 [r12 [HEq' [HP HQ]]]].
     rewrite <- HEq', assoc in HEq; setoid_rewrite HLe.
-    exists✓ (rd · ra_proj r11).
-    { eapply ra_op_pos_valid; eassumption. }
+    exists✓ (rd · ra_proj r11) by auto_valid.
     exists r12.
     split; [|split;[|assumption] ].
     - simpl. assumption.
@@ -193,9 +192,7 @@ Section UPredBI.
   Next Obligation.
     intros n m r1 r2 HLe [r12 HEq] HSI k r rr HEq' HSub HP.
     rewrite comm in HEq; rewrite <- HEq, <- assoc in HEq'.
-    assert (VAL: ✓ (r12 · ra_proj r) ).
-    { eapply ra_op_pos_valid. erewrite comm. eassumption. }
-    pose (rc := ra_mk_pos _ (VAL:=VAL)).
+    pose✓ rc := (r12 · ra_proj r) by auto_valid.
     eapply HSI with (r':=rc); [| etransitivity; eassumption |].
     - simpl. assumption. 
     - eapply uni_pred, HP; [reflexivity|]. exists r12. reflexivity.
@@ -369,15 +366,13 @@ Section UPredBI.
     intros P Q R n r; split.
     - intros [r1 [rr [EQr [HP [r2 [r3 [EQrr [HQ HR]]]]]]]].
       rewrite <- EQrr, assoc in EQr. unfold sc.
-      exists✓ (ra_proj r1 · ra_proj r2).
-      { eapply ra_op_pos_valid; eassumption. }
+      exists✓ (ra_proj r1 · ra_proj r2) by auto_valid.
       exists r3; split; [assumption | split; [| assumption] ].
       exists r1 r2; split; [reflexivity | split; assumption].
     - intros [rr [r3 [EQr [[r1 [r2 [EQrr [HP HQ]]]] HR]]]].
       rewrite <- EQrr, <- assoc in EQr; clear EQrr.
       exists r1.
-      exists✓ (ra_proj r2 · ra_proj r3).
-      { eapply ra_op_pos_valid. rewrite comm. eassumption. }
+      exists✓ (ra_proj r2 · ra_proj r3) by auto_valid.
       split; [assumption | split; [assumption |] ].
       exists r2 r3; split; [reflexivity | split; assumption].
   Qed.

lib/ModuRes/RA.v

@@ -127,7 +127,22 @@ Section PositiveCarrier.
 
 End PositiveCarrier.
 Global Arguments ra_pos T {_}.
+
+(** Validity automation tactics *)
+Ltac auto_valid_inner :=
+  solve [ eapply ra_op_pos_valid; (eassumption || rewrite comm; eassumption)
+        | eapply ra_op_pos_valid2; (eassumption || rewrite comm; eassumption)
+        | eapply ra_op_valid; (eassumption || rewrite comm; eassumption) ].
+Ltac auto_valid := match goal with
+                     | |- @ra_valid ?T _ _ = true =>
+                       let H := fresh in assert (H : RA T) by apply _; auto_valid_inner
+                   end.
+
+(* FIXME put the common parts into a helper tactic, and allow arbitrary tactics after "by" *)
 Tactic Notation "exists✓" constr(t) := let H := fresh "Hval" in assert(H:(✓t)%ra); [|exists (ra_mk_pos t (VAL:=H) ) ].
+Tactic Notation "exists✓" constr(t) "by" "auto_valid" := let H := fresh "Hval" in assert(H:(✓t)%ra); [auto_valid|exists (ra_mk_pos t (VAL:=H) ) ].
+Tactic Notation "pose✓" ident(name) ":=" constr(t) := let H := fresh "Hval" in assert(H:(✓t)%ra); [|pose (name := ra_mk_pos t (VAL:=H) ) ].
+Tactic Notation "pose✓" ident(name) ":=" constr(t) "by" "auto_valid" := let H := fresh "Hval" in assert(H:(✓t)%ra); [auto_valid|pose (name := ra_mk_pos t (VAL:=H) ) ].
 
 
 Section Order.