Merge branch 'master' of git.fp.mpi-sws.org:nowbook

iris_core.v

@@ -191,8 +191,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) by auto_valid.
-        exists✓ t by auto_valid.
+        exists↓ (s · u) by auto_valid.
+        exists↓ t by auto_valid.
         split; [|split].
         + rewrite <-Heq. reflexivity.
         + exists s. reflexivity.
@@ -203,7 +203,7 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
         rewrite <-assoc, (comm _ u), assoc. reflexivity.
     Qed.
 
-    Lemma ownR_valid u (INVAL: ~✓u):
+    Lemma ownR_valid u (INVAL: ~↓u):
       ownR u ⊑ ⊥.
     Proof.
       intros w n [r VAL] [v Heq]. hnf. unfold ra_proj, proj1_sig in Heq.
@@ -346,7 +346,7 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
         rewrite-> !assoc, (comm (_ r2)); reflexivity.
     Qed.
 
-    Definition state_sat (r: res) σ: Prop := ✓r /\
+    Definition state_sat (r: res) σ: Prop := ↓r /\
       match fst r with
         | ex_own s => s = σ
         | _ => True
@@ -404,7 +404,7 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
     Qed.
 
     Lemma wsat_valid σ m (r: res) w k :
-      wsat σ m r w (S k) tt -> ✓r.
+      wsat σ m r w (S k) tt -> ↓r.
     Proof.
       intros [rs [HD _] ]. destruct HD as [VAL _].
       eapply ra_op_valid; [now apply _|]. eassumption.

iris_meta.v

@@ -135,7 +135,7 @@ Module IrisMeta (RL : RA_T) (C : CORE_LANG).
         wptp safe m w' (S k') tp' rs' (Q :: φs') /\ wsat σ' m (comp_list rs') w' @ S k'.
     Proof.
       destruct (steps_stepn _ _ HSN) as [n HSN']. clear HSN.
-      pose✓ r := (ex_own _ σ, 1:RL.res).
+      pose↓ r := (ex_own _ σ, 1:RL.res).
       { unfold ra_valid. simpl. eapply ra_valid_unit. now apply _. }
       edestruct (adequacy_ht (w:=fdEmpty) (k:=k') (r:=r) HT HSN') as [w' [rs' [φs' [HW [HSWTP HWS] ] ] ] ]; clear HT HSN'.
       - exists (ra_unit _); now rewrite ->ra_op_unit by apply _.

iris_unsafe.v

@@ -27,14 +27,6 @@ Module Unsafety (RL : RA_T) (C : CORE_LANG).
     by move=> /= ->.
   Qed.
 
-  (* PDS: masks.v *)
-  Lemma mask_full_disjoint m (HD : m # mask_full) :
-    meq m mask_emp.
-  Proof.
-    move=> i; move: {HD} (HD i) => HD; split; last done.
-    move=> Hm; exfalso; exact: HD.
-  Qed.
-
   Implicit Types (P : Props) (i n k : nat) (safe : bool) (m : mask) (e : expr) (Q : vPred) (r : pres) (w : Wld) (σ : state).
 
   (* PDS: Move to iris_wp.v *)
@@ -60,14 +52,7 @@ Module Unsafety (RL : RA_T) (C : CORE_LANG).
 
 	PDS: Should be moved or discarded.
   *)
-  Definition iffBI {T : Type} `{_ : ComplBI T} (p q : T) :=
-    (BI.and (BI.impl p q) (BI.impl q p)).
-
-  Notation "P ↔ Q" := (iffBI P Q) (at level 95, no associativity) : iris_scope.
-  Notation "p * q" := (BI.sc p q) (at level 40, left associativity) : iris_scope. (* RJ: there's already notation for this in iris_core? *)
-
-  (* RJ commented out for now, should not be necessary *)
-  (*Notation "a ⊑%pcm b" := ( _ a b) (at level 70, no associativity) : pcm_scope.*)
+  Notation "p * q" := (BI.sc p q) (at level 40, left associativity) : iris_scope. (* RJ: there's already notation for this in iris_core? *) (* PDS: The notation in Iris core uses sc : UPred (ra_pos res) -> UPred (ra_pos res) -> UPred (ra_pos res) rather than BI.sc. This variant is generic, so it survives more simplification. *)
 
   Lemma wpO {safe m e Q w r} : wp safe m e Q w O r.
   Proof.
@@ -76,13 +61,8 @@ Module Unsafety (RL : RA_T) (C : CORE_LANG).
     by exfalso; omega.
   Qed.
 
-  (* Easier to apply (with SSR, at least) than wsat_not_empty. *)
-  (* RJ: Commented out, does not have a multi-zero equivalent
-  Lemma wsat_nz {σ m w k} : ~ wsat σ m 0 w (S k) tt.
-  Proof. by move=> [rs [HD _] ]; exact: HD. Qed. *)
-
   (* Leibniz equality arise from SSR's case tactic.
-     RJ: I could use this ;-) move to CSetoid? *)
+     RJ: I could use this ;-) move to CSetoid? *) (* PDS: Feel free. I'd like to eventually get everything but the robust safety theorem out of this file. *)
   Lemma equivP {T : Type} `{eqT : Setoid T} {a b : T} : a = b -> a == b.
   Proof. by move=>->; reflexivity. Qed.
 
@@ -226,9 +206,9 @@ Module Unsafety (RL : RA_T) (C : CORE_LANG).
         move: {He HLe H1ei Hei} (He _ HSw' _ _ HLe H1ei Hei) => He.
         move: {HD} (mask_emp_disjoint (mask_full ∪ mask_full)) => HD.
         move: {He HSw' HW} (He _ _ _ _ _ HSw' HLt' HD HW) => [w'' [r' [HSw' [Hei' HW] ] ] ].
-        move: HW; rewrite assoc. move=>HW.
-        pose✓ α := (ra_proj r' · ra_proj rK).
-        { clear -HW. apply wsat_valid in HW. auto_valid. }
+        move: HW; rewrite assoc=>HW.
+        pose↓ α := (ra_proj r' · ra_proj rK).
+        + by apply wsat_valid in HW; auto_valid.
         have {HSw₀} HSw₀: w₀ ⊑ w'' by transitivity w'.
         exists w'' α; split; [done| split]; last first.
         + by move: HW; rewrite 2! mask_full_union => HW; wsatM HW.
@@ -244,9 +224,9 @@ Module Unsafety (RL : RA_T) (C : CORE_LANG).
       move: {He HLe H1ei Hei} (He _ HSw' _ _ HLe H1ei Hei) => He.
       (* unroll wp(ei,E)—step case—to get wp(ei',E) *)
       move: He; rewrite {1}unfold_wp => He.
-      move: {HD} (mask_emp_disjoint (mask_full)) => HD.
+      move: {HD} (mask_emp_disjoint mask_full) => HD.
       move: {He HSw' HLt' HW} (He _ _ _ _ _ HSw' HLt' HD HW) => [_ [HS _] ].
-      have Hεei: ei = ε[[ei]] by move: (fill_empty ei)->.
+      have Hεei: ei = ε[[ei]] by rewrite fill_empty.
       move: {HS Hεei HStep} (HS _ _ _ _ Hεei HStep) => [w'' [r' [HSw' [He' HW] ] ] ].
       (* unroll wp(ei',E)—value case—to get E ei' *)
       move: He'; rewrite {1}unfold_wp => He'.
@@ -258,9 +238,9 @@ Module Unsafety (RL : RA_T) (C : CORE_LANG).
       move: HV; rewrite -(fill_empty ei') => HV.
       move: {Hv} (Hv HV) => [w''' [rei' [HSw'' [Hei' HW] ] ] ].
       (* now IH *)
-      move: HW; rewrite assoc. move=>HW.
-      pose✓ α := (ra_proj rei' · ra_proj rK).
-      { clear -HW. apply wsat_valid in HW. auto_valid. }
+      move: HW; rewrite assoc => HW.
+      pose↓ α := (ra_proj rei' · ra_proj rK).
+      + by apply wsat_valid in HW; auto_valid.
       exists w''' α. split; first by transitivity w''.
       split; last by rewrite mask_full_union -(mask_full_union mask_emp).
       rewrite/= in Hei'; rewrite fill_empty -Hk' in Hei' * => {Hk'}.

iris_vs.v

@@ -29,7 +29,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
       - eapply wsat_equiv, HE; try reflexivity.
         rewrite ->assoc, (comm (_ r1)), HR; reflexivity.
       - rewrite ->assoc, (comm (_ r1')) in HE'.
-        exists w2. exists✓ (rd · ra_proj r1').
+        exists w2. exists↓ (rd · ra_proj r1').
         { apply wsat_valid in HE'. auto_valid. }
         split; [assumption | split; [| assumption] ].
         eapply uni_pred, HP'; [reflexivity|]. exists rd. reflexivity.
@@ -110,7 +110,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
       - rewrite ->comp_map_remove with (i := i) (r := ri) in HE by (rewrite HLr; reflexivity).
         rewrite ->assoc, <- (assoc (_ r)), (comm rf), assoc in HE.
         exists w'.
-        exists✓ (ra_proj r · ra_proj ri). { destruct HE as [HE _]. eapply ra_op_valid, ra_op_valid; eauto with typeclass_instances. }
+        exists↓ (ra_proj r · ra_proj ri). { destruct HE as [HE _]. eapply ra_op_valid, ra_op_valid; eauto with typeclass_instances. }
         split; [reflexivity |].
         split.
         + simpl; eapply HInv; [now auto with arith |].
@@ -145,7 +145,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
       exists w' ra_pos_unit; split; [reflexivity | split; [exact I |] ].
       rewrite ->(comm (_ r)), <-assoc in HE.
       remember (match rs i with Some ri => ri | None => ra_pos_unit end) as ri eqn: EQri.
-      pose✓ rri := (ra_proj ri · ra_proj r).
+      pose↓ rri := (ra_proj ri · ra_proj r).
       { destruct (rs i) as [rsi |] eqn: EQrsi; subst;
         [| simpl; rewrite ->ra_op_unit by apply _; now apply ra_pos_valid].
         clear - HE EQrsi. destruct HE as [HE _].
@@ -222,7 +222,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
       - rewrite ->assoc, HR; eapply wsat_equiv, HE; try reflexivity; [].
         clear; intros i; unfold mcup; tauto.
       - rewrite ->assoc in HEq.
-        exists w''. exists✓ (ra_proj rq · ra_proj rr).
+        exists w''. exists↓ (ra_proj rq · ra_proj rr).
         { apply wsat_valid in HEq. auto_valid. }
         split; [assumption | split].
         + unfold lt in HLe0; rewrite ->HSub, HSub', <- HLe0 in Hr; exists rq rr.
@@ -241,7 +241,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
       ownL <M< inclM.
 
     Lemma vsGhostUpd m rl (P : RL.res -> Prop)
-          (HU : forall rf (HD : ✓(rl · rf)), exists sl, P sl /\ ✓(sl · rf)) :
+          (HU : forall rf (HD : ↓(rl · rf)), exists sl, P sl /\ ↓(sl · rf)) :
       valid (vs m m (ownL rl) (xist (ownLP P))).
     Proof.
       unfold ownLP; intros _ _ _ w _ n [ [rp' rl'] Hrval] _ _ HG w'; intros.
@@ -251,7 +251,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
       - clear - Hval EQrl. eapply ra_prod_valid2 in Hval. destruct Hval as [_ Hsnd].
         rewrite ->assoc, (comm rl), EQrl.
         rewrite ra_op_prod_snd in Hsnd. exact Hsnd.
-      - exists w'. exists✓ (rp', rsl).
+      - exists w'. exists↓ (rp', rsl).
         { clear - Hval HCrsl.
           apply ra_prod_valid. split; [|auto_valid].
           eapply ra_prod_valid2 in Hval. destruct Hval as [Hfst _].

iris_wp.v

@@ -60,21 +60,21 @@ Module IrisWP (RL : RA_T) (C : CORE_LANG).
       split; [clear HS HF | split; [clear HV HF | split; clear HV HS; [| clear HF ] ] ]; intros.
       - specialize (HV HV0); destruct HV as [w'' [r1' [HSw' [Hφ HE'] ] ] ].
         rewrite ->assoc, (comm (_ r1')) in HE'.
-        exists w''. exists✓ (rd · ra_proj r1').
+        exists w''. exists↓ (rd · ra_proj r1').
         { clear -HE'. apply wsat_valid in HE'. auto_valid. }
         split; [assumption | split; [| assumption] ].
         eapply uni_pred, Hφ; [| exists rd]; reflexivity.
       - specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r1' [HSw' [HWP HE'] ] ] ].
         rewrite ->assoc, (comm (_ r1')) in HE'. exists w''.
         destruct k as [| k]; [exists r1'; simpl wsat; tauto |].
-        exists✓ (rd · ra_proj r1').
+        exists↓ (rd · ra_proj r1').
         { clear- HE'. apply wsat_valid in HE'. auto_valid. }
         split; [assumption | split; [| assumption] ].
         eapply uni_pred, HWP; [| exists rd]; reflexivity.
       - specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret1 [HSw' [HWR [HWF HE'] ] ] ] ] ].
         destruct k as [| k]; [exists w'' rfk rret1; simpl wsat; tauto |].
         rewrite ->assoc, <- (assoc (_ rfk)) in HE'.
-        exists w''. exists rfk. exists✓ (rd · ra_proj rret1).
+        exists w''. exists rfk. exists↓ (rd · ra_proj rret1).
         { clear- HE'. apply wsat_valid in HE'. rewrite comm. eapply ra_op_valid, ra_op_valid; try now apply _.
           rewrite ->(comm (_ rfk)) in HE'. eassumption. }
         repeat (split; try assumption).
@@ -448,14 +448,14 @@ Module IrisWP (RL : RA_T) (C : CORE_LANG).
       clear He; split; [intros HVal; clear HS HF IH HE | split; [clear HV HF HE | clear HV HS HE; split; [clear HS' | clear HF] ]; intros ].
       - specialize (HV HVal); destruct HV as [w'' [r1' [HSw' [Hφ HE] ] ] ].
         rewrite ->assoc in HE. exists w''.
-        exists✓ (ra_proj r1' · ra_proj r2).
+        exists↓ (ra_proj r1' · ra_proj r2).
         { apply wsat_valid in HE. auto_valid. }
         split; [eassumption | split; [| eassumption ] ].
         exists r1' r2; split; [reflexivity | split; [assumption |] ].
         unfold lt in HLt; rewrite ->HLt, <- HSw', <- HSw; apply HLR.
       - edestruct HS as [w'' [r1' [HSw' [He HE] ] ] ]; try eassumption; []; clear HS.
         destruct k as [| k]; [exists w' r1'; split; [reflexivity | split; [apply wpO | exact I] ] |].
-        rewrite ->assoc in HE. exists w''. exists✓ (ra_proj r1' · ra_proj r2).
+        rewrite ->assoc in HE. exists w''. exists↓ (ra_proj r1' · ra_proj r2).
         { apply wsat_valid in HE. auto_valid. }
         split; [eassumption | split; [| eassumption] ].
         eapply IH; try eassumption; [ reflexivity |].
@@ -463,7 +463,7 @@ Module IrisWP (RL : RA_T) (C : CORE_LANG).
       - specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [HSw' [HWF [HWR HE] ] ] ] ] ].
         destruct k as [| k]; [exists w' rfk rret; split; [reflexivity | split; [apply wpO | split; [apply wpO | exact I] ] ] |].
         rewrite ->assoc, <- (assoc (_ rfk)) in HE.
-        exists w''. exists rfk. exists✓ (ra_proj rret · ra_proj r2).
+        exists w''. exists rfk. exists↓ (ra_proj rret · ra_proj r2).
         { clear- HE. apply wsat_valid in HE. eapply ra_op_valid2, ra_op_valid; try now apply _. eassumption. }
         split; [eassumption | split; [| split; eassumption] ].
         eapply IH; try eassumption; [ reflexivity |].
@@ -488,7 +488,7 @@ Module IrisWP (RL : RA_T) (C : CORE_LANG).
         edestruct He as [_ [HeS _] ]; try eassumption; [].
         edestruct HeS as [w'' [r1' [HSw' [He' HE'] ] ] ]; try eassumption; [].
         clear HE He HeS; rewrite ->assoc in HE'.
-        exists w''. exists✓ (ra_proj r1' · ra_proj r2).
+        exists w''. exists↓ (ra_proj r1' · ra_proj r2).
         { clear- HE'. apply wsat_valid in HE'. auto_valid. }
         split; [eassumption | split; [| eassumption] ].
         assert (HNV : ~ is_value ei)
@@ -503,7 +503,7 @@ Module IrisWP (RL : RA_T) (C : CORE_LANG).
           edestruct He' as [HVal _]; try eassumption; [].
           specialize (HVal HV); destruct HVal as [w'' [r1'' [HSw' [Hφ HE'] ] ] ].
           rewrite ->assoc in HE'.
-          exists w''. exists✓ (ra_proj r1'' · ra_proj r2).
+          exists w''. exists↓ (ra_proj r1'' · ra_proj r2).
           { clear- HE'. apply wsat_valid in HE'. auto_valid. }
           split; [eassumption | split; [| eassumption] ].
           exists r1'' r2; split; [reflexivity | split; [assumption |] ].

lib/ModuRes/BI.v

@@ -178,7 +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) by auto_valid.
+    exists↓ (rd · ra_proj r11) by auto_valid.
     exists r12.
     split; [|split;[|assumption] ].
     - simpl. assumption.
@@ -192,7 +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'.
-    pose✓ rc := (r12 · ra_proj r) by auto_valid.
+    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.
@@ -366,13 +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) by auto_valid.
+      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) by auto_valid.
+      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

@@ -32,11 +32,11 @@ Arguments ra_valid {T} {_} t.
 
 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.
+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) "as" ident(H) := destruct (ra_valid t1) eqn:H; [|apply not_true_iff_false in H].
+Tactic Notation "decide↓" ident(t1) "as" ident(H) := destruct (ra_valid t1) eqn:H; [|apply not_true_iff_false in H].
 
 
 (* General RA lemmas *)
@@ -49,19 +49,19 @@ Section RAs.
     rewrite comm. now eapply ra_op_unit.
   Qed.
   
-  Lemma ra_op_valid2 t1 t2: ✓ (t1 · t2) -> ✓ t2.
+  Lemma ra_op_valid2 t1 t2: ↓ (t1 · t2) -> ↓ t2.
   Proof.
     rewrite comm. now eapply ra_op_valid.
   Qed.
 
-  Lemma ra_op_invalid t1 t2: ~✓t1 -> ~✓(t1 · t2).
+  Lemma ra_op_invalid t1 t2: ~↓t1 -> ~↓(t1 · t2).
   Proof.
     intros Hinval Hval.
     apply Hinval.
     eapply ra_op_valid; now eauto.
   Qed.
 
-  Lemma ra_op_invalid2 t1 t2: ~✓t2 -> ~✓(t1 · t2).
+  Lemma ra_op_invalid2 t1 t2: ~↓t2 -> ~↓(t1 · t2).
   Proof.
     rewrite comm. now eapply ra_op_invalid.
   Qed.
@@ -115,7 +115,7 @@ Section ProductLemmas.
   Qed.
 
   Lemma ra_prod_valid (s: S) (t: T):
-    ✓(s, t) <-> ✓s /\ ✓t.
+    ↓(s, t) <-> ↓s /\ ↓t.
   Proof.
     unfold ra_valid, ra_valid_prod.
     rewrite andb_true_iff.
@@ -123,7 +123,7 @@ Section ProductLemmas.
   Qed.
 
   Lemma ra_prod_valid2 (st: S*T):
-    ✓st <-> ✓(fst st) /\ ✓(snd st).
+    ↓st <-> ↓(fst st) /\ ↓(snd st).
   Proof.
     destruct st as [s t]. unfold ra_valid, ra_valid_prod.
     rewrite andb_true_iff.
@@ -136,37 +136,37 @@ Section PositiveCarrier.
   Context {T} `{raT : RA T}.
   Local Open Scope ra_scope.
 
-  Definition ra_pos: Type := { r | ✓ r }.
+  Definition ra_pos: Type := { r | ↓ r }.
   Coercion ra_proj (t:ra_pos): T := proj1_sig t.
 
-  Definition ra_mk_pos t {VAL: ✓ t}: ra_pos := exist _ t VAL.
+  Definition ra_mk_pos t {VAL: ↓ t}: ra_pos := exist _ t VAL.
 
   Program Definition ra_pos_unit: ra_pos := exist _ 1 _.
   Next Obligation.
     now erewrite ra_valid_unit by apply _.
   Qed.
 
-  Lemma ra_proj_cancel r (VAL: ✓r):
+  Lemma ra_proj_cancel r (VAL: ↓r):
     ra_proj (ra_mk_pos r (VAL:=VAL)) = r.
   Proof.
     reflexivity.
   Qed.
 
   Lemma ra_op_pos_valid t1 t2 t:
-    t1 · t2 == ra_proj t -> ✓ t1.
+    t1 · t2 == ra_proj t -> ↓ t1.
   Proof.
     destruct t as [t Hval]; simpl. intros Heq. rewrite <-Heq in Hval.
     eapply ra_op_valid; eassumption.
   Qed.
 
   Lemma ra_op_pos_valid2 t1 t2 t:
-    t1 · t2 == ra_proj t -> ✓ t2.
+    t1 · t2 == ra_proj t -> ↓ t2.
   Proof.
     rewrite comm. now eapply ra_op_pos_valid.
   Qed.
 
   Lemma ra_pos_valid (r : ra_pos):
-    ✓(ra_proj r).
+    ↓(ra_proj r).
   Proof.
     destruct r as [r VAL].
     exact VAL.
@@ -186,10 +186,10 @@ Ltac auto_valid := match goal with
                    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) ) ].
+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.