Define order predicates on locations.

iris_heap_lang/lang.v

@@ -560,8 +560,8 @@ Definition bin_op_eval_bool (op : bin_op) (b1 b2 : bool) : option base_lit :=
 Definition bin_op_eval_loc (op : bin_op) (l1 : loc) (v2 : base_lit) : option base_lit :=
   match op, v2 with
   | OffsetOp, LitInt off => Some $ LitLoc (l1 +ₗ off)
-  | LeOp, LitLoc l2 => Some $ LitBool (bool_decide (loc_car l1 ≤ loc_car l2)%Z)
-  | LtOp, LitLoc l2 => Some $ LitBool (bool_decide (loc_car l1 < loc_car l2)%Z)
+  | LeOp, LitLoc l2 => Some $ LitBool (bool_decide (l1 ≤ₗ l2))
+  | LtOp, LitLoc l2 => Some $ LitBool (bool_decide (l1 <ₗ l2))
   | _, _ => None
   end.
 

iris_heap_lang/locations.v

@@ -27,9 +27,17 @@ Module Loc.
   Definition add (l : loc) (off : Z) : loc :=
     {| loc_car := loc_car l + off|}.
 
+  Definition le (l1 l2 : loc) : Prop :=
+    loc_car l1 ≤ loc_car l2.
+
+  Definition lt (l1 l2 : loc) : Prop :=
+    loc_car l1 < loc_car l2.
+
   Module Import notations.
     Notation "l +ₗ off" :=
       (add l off) (at level 50, left associativity) : stdpp_scope.
+    Notation "l1 ≤ₗ l2" := (le l1 l2) (at level 70) : stdpp_scope.
+    Notation "l1 <ₗ l2" := (lt l1 l2) (at level 70) : stdpp_scope.
   End notations.
 
   Lemma add_assoc l i j : l +ₗ i +ₗ j = l +ₗ (i + j).
@@ -41,6 +49,44 @@ Module Loc.
   Global Instance add_inj l : Inj eq eq (add l).
   Proof. intros x1 x2. rewrite eq_spec /=. lia. Qed.
 
+  Global Instance le_dec l1 l2 : Decision (l1 ≤ₗ l2).
+  Proof. rewrite /le. apply _. Qed.
+
+  Global Instance lt_dec l1 l2 : Decision (l1 <ₗ l2).
+  Proof. rewrite /lt. apply _. Qed.
+
+  Global Instance le_po : PartialOrder le.
+  Proof.
+    rewrite /le. split; [split|].
+    - intros ?. reflexivity.
+    - intros ? ? ?. apply PreOrder_Transitive.
+    - intros [x] [y]. simpl. intros xy yx.
+      assert (x = y) by lia. congruence.
+  Qed.
+
+  Global Instance le_total : Total le.
+  Proof.
+    rewrite /le. intros ? ?.
+    apply Z.le_total.
+  Qed.
+
+  Lemma le_ngt l1 l2 : l1 ≤ₗ l2 ↔ ¬l2 <ₗ l1.
+  Proof.
+    rewrite /le /lt. intuition lia.
+  Qed.
+
+  Lemma le_lteq l1 l2 : l1 ≤ₗ l2 ↔ l1 <ₗ l2 ∨ l1 = l2.
+  Proof.
+    rewrite /le /lt. destruct l1 as [x], l2 as [y]. simpl.
+    intuition.
+    - assert (x < y ∨ x = y)%Z by lia. intuition congruence.
+    - lia.
+    - assert (x = y) by congruence. lia.
+  Qed.
+
+  Lemma add_le l1 l2 i1 i2 : l1 ≤ₗ l2 → (i1 ≤ i2)%Z → l1 +ₗ i1 ≤ₗ l2 +ₗ i2.
+  Proof. rewrite /le /add. simpl. lia. Qed.
+
   Definition fresh (ls : gset loc) : loc :=
     {| loc_car := set_fold (λ k r, (1 + loc_car k) `max` r) 1 ls |}.