diff --git a/opam.pins b/opam.pins index fccfabe033c8f51c5b06fae4dbc010044107cf53..010e619e85ca18e00bb86757fe4302e85b2d3623 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 3f02ee64cc8b87d7b3f782735720a345b4ef12c2..eac3265ee6eb6ed35be8cbdf5b8db260a1706b73 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 7dfd5b92e87e9ca624fbce5e9b7254c71ff2f4c4..f9d36f3cd085c0164217ea0f9f82a902ecc0c15f 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 89df57d6bc9eb93ab43cf47c2cb4dd758fbb3f1a..9bb911c345090afec4f60cae462f6a1abdef6546 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.