introduce notation to provide "pres" existential witnesses by giving the...

introduce notation to provide "pres" existential witnesses by giving the missing proof. (This is a natural candidate for more ltac magic, to solve these obligations automatically... actually, why can't eauto do that?)

iris_core.v

@@ -188,9 +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.
-        assert (VALu:✓(s · u) ). { eapply ra_op_pos_valid. eassumption. }
-        assert (VALt:✓t ). { eapply ra_op_pos_valid2. eassumption. }
-        exists (ra_mk_pos (s · u) (VAL:=VALu)). exists (ra_mk_pos t (VAL:=VALt)).
+        exists✓ (s · u). { eapply ra_op_pos_valid. eassumption. }
+        exists✓ t. { eapply ra_op_pos_valid2. eassumption. }
         split; [|split].
         + rewrite <-Heq. reflexivity.
         + exists s. reflexivity.
@@ -401,13 +400,11 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
         apply HR; [reflexivity | assumption].
     Qed.
 
-    Lemma wsat_not_empty σ m (r: res) w k (HN : ~✓r) :
-      ~ wsat σ m r w (S k) tt.
+    Lemma wsat_not_empty σ m (r: res) w k :
+      wsat σ m r w (S k) tt -> ✓r.
     Proof.
       intros [rs [HD _] ]. destruct HD as [VAL _].
-      assert(VALr:✓r).
-      { eapply ra_op_valid; [now apply _|]. eassumption. }
-      congruence.
+      eapply ra_op_valid; [now apply _|]. eassumption.
     Qed.
 
   End WorldSatisfaction.

lib/ModuRes/BI.v

@@ -178,9 +178,9 @@ 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.
-    assert(VAL: ✓ (rd · ra_proj r11) ).
+    exists✓ (rd · ra_proj r11).
     { eapply ra_op_pos_valid; eassumption. }
-    exists (ra_cr_pos VAL) r12.
+    exists r12.
     split; [|split;[|assumption] ].
     - simpl. assumption.
     - eapply uni_pred, HP; [reflexivity|].
@@ -195,7 +195,7 @@ Section UPredBI.
     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_cr_pos VAL).
+    pose (rc := ra_mk_pos _ (VAL:=VAL)).
     eapply HSI with (r':=rc); [| etransitivity; eassumption |].
     - simpl. assumption. 
     - eapply uni_pred, HP; [reflexivity|]. exists r12. reflexivity.
@@ -369,17 +369,16 @@ 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.
-      assert(VAL: ✓ (ra_proj r1 · ra_proj r2) ).
+      exists✓ (ra_proj r1 · ra_proj r2).
       { eapply ra_op_pos_valid; eassumption. }
-      pose (r12 := ra_cr_pos VAL).
-      exists r12 r3; split; [assumption | split; [| assumption] ].
+      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.
-      assert(VAL: ✓ (ra_proj r2 · ra_proj r3) ).
+      exists r1.
+      exists✓ (ra_proj r2 · ra_proj r3).
       { eapply ra_op_pos_valid. rewrite comm. eassumption. }
-      pose (r23 := ra_cr_pos VAL).
-      exists r1 r23; split; [assumption | split; [assumption |] ].
+      split; [assumption | split; [assumption |] ].
       exists r2 r3; split; [reflexivity | split; assumption].
   Qed.
   Next Obligation.

lib/ModuRes/RA.v

@@ -33,10 +33,10 @@ Notation "1" := (ra_unit _) : ra_scope.
 Notation "p · q" := (ra_op _ p q) (at level 40, left associativity) : ra_scope.
 Notation "'✓' p" := (ra_valid p = true) (at level 35) : ra_scope.
 Notation "'~' '✓' p" := (ra_valid p <> true) (at level 35) : ra_scope.
+Delimit Scope ra_scope with ra.
 
 Tactic Notation "decide✓" ident(t1) "eqn:" ident(H) := destruct (ra_valid t1) eqn:H; [|apply not_true_iff_false in H].
 
-Delimit Scope ra_scope with ra.
 
 (* General RA lemmas *)
 Section RAs.
@@ -106,7 +106,6 @@ Section PositiveCarrier.
   Coercion ra_proj (t:ra_pos): T := proj1_sig t.
 
   Definition ra_mk_pos t {VAL: ✓ t}: ra_pos := exist _ t VAL.
-  Definition ra_cr_pos {t} (VAL: ✓ t) := ra_mk_pos t (VAL:=VAL).
 
   Program Definition ra_pos_unit: ra_pos := exist _ 1 _.
   Next Obligation.
@@ -128,6 +127,7 @@ Section PositiveCarrier.
 
 End PositiveCarrier.
 Global Arguments ra_pos T {_}.
+Tactic Notation "exists✓" constr(t) := let H := fresh "Hval" in assert(H:(✓t)%ra); [|exists (ra_mk_pos t (VAL:=H) ) ].
 
 
 Section Order.