From c75aa8f4f3e681cd499cc4b8b66fee2f42e39993 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 11 Mar 2017 10:54:48 +0100
Subject: [PATCH] Update to latest stdpp.

---
 opam.pins               |  2 +-
 theories/algebra/cmra.v | 12 ++----------
 theories/algebra/frac.v | 12 +-----------
 theories/algebra/ofe.v  |  4 ++--
 4 files changed, 6 insertions(+), 24 deletions(-)

diff --git a/opam.pins b/opam.pins
index fccfabe03..010e619e8 100644
--- a/opam.pins
+++ b/opam.pins
@@ -1 +1 @@
-coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 5061c3cbfe8954faa67dc5eed061c92eaca65308
+coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 09e255a930646d8a2b4302b82137356cf37681f3
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index 3f02ee64c..eac3265ee 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -965,11 +965,7 @@ Section nat.
   Instance nat_op : Op nat := plus.
   Definition nat_op_plus x y : x â‹… y = x + y := eq_refl.
   Lemma nat_included (x y : nat) : x ≼ y ↔ x ≤ y.
-  Proof.
-    split.
-    - intros [z ->]; unfold op, nat_op; lia.
-    - exists (y - x). by apply le_plus_minus.
-  Qed.
+  Proof. by rewrite nat_le_sum. Qed.
   Lemma nat_ra_mixin : RAMixin nat.
   Proof.
     apply ra_total_mixin; try by eauto.
@@ -1037,11 +1033,7 @@ Section positive.
   Instance pos_op : Op positive := Pos.add.
   Definition pos_op_plus x y : x â‹… y = (x + y)%positive := eq_refl.
   Lemma pos_included (x y : positive) : x ≼ y ↔ (x < y)%positive.
-  Proof.
-    split.
-    - intros [z ->]; unfold op, pos_op. lia.
-    - exists (y - x)%positive. symmetry. apply Pplus_minus. lia.
-  Qed.
+  Proof. by rewrite Plt_sum. Qed.
   Lemma pos_ra_mixin : RAMixin positive.
   Proof.
     split; try by eauto.
diff --git a/theories/algebra/frac.v b/theories/algebra/frac.v
index 7dfd5b92e..f9d36f3cd 100644
--- a/theories/algebra/frac.v
+++ b/theories/algebra/frac.v
@@ -11,18 +11,8 @@ Instance frac_valid : Valid frac := λ x, (x ≤ 1)%Qc.
 Instance frac_pcore : PCore frac := λ _, None.
 Instance frac_op : Op frac := λ x y, (x + y)%Qp.
 
-(* TODO: Find better place for this lemma. *)
-Lemma Qp_le_sum (x y : Qp) : (x < y)%Qc ↔ (∃ z, y = x + z)%Qp.
-Proof.
-  split.
-  - intros Hlt%Qclt_minus_iff. exists (mk_Qp (y - x) Hlt). apply Qp_eq; simpl.
-    by rewrite (Qcplus_comm y) Qcplus_assoc Qcplus_opp_r Qcplus_0_l.
-  - intros [z ->%leibniz_equiv]; simpl.
-    rewrite -{1}(Qcplus_0_r x). apply Qcplus_lt_mono_l, Qp_prf.
-Qed.
-
 Lemma frac_included (x y : frac) : x ≼ y ↔ (x < y)%Qc.
-Proof. symmetry. exact: Qp_le_sum. Qed.
+Proof. by rewrite Qp_lt_sum. Qed.
 
 Corollary frac_included_weak (x y : frac) : x ≼ y → (x ≤ y)%Qc.
 Proof. intros ?%frac_included. auto using Qclt_le_weak. Qed.
diff --git a/theories/algebra/ofe.v b/theories/algebra/ofe.v
index 89df57d6b..9bb911c34 100644
--- a/theories/algebra/ofe.v
+++ b/theories/algebra/ofe.v
@@ -346,7 +346,7 @@ Section fixpoint.
     { apply equiv_dist=>n. rewrite /fp2 (conv_compl n) /= /chcar.
       induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S. }
     rewrite -(fixpoint_unique fp2) //.
-    apply Hlim=> n /=. by apply nat_iter_ind.
+    apply Hlim=> n /=. by apply Nat_iter_ind.
   Qed.
 End fixpoint.
 
@@ -419,7 +419,7 @@ Section fixpointK.
     P (fixpointK k f).
   Proof.
     intros. rewrite /fixpointK. apply fixpoint_ind; eauto.
-    intros; apply nat_iter_ind; auto.
+    intros; apply Nat_iter_ind; auto.
   Qed.
 End fixpointK.
 
-- 
GitLab