From b2903d4f332d4bda4694f500421e982092561eed Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Sat, 3 Oct 2020 13:33:17 +0200 Subject: [PATCH] Add conversion function `pos_to_Qp` from `positive` to `Qp`. --- theories/numbers.v | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/theories/numbers.v b/theories/numbers.v index 416d11d1..491d4522 100644 --- a/theories/numbers.v +++ b/theories/numbers.v @@ -764,6 +764,10 @@ Definition Qp_min (q p : Qp) : Qp := if decide (q ≤ p) then q else p. Infix "`max`" := Qp_max : Qp_scope. Infix "`min`" := Qp_min : Qp_scope. +Program Definition pos_to_Qp (n : positive) : Qp := mk_Qp (Z.pos n) _. +Next Obligation. intros n. by rewrite <-Z2Qc_inj_0, <-Z2Qc_inj_lt. Qed. +Arguments pos_to_Qp : simpl never. + Instance Qp_inhabited : Inhabited Qp := populate 1. Instance Qp_plus_assoc : Assoc (=) Qp_plus. @@ -1163,6 +1167,21 @@ Qed. Lemma Qp_min_r_iff q p : q `min` p = p ↔ p ≤ q. Proof. rewrite (comm_L Qp_min q). apply Qp_min_l_iff. Qed. +Lemma pos_to_Qp_1 : pos_to_Qp 1 = 1. +Proof. apply (bool_decide_unpack _); by compute. Qed. +Lemma pos_to_Qp_inj n m : pos_to_Qp n = pos_to_Qp m → n = m. +Proof. by injection 1. Qed. +Lemma pos_to_Qp_inj_iff n m : pos_to_Qp n = pos_to_Qp m ↔ n = m. +Proof. split; [apply pos_to_Qp_inj|by intros ->]. Qed. +Lemma pos_to_Qp_inj_le n m : (n ≤ m)%positive ↔ pos_to_Qp n ≤ pos_to_Qp m. +Proof. rewrite Qp_to_Qc_inj_le; simpl. by rewrite <-Z2Qc_inj_le. Qed. +Lemma pos_to_Qp_inj_lt n m : (n < m)%positive ↔ pos_to_Qp n < pos_to_Qp m. +Proof. by rewrite Pos.lt_nle, Qp_lt_nge, <-pos_to_Qp_inj_le. Qed. +Lemma pos_to_Qp_plus x y : pos_to_Qp x + pos_to_Qp y = pos_to_Qp (x + y). +Proof. apply Qp_to_Qc_inj_iff; simpl. by rewrite Pos2Z.inj_add, Z2Qc_inj_add. Qed. +Lemma pos_to_Qp_mult x y : pos_to_Qp x * pos_to_Qp y = pos_to_Qp (x * y). +Proof. apply Qp_to_Qc_inj_iff; simpl. by rewrite Pos2Z.inj_mul, Z2Qc_inj_mul. Qed. + Local Close Scope Qp_scope. (** * Helper for working with accessing lists with wrap-around -- GitLab