Commit c75aa8f4 authored by Robbert Krebbers's avatar Robbert Krebbers

Update to latest stdpp.

parent e772028a
coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 5061c3cbfe8954faa67dc5eed061c92eaca65308 coq-stdpp https://gitlab.mpi-sws.org/robbertkrebbers/coq-stdpp 09e255a930646d8a2b4302b82137356cf37681f3
...@@ -965,11 +965,7 @@ Section nat. ...@@ -965,11 +965,7 @@ Section nat.
Instance nat_op : Op nat := plus. Instance nat_op : Op nat := plus.
Definition nat_op_plus x y : x y = x + y := eq_refl. Definition nat_op_plus x y : x y = x + y := eq_refl.
Lemma nat_included (x y : nat) : x y x y. Lemma nat_included (x y : nat) : x y x y.
Proof. Proof. by rewrite nat_le_sum. Qed.
split.
- intros [z ->]; unfold op, nat_op; lia.
- exists (y - x). by apply le_plus_minus.
Qed.
Lemma nat_ra_mixin : RAMixin nat. Lemma nat_ra_mixin : RAMixin nat.
Proof. Proof.
apply ra_total_mixin; try by eauto. apply ra_total_mixin; try by eauto.
...@@ -1037,11 +1033,7 @@ Section positive. ...@@ -1037,11 +1033,7 @@ Section positive.
Instance pos_op : Op positive := Pos.add. Instance pos_op : Op positive := Pos.add.
Definition pos_op_plus x y : x y = (x + y)%positive := eq_refl. Definition pos_op_plus x y : x y = (x + y)%positive := eq_refl.
Lemma pos_included (x y : positive) : x y (x < y)%positive. Lemma pos_included (x y : positive) : x y (x < y)%positive.
Proof. Proof. by rewrite Plt_sum. Qed.
split.
- intros [z ->]; unfold op, pos_op. lia.
- exists (y - x)%positive. symmetry. apply Pplus_minus. lia.
Qed.
Lemma pos_ra_mixin : RAMixin positive. Lemma pos_ra_mixin : RAMixin positive.
Proof. Proof.
split; try by eauto. split; try by eauto.
......
...@@ -11,18 +11,8 @@ Instance frac_valid : Valid frac := λ x, (x ≤ 1)%Qc. ...@@ -11,18 +11,8 @@ Instance frac_valid : Valid frac := λ x, (x ≤ 1)%Qc.
Instance frac_pcore : PCore frac := λ _, None. Instance frac_pcore : PCore frac := λ _, None.
Instance frac_op : Op frac := λ x y, (x + y)%Qp. 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. 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. Corollary frac_included_weak (x y : frac) : x y (x y)%Qc.
Proof. intros ?%frac_included. auto using Qclt_le_weak. Qed. Proof. intros ?%frac_included. auto using Qclt_le_weak. Qed.
......
...@@ -346,7 +346,7 @@ Section fixpoint. ...@@ -346,7 +346,7 @@ Section fixpoint.
{ apply equiv_dist=>n. rewrite /fp2 (conv_compl n) /= /chcar. { apply equiv_dist=>n. rewrite /fp2 (conv_compl n) /= /chcar.
induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S. } induction n as [|n IH]; simpl; eauto using contractive_0, contractive_S. }
rewrite -(fixpoint_unique fp2) //. rewrite -(fixpoint_unique fp2) //.
apply Hlim=> n /=. by apply nat_iter_ind. apply Hlim=> n /=. by apply Nat_iter_ind.
Qed. Qed.
End fixpoint. End fixpoint.
...@@ -419,7 +419,7 @@ Section fixpointK. ...@@ -419,7 +419,7 @@ Section fixpointK.
P (fixpointK k f). P (fixpointK k f).
Proof. Proof.
intros. rewrite /fixpointK. apply fixpoint_ind; eauto. intros. rewrite /fixpointK. apply fixpoint_ind; eauto.
intros; apply nat_iter_ind; auto. intros; apply Nat_iter_ind; auto.
Qed. Qed.
End fixpointK. End fixpointK.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment