From 61b66b335bafdc8333979ff1697d64794aa1382f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 8 Feb 2023 19:12:09 +0100
Subject: [PATCH] Tweak new proofs.

---
 iris_heap_lang/locations.v | 35 +++++++++++------------------------
 1 file changed, 11 insertions(+), 24 deletions(-)

diff --git a/iris_heap_lang/locations.v b/iris_heap_lang/locations.v
index 124b0c16d..92c562bb7 100644
--- a/iris_heap_lang/locations.v
+++ b/iris_heap_lang/locations.v
@@ -27,11 +27,9 @@ 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 le (l1 l2 : loc) : Prop := loc_car l1 ≤ loc_car l2.
 
-  Definition lt (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" :=
@@ -58,34 +56,23 @@ Module Loc.
   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.
+    - by intros ?.
+    - intros [x] [y] [z]; lia.
+    - intros [x] [y] ??; f_equal/=; lia.
   Qed.
 
   Global Instance le_total : Total le.
-  Proof.
-    rewrite /le. intros ? ?.
-    apply Z.le_total.
-  Qed.
+  Proof. rewrite /Total /le. lia. Qed.
 
   Lemma le_ngt l1 l2 : l1 ≤ₗ l2 ↔ ¬l2 <ₗ l1.
-  Proof.
-    rewrite /le /lt. intuition lia.
-  Qed.
+  Proof. apply Z.le_ngt. 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.
+  Proof. rewrite eq_spec. apply Z.le_lteq. Qed.
 
-  Lemma add_le l1 l2 i1 i2 : l1 ≤ₗ l2 → (i1 ≤ i2)%Z → l1 +ₗ i1 ≤ₗ l2 +ₗ i2.
-  Proof. rewrite /le /add. simpl. lia. Qed.
+  Lemma add_le_mono l1 l2 i1 i2 :
+    l1 ≤ₗ l2 → i1 ≤ i2 → l1 +ₗ i1 ≤ₗ l2 +ₗ i2.
+  Proof. apply Z.add_le_mono. Qed.
 
   Definition fresh (ls : gset loc) : loc :=
     {| loc_car := set_fold (λ k r, (1 + loc_car k) `max` r) 1 ls |}.
-- 
GitLab