diff --git a/theories/countable.v b/theories/countable.v index d73d18c9f95e55b8d2c358b77ab73d1a73852cee..72eeb254780c08fa01ac58b946d064ea7cf7282e 100644 --- a/theories/countable.v +++ b/theories/countable.v @@ -273,13 +273,8 @@ Next Obligation. Qed. Global Program Instance Qp_countable : Countable Qp := - inj_countable - Qp_to_Qc - (λ p : Qc, guard (0 < p)%Qc as Hp; Some (mk_Qp p Hp)) _. -Next Obligation. - intros [p Hp]. unfold mguard, option_guard; simpl. - case_match; [|done]. f_equal. by apply Qp_to_Qc_inj_iff. -Qed. + inj_countable Qp_to_Qc Qc_to_Qp _. +Next Obligation. intros p. by apply Qc_to_Qp_Some. Qed. Global Program Instance fin_countable n : Countable (fin n) := inj_countable diff --git a/theories/numbers.v b/theories/numbers.v index 9600f0fc46d6493dc07613f450e13acb954beb22..22a6dd9d2d498e0df2eb876ea9dd17dcb80a17d2 100644 --- a/theories/numbers.v +++ b/theories/numbers.v @@ -3,7 +3,7 @@ natural numbers, and the type [Z] for integers. It also declares some useful notations. *) From Coq Require Export EqdepFacts PArith NArith ZArith NPeano. From Coq Require Import QArith Qcanon. -From stdpp Require Export base decidable option. +From stdpp Require Export base decidable option sprop. From stdpp Require Import options. Local Open Scope nat_scope. @@ -721,77 +721,104 @@ Qed. Local Close Scope Qc_scope. (** * Positive rationals *) -Declare Scope Qp_scope. -Delimit Scope Qp_scope with Qp. +Definition Qp_red (q : positive * positive) : positive * positive := + (Pos.ggcd (q.1) (q.2)).2. +Definition Qp_wf (q : positive * positive) : SProp := + sprop_decide (Qp_red q = q). + +Lemma Qp_red_wf q : Qp_wf (Qp_red q). +Proof. + apply sprop_decide_pack. unfold Qp_red. destruct q as [n d]; simpl. + pose proof (Pos.ggcd_greatest n d) as Hgreatest. + destruct (Pos.ggcd n d) as [q [r1 r2]] eqn:?; simpl in *. + pose proof (Pos.ggcd_correct_divisors r1 r2) as Hdiv. + destruct (Pos.ggcd r1 r2) as [q' [r1' r2']] eqn:?; simpl in *. + destruct Hdiv as [-> ->]. + rewrite (Hgreatest q') by (by apply Pos.divide_mul_l, Z.divide_Zpos). + by rewrite !Pos.mul_1_l. +Qed. + +Record Qp := QP' { + Qp_car : positive * positive; + Qp_prf : Qp_wf Qp_car; +}. +Definition QP (n d : positive) : Qp := + QP' (Qp_red (n,d)) (Qp_red_wf _). -Record Qp := mk_Qp { Qp_to_Qc : Qc ; Qp_prf : (0 < Qp_to_Qc)%Qc }. Add Printing Constructor Qp. + +Declare Scope Qp_scope. +Delimit Scope Qp_scope with Qp. Bind Scope Qp_scope with Qp. -Global Arguments Qp_to_Qc _%Qp : assert. Local Open Scope Qp_scope. -Lemma Qp_to_Qc_inj_iff p q : Qp_to_Qc p = Qp_to_Qc q ↔ p = q. -Proof. - split; [|by intros ->]. - destruct p, q; intros; simplify_eq/=; f_equal; apply (proof_irrel _). -Qed. -Global Instance Qp_eq_dec : EqDecision Qp. -Proof. - refine (λ p q, cast_if (decide (Qp_to_Qc p = Qp_to_Qc q))); - by rewrite <-Qp_to_Qc_inj_iff. -Defined. - +(** ** Operations *) Definition Qp_add (p q : Qp) : Qp := - let 'mk_Qp p Hp := p in let 'mk_Qp q Hq := q in - mk_Qp (p + q) (Qcplus_pos_pos _ _ Hp Hq). + let '(QP' (pn,pd) _) := p in let '(QP' (qn,qd) _) := q in + QP (pn * qd + qn * pd) (pd * qd). Global Arguments Qp_add : simpl never. Definition Qp_sub (p q : Qp) : option Qp := - let 'mk_Qp p Hp := p in let 'mk_Qp q Hq := q in - let pq := (p - q)%Qc in - guard (0 < pq)%Qc as Hpq; Some (mk_Qp pq Hpq). + let '(QP' (pn,pd) _) := p in let '(QP' (qn,qd) _) := q in + guard (qn * pd < pn * qd)%positive; + Some (QP (pn * qd - qn * pd) (pd * qd)). Global Arguments Qp_sub : simpl never. Definition Qp_mul (p q : Qp) : Qp := - let 'mk_Qp p Hp := p in let 'mk_Qp q Hq := q in - mk_Qp (p * q) (Qcmult_pos_pos _ _ Hp Hq). + let '(QP' (pn,pd) _) := p in let '(QP' (qn,qd) _) := q in + QP (pn * qn) (pd * qd). Global Arguments Qp_mul : simpl never. Definition Qp_inv (q : Qp) : Qp := - let 'mk_Qp q Hq := q return _ in - mk_Qp (/ q)%Qc (Qcinv_pos _ Hq). + let '(QP' (qn,qd) _) := q in + QP qd qn. Global Arguments Qp_inv : simpl never. Definition Qp_div (p q : Qp) : Qp := Qp_mul p (Qp_inv q). Typeclasses Opaque Qp_div. Global Arguments Qp_div : simpl never. +Definition pos_to_Qp (n : positive) : Qp := QP n 1. +Global Arguments pos_to_Qp : simpl never. + +Definition Qp_to_Q (q : Qp) : Q := + let '(QP' (pn,pd) _) := q in + Qmake (Z.pos pn) pd. + +Lemma Qred_Qp_to_Q q : Qred (Qp_to_Q q) = Qp_to_Q q. +Proof. + destruct q as [[qn qd] Hq]; unfold Qred; simpl. + apply sprop_decide_unpack in Hq; unfold Qp_red in Hq; simpl in *. + destruct (Pos.ggcd qn qd) as [? [??]]; by simplify_eq/=. +Qed. +Definition Qp_to_Qc (q : Qp) : Qc := Qcmake (Qp_to_Q q) (Qred_Qp_to_Q q). + +Definition Qc_to_Qp (q : Qc) : option Qp := + match q return _ with + | Qcmake (Qmake (Z.pos n) d) _ => Some (QP n d) + | _ => None + end. + +Definition Qp_le (p q : Qp) : Prop := + let '(QP' (pn,pd) _) := p in let '(QP' (qn,qd) _) := q in + (pn * qd ≤ qn * pd)%positive. +Definition Qp_lt (p q : Qp) : Prop := + let '(QP' (pn,pd) _) := p in let '(QP' (qn,qd) _) := q in + (pn * qd < qn * pd)%positive. + +(** ** Notations *) Infix "+" := Qp_add : Qp_scope. Infix "-" := Qp_sub : Qp_scope. Infix "*" := Qp_mul : Qp_scope. Notation "/ q" := (Qp_inv q) : Qp_scope. Infix "/" := Qp_div : Qp_scope. -Lemma Qp_to_Qc_inj_add p q : (Qp_to_Qc (p + q) = Qp_to_Qc p + Qp_to_Qc q)%Qc. -Proof. by destruct p, q. Qed. -Lemma Qp_to_Qc_inj_mul p q : (Qp_to_Qc (p * q) = Qp_to_Qc p * Qp_to_Qc q)%Qc. -Proof. by destruct p, q. Qed. - -Program Definition pos_to_Qp (n : positive) : Qp := mk_Qp (Qc_of_Z $ Z.pos n) _. -Next Obligation. intros n. by rewrite <-Z2Qc_inj_0, <-Z2Qc_inj_lt. Qed. -Global Arguments pos_to_Qp : simpl never. - Notation "1" := (pos_to_Qp 1) : Qp_scope. Notation "2" := (pos_to_Qp 2) : Qp_scope. Notation "3" := (pos_to_Qp 3) : Qp_scope. Notation "4" := (pos_to_Qp 4) : Qp_scope. -Definition Qp_le (p q : Qp) : Prop := - let 'mk_Qp p _ := p in let 'mk_Qp q _ := q in (p ≤ q)%Qc. -Definition Qp_lt (p q : Qp) : Prop := - let 'mk_Qp p _ := p in let 'mk_Qp q _ := q in (p < q)%Qc. - Infix "≤" := Qp_le : Qp_scope. Infix "<" := Qp_lt : Qp_scope. Notation "p ≤ q ≤ r" := (p ≤ q ∧ q ≤ r) : Qp_scope. @@ -804,56 +831,141 @@ Notation "(<)" := Qp_lt (only parsing) : Qp_scope. Global Hint Extern 0 (_ ≤ _)%Qp => reflexivity : core. +(** ** Properties about the conversion to [Qc] *) +(** After having proved these, we never break the [Qp] abstraction and derive +all [Qp] properties from the corresponding properties for [Qc]. *) +Lemma Qp_to_Qc_pos p : (0 < Qp_to_Qc p)%Qc. +Proof. destruct p as [[pn pd] Hp]. unfold Qclt, Qlt; simpl; lia. Qed. +Lemma Qp_to_Qc_inj_add p q : Qp_to_Qc (p + q) = (Qp_to_Qc p + Qp_to_Qc q)%Qc. +Proof. + destruct p as [[pn pd] Hp], q as [[qn qd] Hq]; simpl. unfold Qp_add. + apply Qc_is_canon; simpl. unfold Qeq, Qp_red, Qred; simpl. + by destruct (Pos.ggcd _ _) as [? [??]]. +Qed. +Lemma Qp_to_Qc_inj_sub p q : + Qp_to_Qc <$> (p - q) = + guard (Qp_to_Qc q < Qp_to_Qc p)%Qc; Some (Qp_to_Qc p - Qp_to_Qc q)%Qc. +Proof. + destruct p as [[pn pd] Hp], q as [[qn qd] Hq]; simpl. unfold Qp_sub. + case_option_guard as Hpq; [|by rewrite option_guard_False]. + rewrite option_guard_True by done; f_equal/=. + apply Qc_is_canon; simpl. rewrite (Qred_correct (- _)). + unfold Qeq, Qp_red, Qred; simpl. + replace (Z.pos pn * Z.pos qd + - Z.pos qn * Z.pos pd)%Z + with (Z.pos (pn * qd - qn * pd)) by lia; simpl. + by destruct (Pos.ggcd _ _) as [? [??]]. +Qed. +Lemma Qp_to_Qc_inj_mul p q : Qp_to_Qc (p * q) = (Qp_to_Qc p * Qp_to_Qc q)%Qc. +Proof. + destruct p as [[pn pd] Hp], q as [[qn qd] Hq]; simpl. + apply Qc_is_canon; simpl. unfold Qeq, Qp_red, Qred; simpl. + by destruct (Pos.ggcd _ _) as [? [??]]. +Qed. +Lemma Qp_to_Qc_inj_inv p : Qp_to_Qc (/ p) = (/ Qp_to_Qc p)%Qc. +Proof. + destruct p as [[pn pd] Hp]. + apply Qc_is_canon; simpl. unfold Qeq, Qp_red, Qred; simpl. + by destruct (Pos.ggcd _ _) as [? [??]]. +Qed. +Lemma Qp_to_Qc_inj_div p q : Qp_to_Qc (p / q) = (Qp_to_Qc p / Qp_to_Qc q)%Qc. +Proof. unfold Qp_div. by rewrite Qp_to_Qc_inj_mul, Qp_to_Qc_inj_inv. Qed. +Lemma Qp_to_Qc_inj_iff p q : Qp_to_Qc p = Qp_to_Qc q ↔ p = q. +Proof. + split; [|by intros ->]. + destruct p as [[pn pd] Hp], q as [[qn qd] Hq]; simpl. by intros [= -> ->]. +Qed. Lemma Qp_to_Qc_inj_le p q : p ≤ q ↔ (Qp_to_Qc p ≤ Qp_to_Qc q)%Qc. -Proof. by destruct p, q. Qed. +Proof. by destruct p as [[pn pd] ?], q as [[qn qd] ?]. Qed. Lemma Qp_to_Qc_inj_lt p q : p < q ↔ (Qp_to_Qc p < Qp_to_Qc q)%Qc. -Proof. by destruct p, q. Qed. +Proof. by destruct p as [[pn pd] ?], q as [[qn qd] ?]. Qed. +Lemma Qp_to_Qc_pos_to_Qp n : Qp_to_Qc (pos_to_Qp n) = Qc_of_Z (Z.pos n). +Proof. + apply Qc_is_canon. unfold Qeq. simpl. unfold Qp_red; simpl. + pose proof (Pos.ggcd_correct_divisors n 1) as Hdiv. + destruct (Pos.ggcd _ _) as [p [r1 r2]]; simpl in *. + destruct Hdiv as [-> ?]. + rewrite (Pos.mul_eq_1_l p r2), (Pos.mul_eq_1_r p r2) by done. lia. +Qed. +Lemma Qc_to_Qp_Some p q : Qc_to_Qp p = Some q ↔ p = Qp_to_Qc q. +Proof. + split. + - intros Hpq. destruct p as [[[|pn|] pd] Hp]; simplify_eq/=. + apply Qc_is_canon; simpl. rewrite <-Hp. unfold Qeq, Qp_red, Qred; simpl. + by destruct (Pos.ggcd _ _) as [? [??]]. + - intros ->. destruct q as [[qn qd] Hq]; simpl. + f_equal. unfold QP. + generalize (sprop_decide_unpack _ Hq). generalize (Qp_red_wf (qn, qd)). + generalize (Qp_red (qn, qd)). by intros ?? ->. +Qed. +(** ** Basic type class instances *) +Global Instance Qp_eq_dec : EqDecision Qp. +Proof. + refine (λ p q, cast_if (decide (Qp_to_Qc p = Qp_to_Qc q))); + by rewrite <-Qp_to_Qc_inj_iff. +Defined. Global Instance Qp_le_dec : RelDecision (≤). Proof. refine (λ p q, cast_if (decide (Qp_to_Qc p ≤ Qp_to_Qc q)%Qc)); by rewrite Qp_to_Qc_inj_le. -Qed. +Defined. Global Instance Qp_lt_dec : RelDecision (<). Proof. refine (λ p q, cast_if (decide (Qp_to_Qc p < Qp_to_Qc q)%Qc)); by rewrite Qp_to_Qc_inj_lt. -Qed. +Defined. Global Instance Qp_lt_pi p q : ProofIrrel (p < q). -Proof. destruct p, q; apply _. Qed. +Proof. + destruct p as [[pn pd] ?], q as [[qn qd] ?]. unfold Qp_lt, Pos.lt. apply _. +Qed. + +Global Instance Qp_inhabited : Inhabited Qp := populate 1. +(** ** Lattice structure *) Definition Qp_max (q p : Qp) : Qp := if decide (q ≤ p) then p else q. 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. -Global Instance Qp_inhabited : Inhabited Qp := populate 1. - +(** ** Algebraic properties *) Global Instance Qp_add_assoc : Assoc (=) Qp_add. -Proof. intros [p ?] [q ?] [r ?]; apply Qp_to_Qc_inj_iff, Qcplus_assoc. Qed. +Proof. + intros p q r. apply Qp_to_Qc_inj_iff. + by rewrite !Qp_to_Qc_inj_add, Qcplus_assoc. +Qed. Global Instance Qp_add_comm : Comm (=) Qp_add. -Proof. intros [p ?] [q ?]; apply Qp_to_Qc_inj_iff, Qcplus_comm. Qed. +Proof. + intros p q. apply Qp_to_Qc_inj_iff. + by rewrite !Qp_to_Qc_inj_add, Qcplus_comm. +Qed. Global Instance Qp_add_inj_r p : Inj (=) (=) (Qp_add p). Proof. - destruct p as [p ?]. - intros [q1 ?] [q2 ?]. rewrite <-!Qp_to_Qc_inj_iff; simpl. apply (inj (Qcplus p)). + intros q1 q2. rewrite <-!Qp_to_Qc_inj_iff, !Qp_to_Qc_inj_add. + apply (inj (Qcplus (Qp_to_Qc p))). Qed. Global Instance Qp_add_inj_l p : Inj (=) (=) (λ q, q + p). Proof. - destruct p as [p ?]. - intros [q1 ?] [q2 ?]. rewrite <-!Qp_to_Qc_inj_iff; simpl. apply (inj (λ q, q + p)%Qc). + intros q1 q2. rewrite <-!Qp_to_Qc_inj_iff, !Qp_to_Qc_inj_add. + apply (inj (λ q, q + Qp_to_Qc p)%Qc). Qed. Global Instance Qp_mul_assoc : Assoc (=) Qp_mul. -Proof. intros [p ?] [q ?] [r ?]. apply Qp_to_Qc_inj_iff, Qcmult_assoc. Qed. +Proof. + intros p q r. apply Qp_to_Qc_inj_iff. + by rewrite !Qp_to_Qc_inj_mul, Qcmult_assoc. +Qed. Global Instance Qp_mul_comm : Comm (=) Qp_mul. -Proof. intros [p ?] [q ?]; apply Qp_to_Qc_inj_iff, Qcmult_comm. Qed. +Proof. + intros p q. apply Qp_to_Qc_inj_iff. + by rewrite !Qp_to_Qc_inj_mul, Qcmult_comm. +Qed. Global Instance Qp_mul_inj_r p : Inj (=) (=) (Qp_mul p). Proof. - destruct p as [p ?]. intros [q1 ?] [q2 ?]. rewrite <-!Qp_to_Qc_inj_iff; simpl. + intros q1 q2. rewrite <-!Qp_to_Qc_inj_iff, !Qp_to_Qc_inj_mul. intros Hpq. - apply (anti_symm Qcle); apply (Qcmult_le_mono_pos_l _ _ p); by rewrite ?Hpq. + apply (anti_symm Qcle); apply (Qcmult_le_mono_pos_l _ _ (Qp_to_Qc p)); + first [apply Qp_to_Qc_pos|by rewrite Hpq]. Qed. Global Instance Qp_mul_inj_l p : Inj (=) (=) (λ q, q * p). Proof. @@ -861,23 +973,31 @@ Proof. Qed. Lemma Qp_mul_add_distr_l p q r : p * (q + r) = p * q + p * r. -Proof. destruct p, q, r; by apply Qp_to_Qc_inj_iff, Qcmult_plus_distr_r. Qed. +Proof. + by rewrite <-Qp_to_Qc_inj_iff, Qp_to_Qc_inj_add, + !Qp_to_Qc_inj_mul, Qp_to_Qc_inj_add, Qcmult_plus_distr_r. +Qed. Lemma Qp_mul_add_distr_r p q r : (p + q) * r = p * r + q * r. -Proof. destruct p, q, r; by apply Qp_to_Qc_inj_iff, Qcmult_plus_distr_l. Qed. +Proof. + by rewrite <-Qp_to_Qc_inj_iff, Qp_to_Qc_inj_add, + !Qp_to_Qc_inj_mul, Qp_to_Qc_inj_add, Qcmult_plus_distr_l. +Qed. Lemma Qp_mul_1_l p : 1 * p = p. -Proof. destruct p; apply Qp_to_Qc_inj_iff, Qcmult_1_l. Qed. +Proof. rewrite <-Qp_to_Qc_inj_iff, Qp_to_Qc_inj_mul. apply Qcmult_1_l. Qed. Lemma Qp_mul_1_r p : p * 1 = p. -Proof. destruct p; apply Qp_to_Qc_inj_iff, Qcmult_1_r. Qed. +Proof. rewrite <-Qp_to_Qc_inj_iff, Qp_to_Qc_inj_mul. apply Qcmult_1_r. Qed. Lemma Qp_1_1 : 1 + 1 = 2. -Proof. compute_done. Qed. +Proof. done. Qed. Lemma Qp_add_diag p : p + p = 2 * p. Proof. by rewrite <-Qp_1_1, Qp_mul_add_distr_r, !Qp_mul_1_l. Qed. Lemma Qp_mul_inv_l p : /p * p = 1. Proof. - destruct p as [p ?]; apply Qp_to_Qc_inj_iff; simpl. - by rewrite Qcmult_inv_l, Z2Qc_inj_1 by (by apply not_symmetry, Qclt_not_eq). + rewrite <-Qp_to_Qc_inj_iff, Qp_to_Qc_inj_mul, Qp_to_Qc_inj_inv. + assert (Qp_to_Qc p ≠0)%Qc. + { apply not_symmetry, Qclt_not_eq, Qp_to_Qc_pos. } + rewrite Qcmult_inv_l by done. by apply Qc_is_canon. Qed. Lemma Qp_mul_inv_r p : p * /p = 1. Proof. by rewrite (comm_L Qp_mul), Qp_mul_inv_l. Qed. @@ -898,11 +1018,11 @@ Proof. by rewrite Qp_mul_inv_l, Hp, Qp_mul_inv_l. Qed. Lemma Qp_inv_1 : /1 = 1. -Proof. compute_done. Qed. +Proof. done. Qed. Lemma Qp_inv_half_half : /2 + /2 = 1. -Proof. compute_done. Qed. +Proof. done. Qed. Lemma Qp_inv_quarter_quarter : /4 + /4 = /2. -Proof. compute_done. Qed. +Proof. done. Qed. Lemma Qp_div_diag p : p / p = 1. Proof. apply Qp_mul_inv_r. Qed. @@ -931,13 +1051,13 @@ Qed. Lemma Qp_div_2_mul p q : p / (2 * q) + p / (2 * q) = p / q. Proof. by rewrite <-Qp_div_add_distr, Qp_add_diag, Qp_div_mul_cancel_l. Qed. Lemma Qp_half_half : 1 / 2 + 1 / 2 = 1. -Proof. compute_done. Qed. +Proof. done. Qed. Lemma Qp_quarter_quarter : 1 / 4 + 1 / 4 = 1 / 2. -Proof. compute_done. Qed. +Proof. done. Qed. Lemma Qp_quarter_three_quarter : 1 / 4 + 3 / 4 = 1. -Proof. compute_done. Qed. +Proof. done. Qed. Lemma Qp_three_quarter_quarter : 3 / 4 + 1 / 4 = 1. -Proof. compute_done. Qed. +Proof. done. Qed. Global Instance Qp_div_inj_r p : Inj (=) (=) (Qp_div p). Proof. unfold Qp_div; apply _. Qed. Global Instance Qp_div_inj_l p : Inj (=) (=) (λ q, q / p)%Qp. @@ -989,7 +1109,7 @@ Proof. Qed. Lemma Qp_add_le_mono_l p q r : p ≤ q ↔ r + p ≤ r + q. -Proof. rewrite !Qp_to_Qc_inj_le. destruct p, q, r; apply Qcplus_le_mono_l. Qed. +Proof. by rewrite !Qp_to_Qc_inj_le, !Qp_to_Qc_inj_add, <-Qcplus_le_mono_l. Qed. Lemma Qp_add_le_mono_r p q r : p ≤ q ↔ p + r ≤ q + r. Proof. rewrite !(comm_L Qp_add _ r). apply Qp_add_le_mono_l. Qed. Lemma Qp_add_le_mono q p n m : q ≤ n → p ≤ m → q + p ≤ n + m. @@ -1004,7 +1124,8 @@ Proof. intros. etrans; [by apply Qp_add_lt_mono_l|by apply Qp_add_lt_mono_r]. Qe Lemma Qp_mul_le_mono_l p q r : p ≤ q ↔ r * p ≤ r * q. Proof. - rewrite !Qp_to_Qc_inj_le. destruct p, q, r; by apply Qcmult_le_mono_pos_l. + assert (0 < Qp_to_Qc r)%Qc by apply Qp_to_Qc_pos. + by rewrite !Qp_to_Qc_inj_le, !Qp_to_Qc_inj_mul, <-Qcmult_le_mono_pos_l. Qed. Lemma Qp_mul_le_mono_r p q r : p ≤ q ↔ p * r ≤ q * r. Proof. rewrite !(comm_L Qp_mul _ r). apply Qp_mul_le_mono_l. Qed. @@ -1013,7 +1134,8 @@ Proof. intros. etrans; [by apply Qp_mul_le_mono_l|by apply Qp_mul_le_mono_r]. Qe Lemma Qp_mul_lt_mono_l p q r : p < q ↔ r * p < r * q. Proof. - rewrite !Qp_to_Qc_inj_lt. destruct p, q, r; by apply Qcmult_lt_mono_pos_l. + assert (0 < Qp_to_Qc r)%Qc by apply Qp_to_Qc_pos. + by rewrite !Qp_to_Qc_inj_lt, !Qp_to_Qc_inj_mul, <-Qcmult_lt_mono_pos_l. Qed. Lemma Qp_mul_lt_mono_r p q r : p < q ↔ p * r < q * r. Proof. rewrite !(comm_L Qp_mul _ r). apply Qp_mul_lt_mono_l. Qed. @@ -1022,8 +1144,9 @@ Proof. intros. etrans; [by apply Qp_mul_lt_mono_l|by apply Qp_mul_lt_mono_r]. Qe Lemma Qp_lt_add_l p q : p < p + q. Proof. - destruct p as [p ?], q as [q ?]. apply Qp_to_Qc_inj_lt; simpl. - rewrite <- (Qcplus_0_r p) at 1. by rewrite <-Qcplus_lt_mono_l. + rewrite !Qp_to_Qc_inj_lt, !Qp_to_Qc_inj_add. + rewrite <- (Qcplus_0_r (Qp_to_Qc p)) at 1. rewrite <-Qcplus_lt_mono_l. + by apply Qp_to_Qc_pos. Qed. Lemma Qp_lt_add_r p q : q < p + q. Proof. rewrite (comm_L Qp_add). apply Qp_lt_add_l. Qed. @@ -1043,24 +1166,23 @@ Proof. apply Qp_lt_le_incl, Qp_lt_add_r. Qed. Lemma Qp_sub_Some p q r : p - q = Some r ↔ p = q + r. Proof. - destruct p as [p Hp], q as [q Hq], r as [r Hr]. - unfold Qp_sub, Qp_add; simpl; rewrite <-Qp_to_Qc_inj_iff; simpl. split. - - intros; simplify_option_eq. unfold Qcminus. - by rewrite (Qcplus_comm p), Qcplus_assoc, Qcplus_opp_r, Qcplus_0_l. - - intros ->. unfold Qcminus. - rewrite <-Qcplus_assoc, (Qcplus_comm r), Qcplus_assoc. - rewrite Qcplus_opp_r, Qcplus_0_l. simplify_option_eq; [|done]. - f_equal. by apply Qp_to_Qc_inj_iff. + rewrite <-Qp_to_Qc_inj_iff, Qp_to_Qc_inj_add. + pose proof (Qp_to_Qc_inj_sub p q) as Hsub. + destruct (p - q) as [r'|]; simplify_option_eq. + - split. + + intros [= ->]. rewrite Hsub. ring. + + intros Hp. f_equal. rewrite <-Qp_to_Qc_inj_iff, Hsub, Hp. ring. + - split; [done|]. intros Hp. select (¬ _) (fun H => destruct H). + rewrite Hp. rewrite <- (Qcplus_0_r (Qp_to_Qc q)) at 1. + rewrite <-Qcplus_lt_mono_l. by apply Qp_to_Qc_pos. Qed. Lemma Qp_lt_sum p q : p < q ↔ ∃ r, q = p + r. Proof. - destruct p as [p Hp], q as [q Hq]. rewrite Qp_to_Qc_inj_lt; simpl. - split. - - intros Hlt%Qclt_minus_iff. exists (mk_Qp (q - p) Hlt). - apply Qp_to_Qc_inj_iff; simpl. unfold Qcminus. - by rewrite (Qcplus_comm q), Qcplus_assoc, Qcplus_opp_r, Qcplus_0_l. - - intros [[r ?] ?%Qp_to_Qc_inj_iff]; simplify_eq/=. - rewrite <-(Qcplus_0_r p) at 1. by apply Qcplus_lt_mono_l. + split; [|intros [r ->]; apply Qp_lt_add_l]. intros Hpq. + pose proof (Qp_to_Qc_inj_sub q p) as Hsub. + rewrite option_guard_True in Hsub by (by apply Qp_to_Qc_inj_lt). + apply fmap_Some in Hsub as [r [? Hr]]. exists r. + rewrite <-Qp_to_Qc_inj_iff, Qp_to_Qc_inj_add, <-Hr. ring. Qed. Lemma Qp_sub_None p q : p - q = None ↔ p ≤ q. @@ -1232,19 +1354,25 @@ 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. compute_done. Qed. +Proof. done. Qed. Lemma pos_to_Qp_inj n m : pos_to_Qp n = pos_to_Qp m → n = m. -Proof. by injection 1. Qed. +Proof. rewrite <-Qp_to_Qc_inj_iff, !Qp_to_Qc_pos_to_Qp. 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. +Proof. by rewrite Qp_to_Qc_inj_le, !Qp_to_Qc_pos_to_Qp, <-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_add 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. +Proof. + rewrite <-Qp_to_Qc_inj_iff, Qp_to_Qc_inj_add, !Qp_to_Qc_pos_to_Qp. + by rewrite Pos2Z.inj_add, Z2Qc_inj_add. +Qed. Lemma pos_to_Qp_mul 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. +Proof. + rewrite <-Qp_to_Qc_inj_iff, Qp_to_Qc_inj_mul, !Qp_to_Qc_pos_to_Qp. + by rewrite Pos2Z.inj_mul, Z2Qc_inj_mul. +Qed. Local Close Scope Qp_scope.