From 25f516f0ec10df60b651b250feb8369ca4c2c8fc Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Fri, 2 Oct 2020 19:01:15 +0200 Subject: [PATCH 01/12] Extend the theory of the positive rationals `Qp`. - Remove the coercion from `Qp` to `Qc`, and remove it into from `Qp_car` into `Qp_to_Qc` to be consistent with other conversion functions. - Use `let '(..) = ...` in the definitions of `Qp_plus`/`Qp_mult`/`Qp_div` to avoid Coq tactics (like `injection`) to unfold these definitions eagerly. - Define orders `Qp_le` and `Qp_lt`, instead of relying on the orders on `Qc`, which were obtained through the removed coercion into `Qc`. - Lift lemmas about the orders from `Qc` to `Qp`. - Improve variable names and use of notation scopes. --- theories/countable.v | 2 +- theories/numbers.v | 454 ++++++++++++++++++++++++++----------------- 2 files changed, 281 insertions(+), 175 deletions(-) diff --git a/theories/countable.v b/theories/countable.v index d837e7d5..0a8a4ba1 100644 --- a/theories/countable.v +++ b/theories/countable.v @@ -269,7 +269,7 @@ Qed. Program Instance Qp_countable : Countable Qp := inj_countable - Qp_car + 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. diff --git a/theories/numbers.v b/theories/numbers.v index 420c82d4..8c319507 100644 --- a/theories/numbers.v +++ b/theories/numbers.v @@ -661,155 +661,315 @@ Local Close Scope Qc_scope. Declare Scope Qp_scope. Delimit Scope Qp_scope with Qp. -(** The theory of positive rationals is very incomplete. We merely provide -some operations and theorems that are relevant for fractional permissions. *) -Record Qp := mk_Qp { Qp_car :> Qc ; Qp_prf : (0 < Qp_car)%Qc }. -Hint Resolve Qp_prf : core. -Arguments Qp_car _%Qp : assert. +Record Qp := mk_Qp { Qp_to_Qc : Qc ; Qp_prf : (0 < Qp_to_Qc)%Qc }. +Add Printing Constructor Qp. Bind Scope Qp_scope with Qp. +Arguments Qp_to_Qc _%Qp : assert. -Local Open Scope Qc_scope. Local Open Scope Qp_scope. Definition Qp_one : Qp := mk_Qp 1 eq_refl. -Program Definition Qp_plus (x y : Qp) : Qp := mk_Qp (x + y) _. -Next Obligation. by intros x y; apply Qcplus_pos_pos. Qed. -Definition Qp_minus (x y : Qp) : option Qp := - let z := (x - y)%Qc in - match decide (0 < z)%Qc with left Hz => Some (mk_Qp z Hz) | _ => None end. -Program Definition Qp_mult (x y : Qp) : Qp := mk_Qp (x * y) _. -Next Obligation. intros x y. apply Qcmult_pos_pos; apply Qp_prf. Qed. - -Program Definition Qp_div (x : Qp) (y : positive) : Qp := mk_Qp (x / Zpos y) _. + +Definition Qp_plus (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). +Arguments Qp_plus : simpl never. + +Definition Qp_minus (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). +Arguments Qp_minus : simpl never. + +Definition Qp_mult (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). +Arguments Qp_mult : simpl never. + +Program Definition Qp_div (p : Qp) (y : positive) : Qp := + let 'mk_Qp p Hp := p return _ in + mk_Qp (p / Zpos y)%Qc _. Next Obligation. - intros x y. unfold Qcdiv. assert (0 < Zpos y)%Qc. + intros _ y p Hp. unfold Qcdiv. assert (0 < Zpos y)%Qc. { apply (Z2Qc_inj_lt 0%Z (Zpos y)), Pos2Z.is_pos. } by rewrite (Qcmult_lt_mono_pos_r _ _ (Zpos y)%Z), Qcmult_0_l, <-Qcmult_assoc, Qcmult_inv_l, Qcmult_1_r. Qed. - -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. +Arguments Qp_div : simpl never. Infix "+" := Qp_plus : Qp_scope. Infix "-" := Qp_minus : Qp_scope. Infix "*" := Qp_mult : Qp_scope. Infix "/" := Qp_div : Qp_scope. -Infix "`max`" := Qp_max (at level 35) : Qp_scope. -Infix "`min`" := Qp_min (at level 35) : Qp_scope. Notation "1" := Qp_one : Qp_scope. Notation "2" := (1 + 1)%Qp : Qp_scope. Notation "3" := (1 + 2)%Qp : Qp_scope. Notation "4" := (1 + 3)%Qp : Qp_scope. -Lemma Qp_eq x y : x = y ↔ Qp_car x = Qp_car y. +Definition Qp_le (p q : Qp) := (Qp_to_Qc p ≤ Qp_to_Qc q)%Qc. +Definition Qp_lt (p q : Qp) := (Qp_to_Qc p < Qp_to_Qc q)%Qc. +Typeclasses Opaque Qp_le Qp_lt. + +Instance Qp_le_dec : RelDecision Qp_le := λ p q, + decide (Qp_to_Qc p ≤ Qp_to_Qc q)%Qc. +Instance Qp_lt_dec : RelDecision Qp_lt := λ p q, + decide (Qp_to_Qc p < Qp_to_Qc q)%Qc. + +Definition Qp_max (q p : Qp) : Qp := if decide (Qp_le q p) then p else q. +Definition Qp_min (q p : Qp) : Qp := if decide (Qp_le q p) then q else p. + +Infix "≤" := Qp_le : Qp_scope. +Infix "<" := Qp_lt : Qp_scope. +Notation "p ≤ q ≤ r" := (p ≤ q ∧ q ≤ r) : Qp_scope. +Notation "p ≤ q < r" := (p ≤ q ∧ q < r) : Qp_scope. +Notation "p < q < r" := (p < q ∧ q < r) : Qp_scope. +Notation "p < q ≤ r" := (p < q ∧ q ≤ r) : Qp_scope. +Notation "p ≤ q ≤ r ≤ r'" := (p ≤ q ∧ q ≤ r ∧ r ≤ r') : Qp_scope. +Notation "(≤)" := Qp_le (only parsing) : Qp_scope. +Notation "(<)" := Qp_lt (only parsing) : Qp_scope. + +Infix "`max`" := Qp_max : Qp_scope. +Infix "`min`" := Qp_min : Qp_scope. + +Hint Extern 0 (_ ≤ _)%Qp => reflexivity : core. + +Lemma Qp_eq p q : p = q ↔ Qp_to_Qc p = Qp_to_Qc q. Proof. split; [by intros ->|]. - destruct x, y; intros; simplify_eq/=; f_equal; apply (proof_irrel _). + destruct p, q; intros; simplify_eq/=; f_equal; apply (proof_irrel _). Qed. -Instance Qp_inhabited : Inhabited Qp := populate 1%Qp. Instance Qp_eq_dec : EqDecision Qp. Proof. - refine (λ x y, cast_if (decide (Qp_car x = Qp_car y))); by rewrite Qp_eq. + refine (λ p q, cast_if (decide (Qp_to_Qc p = Qp_to_Qc q))); by rewrite Qp_eq. Defined. +Instance Qp_inhabited : Inhabited Qp := populate 1%Qp. + Instance Qp_plus_assoc : Assoc (=) Qp_plus. -Proof. intros x y z; apply Qp_eq, Qcplus_assoc. Qed. +Proof. intros [p ?] [q ?] [r ?]; apply Qp_eq, Qcplus_assoc. Qed. Instance Qp_plus_comm : Comm (=) Qp_plus. -Proof. intros x y; apply Qp_eq, Qcplus_comm. Qed. +Proof. intros [p ?] [q ?]; apply Qp_eq, Qcplus_comm. Qed. Instance Qp_plus_inj_r p : Inj (=) (=) (Qp_plus p). -Proof. intros q1 q2. rewrite !Qp_eq; simpl. apply (inj (Qcplus p)). Qed. +Proof. + destruct p as [p ?]. + intros [q1 ?] [q2 ?]. rewrite !Qp_eq; simpl. apply (inj (Qcplus p)). +Qed. Instance Qp_plus_inj_l p : Inj (=) (=) (λ q, q + p)%Qp. -Proof. intros q1 q2. rewrite !Qp_eq; simpl. apply (inj (λ q, q + p)%Qc). Qed. - -Lemma Qp_minus_diag x : (x - x)%Qp = None. -Proof. unfold Qp_minus, Qcminus. by rewrite Qcplus_opp_r. Qed. -Lemma Qp_op_minus x y : ((x + y) - x)%Qp = Some y. Proof. - unfold Qp_minus, Qcminus; simpl. - rewrite (Qcplus_comm x), <- Qcplus_assoc, Qcplus_opp_r, Qcplus_0_r. - destruct (decide _) as [|[]]; auto. by f_equal; apply Qp_eq. + destruct p as [p ?]. + intros [q1 ?] [q2 ?]. rewrite !Qp_eq; simpl. apply (inj (λ q, q + p)%Qc). Qed. Instance Qp_mult_assoc : Assoc (=) Qp_mult. -Proof. intros x y z; apply Qp_eq, Qcmult_assoc. Qed. +Proof. intros [p ?] [q ?] [r ?]. apply Qp_eq, Qcmult_assoc. Qed. Instance Qp_mult_comm : Comm (=) Qp_mult. -Proof. intros x y; apply Qp_eq, Qcmult_comm. Qed. -Lemma Qp_mult_plus_distr_r x y z: (x * (y + z) = x * y + x * z)%Qp. -Proof. apply Qp_eq, Qcmult_plus_distr_r. Qed. -Lemma Qp_mult_plus_distr_l x y z: ((x + y) * z = x * z + y * z)%Qp. -Proof. apply Qp_eq, Qcmult_plus_distr_l. Qed. -Lemma Qp_mult_1_l x: (1 * x)%Qp = x. -Proof. apply Qp_eq, Qcmult_1_l. Qed. -Lemma Qp_mult_1_r x: (x * 1)%Qp = x. -Proof. apply Qp_eq, Qcmult_1_r. Qed. +Proof. intros [p ?] [q ?]; apply Qp_eq, Qcmult_comm. Qed. +Lemma Qp_mult_plus_distr_r p q r : p * (q + r) = p * q + p * r. +Proof. + destruct p as [p ?], q as [q ?], r as [r ?]. apply Qp_eq, Qcmult_plus_distr_r. +Qed. +Lemma Qp_mult_plus_distr_l p q r : (p + q) * r = p * r + q * r. +Proof. + destruct p as [p ?], q as [q ?], r as [r ?]. apply Qp_eq, Qcmult_plus_distr_l. +Qed. +Lemma Qp_mult_1_l p : 1 * p = p. +Proof. destruct p; apply Qp_eq, Qcmult_1_l. Qed. +Lemma Qp_mult_1_r p : p * 1 = p. +Proof. destruct p; apply Qp_eq, Qcmult_1_r. Qed. + +Lemma Qp_plus_diag p : p + p = (2 * p). +Proof. by rewrite Qp_mult_plus_distr_l, !Qp_mult_1_l. Qed. -Lemma Qp_div_1 x : (x / 1 = x)%Qp. +Lemma Qp_div_1 p : p / 1 = p. Proof. - apply Qp_eq; simpl. - rewrite <-(Qcmult_div_r x 1) at 2 by done. by rewrite Qcmult_1_l. + destruct p as [p ?]. apply Qp_eq; simpl. + rewrite <-(Qcmult_div_r p 1) at 2 by done. by rewrite Qcmult_1_l. Qed. -Lemma Qp_div_S x y : (x / (2 * y) + x / (2 * y) = x / y)%Qp. +Lemma Qp_div_S p y : p / (2 * y) + p / (2 * y) = p / y. Proof. - apply Qp_eq; simpl. unfold Qcdiv. + destruct p as [p ?]. apply Qp_eq; simpl. unfold Qcdiv. rewrite <-Qcmult_plus_distr_l, Pos2Z.inj_mul, Z2Qc_inj_mul, Z2Qc_inj_2. rewrite Qcplus_diag. by field_simplify. Qed. -Lemma Qp_div_2 x : (x / 2 + x / 2 = x)%Qp. +Lemma Qp_div_2 p : p / 2 + p / 2 = p. Proof. change 2%positive with (2 * 1)%positive. by rewrite Qp_div_S, Qp_div_1. Qed. -Lemma Qp_half_half : (1 / 2 + 1 / 2 = 1)%Qp. +Lemma Qp_half_half : 1 / 2 + 1 / 2 = 1. Proof. apply (bool_decide_unpack _); by compute. Qed. -Lemma Qp_quarter_three_quarter : (1 / 4 + 3 / 4 = 1)%Qp. +Lemma Qp_quarter_three_quarter : 1 / 4 + 3 / 4 = 1. Proof. apply (bool_decide_unpack _); by compute. Qed. -Lemma Qp_three_quarter_quarter : (3 / 4 + 1 / 4 = 1)%Qp. +Lemma Qp_three_quarter_quarter : 3 / 4 + 1 / 4 = 1. Proof. apply (bool_decide_unpack _); by compute. Qed. -Lemma Qp_lt_sum (x y : Qp) : (x < y)%Qc ↔ ∃ z, y = (x + z)%Qp. -Proof. +Instance Qp_le_po : PartialOrder (≤)%Qp. +Proof. + unfold Qp_le. split; [split|]. + - by intros p. + - intros p q r ??. by etrans. + - intros p q ??. by apply Qp_eq, Qcle_antisym. +Qed. +Instance Qp_lt_strict : StrictOrder (<)%Qp. +Proof. + unfold Qp_lt. split. + - intros p. apply (irreflexivity (<)%Qc). + - intros p q r ??. by etrans. +Qed. +Instance Qp_le_total: Total (≤)%Qp. +Proof. intros p q. apply (total Qcle). Qed. + +Lemma Qp_lt_le_weak p q : p < q → p ≤ q. +Proof. apply Qclt_le_weak. Qed. +Lemma Qp_le_lt_or_eq p q : p ≤ q → p < q ∨ p = q. +Proof. intros [? | ->%Qp_eq]%Qcle_lt_or_eq; auto. Qed. +Lemma Qp_lt_le_dec p q : {p < q} + {q ≤ p}. +Proof. apply Qclt_le_dec. Defined. +Lemma Qp_le_lt_trans p q r : p ≤ q → q < r → p < r. +Proof. apply Qcle_lt_trans. Qed. +Lemma Qp_lt_le_trans p q r : p < q → q ≤ r → p < r. +Proof. apply Qclt_le_trans. Qed. + +Lemma Qp_le_not_lt p q : p ≤ q → ¬q < p. +Proof. apply Qcle_not_lt. Qed. +Lemma Qp_not_lt_le p q : ¬p < q → q ≤ p. +Proof. apply Qcnot_lt_le. Qed. +Lemma Qp_lt_not_le p q : p < q → ¬q ≤ p. +Proof. apply Qclt_not_le. Qed. +Lemma Qp_not_le_lt p q : ¬p ≤ q →q < p. +Proof. apply Qcnot_le_lt. Qed. +Lemma Qp_le_ngt p q : p ≤ q ↔ ¬q < p. +Proof. split; auto using Qp_le_not_lt, Qp_not_lt_le. Qed. +Lemma Qp_lt_nge p q : p < q ↔ ¬q ≤ p. +Proof. split; auto using Qp_lt_not_le, Qp_not_le_lt. Qed. + +Lemma Qp_plus_le_mono_l p q r : p ≤ q ↔ r + p ≤ r + q. +Proof. destruct p, q, r; apply Qcplus_le_mono_l. Qed. +Lemma Qp_plus_le_mono_r p q r : p ≤ q ↔ p + r ≤ q + r. +Proof. rewrite !(comm_L Qp_plus _ r). apply Qp_plus_le_mono_l. Qed. +Lemma Qp_le_plus_compat q p n m : q ≤ n → p ≤ m → q + p ≤ n + m. +Proof. intros. etrans; [by apply Qp_plus_le_mono_l|by apply Qp_plus_le_mono_r]. Qed. + +Lemma Qp_plus_lt_mono_l p q r : p < q ↔ r + p < r + q. +Proof. by rewrite !Qp_lt_nge, <-Qp_plus_le_mono_l. Qed. +Lemma Qp_plus_lt_mono_r p q r : p < q ↔ p + r < q + r. +Proof. by rewrite !Qp_lt_nge, <-Qp_plus_le_mono_r. Qed. + +Lemma Qp_mult_le_mono_l p q r : p ≤ q ↔ r * p ≤ r * q. +Proof. destruct p, q, r; by apply Qcmult_le_mono_pos_l. Qed. +Lemma Qp_mult_le_mono_r p q r : p ≤ q ↔ p * r ≤ q * r. +Proof. destruct p, q, r; by apply Qcmult_le_mono_pos_r. Qed. +Lemma Qcmult_lt_mono_l p q r : p < q ↔ r * p < r * q. +Proof. destruct p, q, r; by apply Qcmult_lt_mono_pos_l. Qed. +Lemma Qcmult_lt_mono_r p q r : p < q ↔ p * r < q * r. +Proof. destruct p, q, r; by apply Qcmult_lt_mono_pos_r. Qed. + +Lemma Qp_lt_plus_r q p : p < q + p. +Proof. + destruct p as [p ?], q as [q ?]. unfold Qp_lt; simpl. + rewrite <- (Qcplus_0_l p) at 1. by rewrite <-Qcplus_lt_mono_r. +Qed. +Lemma Qp_lt_plus_l q p : q < q + p. +Proof. rewrite (comm_L Qp_plus). apply Qp_lt_plus_r. Qed. + +Lemma Qp_not_plus_ge q p : ¬(q + p ≤ q). +Proof. apply Qp_lt_not_le, Qp_lt_plus_l. Qed. +Lemma Qp_plus_id_free q p : q + p ≠ q. +Proof. intro Heq. apply (Qp_not_plus_ge q p). by rewrite Heq. Qed. + +Lemma Qp_le_plus_r q p : p ≤ q + p. +Proof. apply Qp_lt_le_weak, Qp_lt_plus_r. Qed. +Lemma Qp_le_plus_l q p : q ≤ q + p. +Proof. apply Qp_lt_le_weak, Qp_lt_plus_l. Qed. + +Lemma Qp_plus_weak_r q p o : q + p ≤ o → q ≤ o. +Proof. intros. etrans; [apply Qp_le_plus_l|done]. Qed. +Lemma Qp_plus_weak_l q p o : q + p ≤ o → p ≤ o. +Proof. rewrite (comm_L Qp_plus). apply Qp_plus_weak_r. Qed. + +Lemma Qp_plus_weak_2_r q p o : q ≤ o → q ≤ p + o. +Proof. intros. etrans; [done|apply Qp_le_plus_r]. Qed. +Lemma Qp_plus_weak_2_l q p o : q ≤ p → q ≤ p + o. +Proof. rewrite (comm_L Qp_plus). apply Qp_plus_weak_2_r. Qed. + +Lemma Qc_minus_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_minus, Qp_plus; simpl; rewrite Qp_eq; 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_eq. +Qed. +Lemma Qp_lt_sum p q : p < q ↔ ∃ r, q = p + r. +Proof. + destruct p as [p Hp], q as [q Hq]. unfold Qp_lt; simpl. split. - - intros Hlt%Qclt_minus_iff. exists (mk_Qp (y - x) Hlt). apply Qp_eq; simpl. - unfold Qcminus. by rewrite (Qcplus_comm y), Qcplus_assoc, Qcplus_opp_r, Qcplus_0_l. - - intros [z ->]; simpl. - rewrite <-(Qcplus_0_r x) at 1. apply Qcplus_lt_mono_l, Qp_prf. + - intros Hlt%Qclt_minus_iff. exists (mk_Qp (q - p) Hlt). + apply Qp_eq; simpl. unfold Qcminus. + by rewrite (Qcplus_comm q), Qcplus_assoc, Qcplus_opp_r, Qcplus_0_l. + - intros [[r ?] ?%Qp_eq]; simplify_eq/=. + rewrite <-(Qcplus_0_r p) at 1. by apply Qcplus_lt_mono_l. Qed. -Lemma Qp_lower_bound q1 q2 : ∃ q q1' q2', (q1 = q + q1' ∧ q2 = q + q2')%Qp. +Lemma Qc_minus_None p q : p - q = None ↔ p ≤ q. Proof. - revert q1 q2. cut (∀ q1 q2 : Qp, (q1 ≤ q2)%Qc → - ∃ q q1' q2', (q1 = q + q1' ∧ q2 = q + q2')%Qp). + rewrite Qp_le_ngt, Qp_lt_sum, eq_None_not_Some. + by setoid_rewrite <-Qc_minus_Some. +Qed. +Lemma Qp_minus_diag p : p - p = None. +Proof. by apply Qc_minus_None. Qed. +Lemma Qp_plus_minus p q : (p + q) - p = Some q. +Proof. by apply Qc_minus_Some. Qed. + +Lemma Qp_div_lt q y : (1 < y)%positive → q / y < q. +Proof. + intros. destruct q as [q Hq]. unfold Qp_lt, Qp_minus; simpl. + apply (Qcmult_lt_mono_pos_l _ _ (Z.pos y)); [done|]. + rewrite Qcmult_div_r by done. rewrite <- (Qcmult_1_l q) at 1. + apply Qcmult_lt_mono_pos_r; [done|]. by rewrite <-Z2Qc_inj_1, <-Z2Qc_inj_lt. +Qed. +Lemma Qp_div_le q y : q / y ≤ q. +Proof. + destruct (Pos.lt_total y 1) as [[]%Pos.nlt_1_r|[->|?]]. + - by rewrite Qp_div_1. + - by apply Qp_lt_le_weak, Qp_div_lt. +Qed. + +Lemma Qp_lower_bound q1 q2 : ∃ q q1' q2', q1 = q + q1' ∧ q2 = q + q2'. +Proof. + revert q1 q2. cut (∀ q1 q2 : Qp, q1 ≤ q2 → + ∃ q q1' q2', q1 = q + q1' ∧ q2 = q + q2'). { intros help q1 q2. - destruct (Qc_le_dec q1 q2) as [LE|LE%Qclt_nge%Qclt_le_weak]; [by eauto|]. + destruct (Qp_le_dec q1 q2) as [LE|LE%Qp_lt_nge%Qp_lt_le_weak]; [by eauto|]. destruct (help q2 q1) as (q&q1'&q2'&?&?); eauto. } intros q1 q2 Hq. exists (q1 / 2)%Qp, (q1 / 2)%Qp. - assert (0 < q2 +- q1 */ 2)%Qc as Hq2'. - { eapply Qclt_le_trans; [|by apply Qcplus_le_mono_r, Hq]. - replace (q1 +- q1 */ 2)%Qc with (q1 * (1 +- 1*/2))%Qc by ring. - replace 0%Qc with (0 * (1+-1*/2))%Qc by ring. by apply Qcmult_lt_compat_r. } - exists (mk_Qp (q2 +- q1 */ 2%Z) Hq2'). split; [by rewrite Qp_div_2|]. - apply Qp_eq; simpl. unfold Qcdiv. ring. + assert (q1 / 2 < q2) as [q2' ->]%Qp_lt_sum. + { eapply Qp_lt_le_trans, Hq. by apply Qp_div_lt. } + eexists; split; [|done]. by rewrite Qp_div_2. Qed. -Lemma Qp_lower_bound_lt (q1 q2 : Qp) : ∃ q : Qp, q < q1 ∧ q < q2. +Lemma Qp_lower_bound_lt q1 q2 : ∃ q : Qp, q < q1 ∧ q < q2. Proof. destruct (Qp_lower_bound q1 q2) as (qmin & q1' & q2' & [-> ->]). exists qmin. split; eapply Qp_lt_sum; eauto. Qed. Lemma Qp_cross_split p a b c d : - (a + b = p → c + d = p → - ∃ ac ad bc bd, ac + ad = a ∧ bc + bd = b ∧ ac + bc = c ∧ ad + bd = d)%Qp. + a + b = p → c + d = p → + ∃ ac ad bc bd, ac + ad = a ∧ bc + bd = b ∧ ac + bc = c ∧ ad + bd = d. Proof. intros H <-. revert a b c d H. cut (∀ a b c d : Qp, - (a < c)%Qc → a + b = c + d → + a < c → a + b = c + d → ∃ ac ad bc bd, ac + ad = a ∧ bc + bd = b ∧ ac + bc = c ∧ ad + bd = d)%Qp. { intros help a b c d Habcd. - destruct (Qclt_le_dec a c) as [?|[?| ->%Qp_eq]%Qcle_lt_or_eq]. + destruct (Qp_lt_le_dec a c) as [?|[?| ->]%Qp_le_lt_or_eq]. - auto. - destruct (help c d a b); [done..|]. naive_solver. - - apply (inj (Qp_plus a)) in Habcd as ->. destruct (Qp_lower_bound a d) as (q&a'&d'&->&->). + - apply (inj (Qp_plus a)) in Habcd as ->. + destruct (Qp_lower_bound a d) as (q&a'&d'&->&->). exists a', q, q, d'. repeat split; done || by rewrite (comm_L Qp_plus). } intros a b c d [e ->]%Qp_lt_sum. rewrite <-(assoc_L _). intros ->%(inj (Qp_plus a)). destruct (Qp_lower_bound a d) as (q&a'&d'&->&->). @@ -818,153 +978,99 @@ Proof. - by rewrite (assoc_L _), (comm_L Qp_plus a'). Qed. -Lemma Qp_bounded_split (p r : Qp) : ∃ q1 q2 : Qp, (q1 ≤ r)%Qc ∧ p = (q1 + q2)%Qp. -Proof. - destruct (Qclt_le_dec r p) as [?|?]. - - assert (0 < p +- r)%Qc as Hpos. - { apply (Qcplus_lt_mono_r _ _ r). rewrite <-Qcplus_assoc, (Qcplus_comm (-r)). - by rewrite Qcplus_opp_r, Qcplus_0_l, Qcplus_0_r. } - exists r, (mk_Qp _ Hpos); simpl; split; [done|]. - apply Qp_eq; simpl. rewrite Qcplus_comm, <-Qcplus_assoc, (Qcplus_comm (-r)). - by rewrite Qcplus_opp_r, Qcplus_0_r. - - exists (p / 2)%Qp, (p / 2)%Qp; split. - + trans p; [|done]. apply Qclt_le_weak, Qp_lt_sum. - exists (p / 2)%Qp. by rewrite Qp_div_2. - + by rewrite Qp_div_2. -Qed. - -Lemma Qp_not_plus_ge (q p : Qp) : ¬ (q + p)%Qp ≤ q. -Proof. - rewrite <- (Qcplus_0_r q). - intros Hle%(Qcplus_le_mono_l p 0 q)%Qcle_ngt. - apply Hle, Qp_prf. -Qed. - -Lemma Qp_ge_0 (q: Qp): (0 ≤ q)%Qc. -Proof. apply Qclt_le_weak, Qp_prf. Qed. - -Lemma Qp_le_plus_r (q p : Qp) : p ≤ q + p. -Proof. - apply (Qcplus_le_mono_l _ _ (-p)%Qc). rewrite Qcplus_comm, Qcplus_opp_r. - rewrite Qcplus_comm, <- Qcplus_assoc, Qcplus_opp_r, Qcplus_0_r. apply Qp_ge_0. -Qed. - -Lemma Qp_le_plus_l (q p : Qp) : q ≤ q + p. -Proof. rewrite Qcplus_comm. apply Qp_le_plus_r. Qed. - -Lemma Qp_le_plus_compat (q p n m : Qp) : q ≤ n → p ≤ m → q + p ≤ n + m. +Lemma Qp_bounded_split p r : ∃ q1 q2 : Qp, q1 ≤ r ∧ p = q1 + q2. Proof. - intros. eapply Qcle_trans; [by apply Qcplus_le_mono_l - |by apply Qcplus_le_mono_r]. + destruct (Qp_lt_le_dec r p) as [[q ->]%Qp_lt_sum|?]. + { by exists r, q. } + exists (p / 2)%Qp, (p / 2)%Qp; split. + + trans p; [|done]. apply Qp_div_le. + + by rewrite Qp_div_2. Qed. -Lemma Qp_plus_id_free q p : q + p = q → False. -Proof. intro Heq. apply (Qp_not_plus_ge q p). by rewrite Heq. Qed. - -Lemma Qp_plus_weak_r (q p o : Qp) : q + p ≤ o → q ≤ o. -Proof. intros Le. eapply Qcle_trans; [ apply Qp_le_plus_l | apply Le ]. Qed. - -Lemma Qp_plus_weak_l (q p o : Qp) : q + p ≤ o → p ≤ o. -Proof. rewrite Qcplus_comm. apply Qp_plus_weak_r. Qed. - -Lemma Qp_plus_weak_2_r (q p o : Qp) : q ≤ o → q ≤ p + o. -Proof. intros Le. eapply Qcle_trans; [apply Le| apply Qp_le_plus_r]. Qed. - -Lemma Qp_plus_weak_2_l (q p o : Qp) : q ≤ p → q ≤ p + o. -Proof. rewrite Qcplus_comm. apply Qp_plus_weak_2_r. Qed. - -Lemma Qp_max_spec (q p : Qp) : (q < p ∧ q `max` p = p) ∨ (p ≤ q ∧ q `max` p = q). +Lemma Qp_max_spec q p : (q < p ∧ q `max` p = p) ∨ (p ≤ q ∧ q `max` p = q). Proof. unfold Qp_max. - destruct (decide (q ≤ p)) as [[?| ->%Qp_eq]%Qcle_lt_or_eq|?]; [by auto..|]. - right. split; [|done]. by apply Qclt_le_weak, Qcnot_le_lt. + destruct (decide (q ≤ p)) as [[?| ->]%Qp_le_lt_or_eq|?]; [by auto..|]. + right. split; [|done]. by apply Qp_lt_le_weak, Qp_not_le_lt. Qed. -Lemma Qp_max_spec_le (q p : Qp) : (q ≤ p ∧ q `max` p = p) ∨ (p ≤ q ∧ q `max` p = q). -Proof. destruct (Qp_max_spec q p) as [[?%Qclt_le_weak?]|]; [left|right]; done. Qed. +Lemma Qp_max_spec_le q p : (q ≤ p ∧ q `max` p = p) ∨ (p ≤ q ∧ q `max` p = q). +Proof. destruct (Qp_max_spec q p) as [[?%Qp_lt_le_weak?]|]; [left|right]; done. Qed. Instance Qp_max_assoc : Assoc (=) Qp_max. Proof. intros q p o. unfold Qp_max. destruct (decide (q ≤ p)), (decide (p ≤ o)); - eauto using decide_True, Qcle_trans. + try by rewrite ?decide_True by (by etrans). rewrite decide_False by done. - by rewrite decide_False by (eapply Qclt_not_le, Qclt_trans; by apply Qclt_nge). + by rewrite decide_False by (apply Qp_lt_not_le; etrans; by apply Qp_lt_nge). Qed. Instance Qp_max_comm : Comm (=) Qp_max. Proof. - intros q p. apply Qp_eq. - destruct (Qp_max_spec_le q p) as [[?->]|[?->]], (Qp_max_spec_le p q) as [[?->]|[?->]]; - eauto using Qcle_antisym. + intros q p. + destruct (Qp_max_spec_le q p) as [[?->]|[?->]], + (Qp_max_spec_le p q) as [[?->]|[?->]]; done || by apply (anti_symm (≤)). Qed. Lemma Qp_max_id q : q `max` q = q. Proof. by destruct (Qp_max_spec q q) as [[_->]|[_->]]. Qed. -Lemma Qp_le_max_l (q p : Qp) : q ≤ q `max` p. +Lemma Qp_le_max_l q p : q ≤ q `max` p. Proof. unfold Qp_max. by destruct (decide (q ≤ p)). Qed. +Lemma Qp_le_max_r q p : p ≤ q `max` p. +Proof. rewrite (comm_L Qp_max q). apply Qp_le_max_l. Qed. -Lemma Qp_le_max_r (q p : Qp) : p ≤ q `max` p. -Proof. rewrite (comm _ q). apply Qp_le_max_l. Qed. - -Lemma Qp_max_plus (q p : Qp) : q `max` p ≤ q + p. +Lemma Qp_max_plus q p : q `max` p ≤ q + p. Proof. - unfold Qp_max. destruct (decide (q ≤ p)). - - apply Qp_le_plus_r. - - apply Qp_le_plus_l. -Qed. - -Lemma Qp_max_lub_l (q p o : Qp) : q `max` p ≤ o → q ≤ o. -Proof. - unfold Qp_max. destruct (decide (q ≤ p)); [by apply Qcle_trans | done]. + unfold Qp_max. + destruct (decide (q ≤ p)); [apply Qp_le_plus_r|apply Qp_le_plus_l]. Qed. -Lemma Qp_max_lub_r (q p o : Qp) : q `max` p ≤ o → p ≤ o. +Lemma Qp_max_lub_l q p o : q `max` p ≤ o → q ≤ o. +Proof. unfold Qp_max. destruct (decide (q ≤ p)); [by etrans|done]. Qed. +Lemma Qp_max_lub_r q p o : q `max` p ≤ o → p ≤ o. Proof. rewrite (comm _ q). apply Qp_max_lub_l. Qed. -Lemma Qp_min_spec (q p : Qp) : (q < p ∧ q `min` p = q) ∨ (p ≤ q ∧ q `min` p = p). +Lemma Qp_min_spec q p : (q < p ∧ q `min` p = q) ∨ (p ≤ q ∧ q `min` p = p). Proof. unfold Qp_min. - destruct (decide (q ≤ p)) as [[?| ->%Qp_eq]%Qcle_lt_or_eq|?]; [by auto..|]. - right. split; [|done]. by apply Qclt_le_weak, Qcnot_le_lt. + destruct (decide (q ≤ p)) as [[?| ->]%Qp_le_lt_or_eq|?]; [by auto..|]. + right. split; [|done]. by apply Qp_lt_le_weak, Qp_not_le_lt. Qed. -Lemma Qp_min_spec_le (q p : Qp) : (q ≤ p ∧ q `min` p = q) ∨ (p ≤ q ∧ q `min` p = p). -Proof. destruct (Qp_min_spec q p) as [[?%Qclt_le_weak?]|]; [left|right]; done. Qed. +Lemma Qp_min_spec_le q p : (q ≤ p ∧ q `min` p = q) ∨ (p ≤ q ∧ q `min` p = p). +Proof. destruct (Qp_min_spec q p) as [[?%Qp_lt_le_weak?]|]; [left|right]; done. Qed. Instance Qp_min_assoc : Assoc (=) Qp_min. Proof. intros q p o. unfold Qp_min. destruct (decide (q ≤ p)), (decide (p ≤ o)); eauto using decide_False. - - rewrite decide_True by done. by rewrite decide_True by (eapply Qcle_trans; done). - - by rewrite (decide_False _ _) by (eapply Qclt_not_le, Qclt_trans; by apply Qclt_nge). + - by rewrite !decide_True by (by etrans). + - by rewrite decide_False by (apply Qp_lt_not_le; etrans; by apply Qp_lt_nge). Qed. Instance Qp_min_comm : Comm (=) Qp_min. Proof. - intros q p. apply Qp_eq. - destruct (Qp_min_spec_le q p) as [[?->]|[?->]], (Qp_min_spec_le p q) as [[? ->]|[? ->]]; - eauto using Qcle_antisym. + intros q p. + destruct (Qp_min_spec_le q p) as [[?->]|[?->]], + (Qp_min_spec_le p q) as [[? ->]|[? ->]]; done || by apply (anti_symm (≤)). Qed. -Lemma Qp_min_id (q : Qp) : q `min` q = q. +Lemma Qp_min_id q : q `min` q = q. Proof. by destruct (Qp_min_spec q q) as [[_->]|[_->]]. Qed. - -Lemma Qp_le_min_r (q p : Qp) : q `min` p ≤ p. +Lemma Qp_le_min_r q p : q `min` p ≤ p. Proof. by destruct (Qp_min_spec_le q p) as [[?->]|[?->]]. Qed. -Lemma Qp_le_min_l (p q : Qp) : p `min` q ≤ p. -Proof. rewrite (comm _ p). apply Qp_le_min_r. Qed. +Lemma Qp_le_min_l p q : p `min` q ≤ p. +Proof. rewrite (comm_L Qp_min p). apply Qp_le_min_r. Qed. -Lemma Qp_min_l_iff (q p : Qp) : q `min` p = q ↔ q ≤ p. +Lemma Qp_min_l_iff q p : q `min` p = q ↔ q ≤ p. Proof. destruct (Qp_min_spec_le q p) as [[?->]|[?->]]; [done|]. - split; [by intros ->|]. intros. by apply Qp_eq, Qcle_antisym. + split; [by intros ->|]. intros. by apply (anti_symm (≤)). Qed. - -Lemma Qp_min_r_iff (q p : Qp) : q `min` p = p ↔ p ≤ q. -Proof. rewrite (comm _ q). apply Qp_min_l_iff. 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. Local Close Scope Qp_scope. -Local Close Scope Qc_scope. (** * Helper for working with accessing lists with wrap-around See also [rotate] and [rotate_take] in [list.v] *) -- GitLab From 9b68ea9431da3274705d6ef0157d7fc0f42dea01 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Fri, 2 Oct 2020 19:04:01 +0200 Subject: [PATCH 02/12] Rename `Qp_eq` into `Qp_to_Qc_inj_iff`. This follows the standard naming for Coq numbers, and avoids one using the old lemma to break abstraction accidentally. --- theories/countable.v | 2 +- theories/numbers.v | 47 +++++++++++++++++++++----------------------- 2 files changed, 23 insertions(+), 26 deletions(-) diff --git a/theories/countable.v b/theories/countable.v index 0a8a4ba1..2c07d66b 100644 --- a/theories/countable.v +++ b/theories/countable.v @@ -273,7 +273,7 @@ Program Instance Qp_countable : Countable Qp := (λ 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_eq. + case_match; [|done]. f_equal. by apply Qp_to_Qc_inj_iff. Qed. Program Instance fin_countable n : Countable (fin n) := diff --git a/theories/numbers.v b/theories/numbers.v index 8c319507..96bc2540 100644 --- a/theories/numbers.v +++ b/theories/numbers.v @@ -733,62 +733,59 @@ Infix "`min`" := Qp_min : Qp_scope. Hint Extern 0 (_ ≤ _)%Qp => reflexivity : core. -Lemma Qp_eq p q : p = q ↔ Qp_to_Qc p = Qp_to_Qc q. +Lemma Qp_to_Qc_inj_iff p q : Qp_to_Qc p = Qp_to_Qc q ↔ p = q. Proof. - split; [by intros ->|]. + split; [|by intros ->]. destruct p, q; intros; simplify_eq/=; f_equal; apply (proof_irrel _). Qed. Instance Qp_eq_dec : EqDecision Qp. Proof. - refine (λ p q, cast_if (decide (Qp_to_Qc p = Qp_to_Qc q))); by rewrite Qp_eq. + refine (λ p q, cast_if (decide (Qp_to_Qc p = Qp_to_Qc q))); + by rewrite <-Qp_to_Qc_inj_iff. Defined. Instance Qp_inhabited : Inhabited Qp := populate 1%Qp. Instance Qp_plus_assoc : Assoc (=) Qp_plus. -Proof. intros [p ?] [q ?] [r ?]; apply Qp_eq, Qcplus_assoc. Qed. +Proof. intros [p ?] [q ?] [r ?]; apply Qp_to_Qc_inj_iff, Qcplus_assoc. Qed. Instance Qp_plus_comm : Comm (=) Qp_plus. -Proof. intros [p ?] [q ?]; apply Qp_eq, Qcplus_comm. Qed. +Proof. intros [p ?] [q ?]; apply Qp_to_Qc_inj_iff, Qcplus_comm. Qed. Instance Qp_plus_inj_r p : Inj (=) (=) (Qp_plus p). Proof. destruct p as [p ?]. - intros [q1 ?] [q2 ?]. rewrite !Qp_eq; simpl. apply (inj (Qcplus p)). + intros [q1 ?] [q2 ?]. rewrite <-!Qp_to_Qc_inj_iff; simpl. apply (inj (Qcplus p)). Qed. Instance Qp_plus_inj_l p : Inj (=) (=) (λ q, q + p)%Qp. Proof. destruct p as [p ?]. - intros [q1 ?] [q2 ?]. rewrite !Qp_eq; simpl. apply (inj (λ q, q + p)%Qc). + intros [q1 ?] [q2 ?]. rewrite <-!Qp_to_Qc_inj_iff; simpl. apply (inj (λ q, q + p)%Qc). Qed. Instance Qp_mult_assoc : Assoc (=) Qp_mult. -Proof. intros [p ?] [q ?] [r ?]. apply Qp_eq, Qcmult_assoc. Qed. +Proof. intros [p ?] [q ?] [r ?]. apply Qp_to_Qc_inj_iff, Qcmult_assoc. Qed. Instance Qp_mult_comm : Comm (=) Qp_mult. -Proof. intros [p ?] [q ?]; apply Qp_eq, Qcmult_comm. Qed. +Proof. intros [p ?] [q ?]; apply Qp_to_Qc_inj_iff, Qcmult_comm. Qed. Lemma Qp_mult_plus_distr_r p q r : p * (q + r) = p * q + p * r. -Proof. - destruct p as [p ?], q as [q ?], r as [r ?]. apply Qp_eq, Qcmult_plus_distr_r. -Qed. +Proof. destruct p, q, r; by apply Qp_to_Qc_inj_iff, Qcmult_plus_distr_r. Qed. Lemma Qp_mult_plus_distr_l p q r : (p + q) * r = p * r + q * r. -Proof. - destruct p as [p ?], q as [q ?], r as [r ?]. apply Qp_eq, Qcmult_plus_distr_l. -Qed. +Proof. destruct p, q, r; by apply Qp_to_Qc_inj_iff, Qcmult_plus_distr_l. Qed. Lemma Qp_mult_1_l p : 1 * p = p. -Proof. destruct p; apply Qp_eq, Qcmult_1_l. Qed. +Proof. destruct p; apply Qp_to_Qc_inj_iff, Qcmult_1_l. Qed. Lemma Qp_mult_1_r p : p * 1 = p. -Proof. destruct p; apply Qp_eq, Qcmult_1_r. Qed. +Proof. destruct p; apply Qp_to_Qc_inj_iff, Qcmult_1_r. Qed. Lemma Qp_plus_diag p : p + p = (2 * p). Proof. by rewrite Qp_mult_plus_distr_l, !Qp_mult_1_l. Qed. Lemma Qp_div_1 p : p / 1 = p. Proof. - destruct p as [p ?]. apply Qp_eq; simpl. + destruct p as [p ?]. apply Qp_to_Qc_inj_iff; simpl. rewrite <-(Qcmult_div_r p 1) at 2 by done. by rewrite Qcmult_1_l. Qed. Lemma Qp_div_S p y : p / (2 * y) + p / (2 * y) = p / y. Proof. - destruct p as [p ?]. apply Qp_eq; simpl. unfold Qcdiv. + destruct p as [p ?]. apply Qp_to_Qc_inj_iff; simpl. unfold Qcdiv. rewrite <-Qcmult_plus_distr_l, Pos2Z.inj_mul, Z2Qc_inj_mul, Z2Qc_inj_2. rewrite Qcplus_diag. by field_simplify. Qed. @@ -808,7 +805,7 @@ Proof. unfold Qp_le. split; [split|]. - by intros p. - intros p q r ??. by etrans. - - intros p q ??. by apply Qp_eq, Qcle_antisym. + - intros p q ??. by apply Qp_to_Qc_inj_iff, Qcle_antisym. Qed. Instance Qp_lt_strict : StrictOrder (<)%Qp. Proof. @@ -822,7 +819,7 @@ Proof. intros p q. apply (total Qcle). Qed. Lemma Qp_lt_le_weak p q : p < q → p ≤ q. Proof. apply Qclt_le_weak. Qed. Lemma Qp_le_lt_or_eq p q : p ≤ q → p < q ∨ p = q. -Proof. intros [? | ->%Qp_eq]%Qcle_lt_or_eq; auto. Qed. +Proof. intros [? | ->%Qp_to_Qc_inj_iff]%Qcle_lt_or_eq; auto. Qed. Lemma Qp_lt_le_dec p q : {p < q} + {q ≤ p}. Proof. apply Qclt_le_dec. Defined. Lemma Qp_le_lt_trans p q r : p ≤ q → q < r → p < r. @@ -895,22 +892,22 @@ Proof. rewrite (comm_L Qp_plus). apply Qp_plus_weak_2_r. Qed. Lemma Qc_minus_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_minus, Qp_plus; simpl; rewrite Qp_eq; simpl. split. + unfold Qp_minus, Qp_plus; 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_eq. + f_equal. by apply Qp_to_Qc_inj_iff. Qed. Lemma Qp_lt_sum p q : p < q ↔ ∃ r, q = p + r. Proof. destruct p as [p Hp], q as [q Hq]. unfold Qp_lt; simpl. split. - intros Hlt%Qclt_minus_iff. exists (mk_Qp (q - p) Hlt). - apply Qp_eq; simpl. unfold Qcminus. + 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_eq]; simplify_eq/=. + - intros [[r ?] ?%Qp_to_Qc_inj_iff]; simplify_eq/=. rewrite <-(Qcplus_0_r p) at 1. by apply Qcplus_lt_mono_l. Qed. -- GitLab From 12590bc6dfb8eacde036d734d7665545deec5b58 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Sat, 3 Oct 2020 10:35:26 +0200 Subject: [PATCH 03/12] Use `let '(...) = ...` in definitions of `Qp_le` and `Qp_lt` to avoid eager unfolding. --- theories/numbers.v | 120 +++++++++++++++++++++++++++------------------ 1 file changed, 72 insertions(+), 48 deletions(-) diff --git a/theories/numbers.v b/theories/numbers.v index 96bc2540..d510e52a 100644 --- a/theories/numbers.v +++ b/theories/numbers.v @@ -668,6 +668,17 @@ 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. +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. + Definition Qp_one : Qp := mk_Qp 1 eq_refl. Definition Qp_plus (p q : Qp) : Qp := @@ -706,17 +717,10 @@ Notation "2" := (1 + 1)%Qp : Qp_scope. Notation "3" := (1 + 2)%Qp : Qp_scope. Notation "4" := (1 + 3)%Qp : Qp_scope. -Definition Qp_le (p q : Qp) := (Qp_to_Qc p ≤ Qp_to_Qc q)%Qc. -Definition Qp_lt (p q : Qp) := (Qp_to_Qc p < Qp_to_Qc q)%Qc. -Typeclasses Opaque Qp_le Qp_lt. - -Instance Qp_le_dec : RelDecision Qp_le := λ p q, - decide (Qp_to_Qc p ≤ Qp_to_Qc q)%Qc. -Instance Qp_lt_dec : RelDecision Qp_lt := λ p q, - decide (Qp_to_Qc p < Qp_to_Qc q)%Qc. - -Definition Qp_max (q p : Qp) : Qp := if decide (Qp_le q p) then p else q. -Definition Qp_min (q p : Qp) : Qp := if decide (Qp_le q p) then q else p. +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. @@ -728,24 +732,33 @@ Notation "p ≤ q ≤ r ≤ r'" := (p ≤ q ∧ q ≤ r ∧ r ≤ r') : Qp_scope Notation "(≤)" := Qp_le (only parsing) : Qp_scope. Notation "(<)" := Qp_lt (only parsing) : Qp_scope. -Infix "`max`" := Qp_max : Qp_scope. -Infix "`min`" := Qp_min : Qp_scope. - Hint Extern 0 (_ ≤ _)%Qp => reflexivity : core. -Lemma Qp_to_Qc_inj_iff p q : Qp_to_Qc p = Qp_to_Qc q ↔ p = q. +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. +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. + +Instance Qp_le_dec : RelDecision (≤). Proof. - split; [|by intros ->]. - destruct p, q; intros; simplify_eq/=; f_equal; apply (proof_irrel _). + refine (λ p q, cast_if (decide (Qp_to_Qc p ≤ Qp_to_Qc q)%Qc)); + by rewrite Qp_to_Qc_inj_le. Qed. - -Instance Qp_eq_dec : EqDecision Qp. +Instance Qp_lt_dec : RelDecision (<). Proof. - refine (λ p q, cast_if (decide (Qp_to_Qc p = Qp_to_Qc q))); - by rewrite <-Qp_to_Qc_inj_iff. -Defined. + refine (λ p q, cast_if (decide (Qp_to_Qc p < Qp_to_Qc q)%Qc)); + by rewrite Qp_to_Qc_inj_lt. +Qed. +Instance Qp_lt_pi p q : ProofIrrel (p < q). +Proof. destruct p, q; apply _. Qed. + +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. -Instance Qp_inhabited : Inhabited Qp := populate 1%Qp. +Instance Qp_inhabited : Inhabited Qp := populate 1. Instance Qp_plus_assoc : Assoc (=) Qp_plus. Proof. intros [p ?] [q ?] [r ?]; apply Qp_to_Qc_inj_iff, Qcplus_assoc. Qed. @@ -802,46 +815,52 @@ Proof. apply (bool_decide_unpack _); by compute. Qed. Instance Qp_le_po : PartialOrder (≤)%Qp. Proof. - unfold Qp_le. split; [split|]. - - by intros p. - - intros p q r ??. by etrans. - - intros p q ??. by apply Qp_to_Qc_inj_iff, Qcle_antisym. + split; [split|]. + - intros p. by apply Qp_to_Qc_inj_le. + - intros p q r. rewrite !Qp_to_Qc_inj_le. by etrans. + - intros p q. rewrite !Qp_to_Qc_inj_le, <-Qp_to_Qc_inj_iff. apply Qcle_antisym. Qed. Instance Qp_lt_strict : StrictOrder (<)%Qp. Proof. - unfold Qp_lt. split. - - intros p. apply (irreflexivity (<)%Qc). - - intros p q r ??. by etrans. + split. + - intros p ?%Qp_to_Qc_inj_lt. by apply (irreflexivity (<)%Qc (Qp_to_Qc p)). + - intros p q r. rewrite !Qp_to_Qc_inj_lt. by etrans. Qed. Instance Qp_le_total: Total (≤)%Qp. -Proof. intros p q. apply (total Qcle). Qed. +Proof. intros p q. rewrite !Qp_to_Qc_inj_le. apply (total Qcle). Qed. Lemma Qp_lt_le_weak p q : p < q → p ≤ q. -Proof. apply Qclt_le_weak. Qed. +Proof. rewrite Qp_to_Qc_inj_lt, Qp_to_Qc_inj_le. apply Qclt_le_weak. Qed. Lemma Qp_le_lt_or_eq p q : p ≤ q → p < q ∨ p = q. -Proof. intros [? | ->%Qp_to_Qc_inj_iff]%Qcle_lt_or_eq; auto. Qed. +Proof. + rewrite Qp_to_Qc_inj_lt, Qp_to_Qc_inj_le. + intros [? | ->%Qp_to_Qc_inj_iff]%Qcle_lt_or_eq; auto. +Qed. Lemma Qp_lt_le_dec p q : {p < q} + {q ≤ p}. -Proof. apply Qclt_le_dec. Defined. +Proof. + refine (cast_if (Qclt_le_dec (Qp_to_Qc p) (Qp_to_Qc q)%Qc)); + [by apply Qp_to_Qc_inj_lt|by apply Qp_to_Qc_inj_le]. +Defined. Lemma Qp_le_lt_trans p q r : p ≤ q → q < r → p < r. -Proof. apply Qcle_lt_trans. Qed. +Proof. rewrite !Qp_to_Qc_inj_lt, Qp_to_Qc_inj_le. apply Qcle_lt_trans. Qed. Lemma Qp_lt_le_trans p q r : p < q → q ≤ r → p < r. -Proof. apply Qclt_le_trans. Qed. +Proof. rewrite !Qp_to_Qc_inj_lt, Qp_to_Qc_inj_le. apply Qclt_le_trans. Qed. Lemma Qp_le_not_lt p q : p ≤ q → ¬q < p. -Proof. apply Qcle_not_lt. Qed. +Proof. rewrite !Qp_to_Qc_inj_lt, Qp_to_Qc_inj_le. apply Qcle_not_lt. Qed. Lemma Qp_not_lt_le p q : ¬p < q → q ≤ p. -Proof. apply Qcnot_lt_le. Qed. +Proof. rewrite !Qp_to_Qc_inj_lt, Qp_to_Qc_inj_le. apply Qcnot_lt_le. Qed. Lemma Qp_lt_not_le p q : p < q → ¬q ≤ p. -Proof. apply Qclt_not_le. Qed. +Proof. rewrite !Qp_to_Qc_inj_lt, Qp_to_Qc_inj_le. apply Qclt_not_le. Qed. Lemma Qp_not_le_lt p q : ¬p ≤ q →q < p. -Proof. apply Qcnot_le_lt. Qed. +Proof. rewrite !Qp_to_Qc_inj_lt, Qp_to_Qc_inj_le. apply Qcnot_le_lt. Qed. Lemma Qp_le_ngt p q : p ≤ q ↔ ¬q < p. Proof. split; auto using Qp_le_not_lt, Qp_not_lt_le. Qed. Lemma Qp_lt_nge p q : p < q ↔ ¬q ≤ p. Proof. split; auto using Qp_lt_not_le, Qp_not_le_lt. Qed. Lemma Qp_plus_le_mono_l p q r : p ≤ q ↔ r + p ≤ r + q. -Proof. destruct p, q, r; apply Qcplus_le_mono_l. Qed. +Proof. rewrite !Qp_to_Qc_inj_le. destruct p, q, r; apply Qcplus_le_mono_l. Qed. Lemma Qp_plus_le_mono_r p q r : p ≤ q ↔ p + r ≤ q + r. Proof. rewrite !(comm_L Qp_plus _ r). apply Qp_plus_le_mono_l. Qed. Lemma Qp_le_plus_compat q p n m : q ≤ n → p ≤ m → q + p ≤ n + m. @@ -853,17 +872,22 @@ Lemma Qp_plus_lt_mono_r p q r : p < q ↔ p + r < q + r. Proof. by rewrite !Qp_lt_nge, <-Qp_plus_le_mono_r. Qed. Lemma Qp_mult_le_mono_l p q r : p ≤ q ↔ r * p ≤ r * q. -Proof. destruct p, q, r; by apply Qcmult_le_mono_pos_l. Qed. +Proof. + rewrite !Qp_to_Qc_inj_le. destruct p, q, r; by apply Qcmult_le_mono_pos_l. +Qed. Lemma Qp_mult_le_mono_r p q r : p ≤ q ↔ p * r ≤ q * r. -Proof. destruct p, q, r; by apply Qcmult_le_mono_pos_r. Qed. +Proof. rewrite !(comm_L Qp_mult _ r). apply Qp_mult_le_mono_l. Qed. + Lemma Qcmult_lt_mono_l p q r : p < q ↔ r * p < r * q. -Proof. destruct p, q, r; by apply Qcmult_lt_mono_pos_l. Qed. +Proof. + rewrite !Qp_to_Qc_inj_lt. destruct p, q, r; by apply Qcmult_lt_mono_pos_l. +Qed. Lemma Qcmult_lt_mono_r p q r : p < q ↔ p * r < q * r. -Proof. destruct p, q, r; by apply Qcmult_lt_mono_pos_r. Qed. +Proof. rewrite !(comm_L Qp_mult _ r). apply Qcmult_lt_mono_l. Qed. Lemma Qp_lt_plus_r q p : p < q + p. Proof. - destruct p as [p ?], q as [q ?]. unfold Qp_lt; simpl. + destruct p as [p ?], q as [q ?]. apply Qp_to_Qc_inj_lt; simpl. rewrite <- (Qcplus_0_l p) at 1. by rewrite <-Qcplus_lt_mono_r. Qed. Lemma Qp_lt_plus_l q p : q < q + p. @@ -902,7 +926,7 @@ Proof. Qed. Lemma Qp_lt_sum p q : p < q ↔ ∃ r, q = p + r. Proof. - destruct p as [p Hp], q as [q Hq]. unfold Qp_lt; simpl. + 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. @@ -923,7 +947,7 @@ Proof. by apply Qc_minus_Some. Qed. Lemma Qp_div_lt q y : (1 < y)%positive → q / y < q. Proof. - intros. destruct q as [q Hq]. unfold Qp_lt, Qp_minus; simpl. + intros. destruct q as [q Hq]. apply Qp_to_Qc_inj_lt; unfold Qp_minus; simpl. apply (Qcmult_lt_mono_pos_l _ _ (Z.pos y)); [done|]. rewrite Qcmult_div_r by done. rewrite <- (Qcmult_1_l q) at 1. apply Qcmult_lt_mono_pos_r; [done|]. by rewrite <-Z2Qc_inj_1, <-Z2Qc_inj_lt. -- GitLab From 2e4d59de1d6309bc60ecd99db14a3058b536e820 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Sat, 3 Oct 2020 13:16:03 +0200 Subject: [PATCH 04/12] Define `Qp_inv`, and generalize `Qp_div` so both arguments range over `Qp`. Moreover, and suitable lemmas. --- theories/numbers.v | 138 ++++++++++++++++++++++++++++++++++----------- 1 file changed, 105 insertions(+), 33 deletions(-) diff --git a/theories/numbers.v b/theories/numbers.v index d510e52a..416d11d1 100644 --- a/theories/numbers.v +++ b/theories/numbers.v @@ -627,6 +627,12 @@ Proof. by apply Qcmult_le_mono_nonneg_r. Qed. +Lemma Qcinv_pos x : 0 < x → 0 < /x. +Proof. + intros. assert (0 ≠ x) by (by apply Qclt_not_eq). + by rewrite (Qcmult_lt_mono_pos_r _ _ x), Qcmult_0_l, Qcmult_inv_l by done. +Qed. + Lemma inject_Z_Qred n : Qred (inject_Z n) = inject_Z n. Proof. apply Qred_identity; auto using Z.gcd_1_r. Qed. Coercion Qc_of_Z (n : Z) : Qc := Qcmake _ (inject_Z_Qred n). @@ -697,21 +703,21 @@ Definition Qp_mult (p q : Qp) : Qp := mk_Qp (p * q) (Qcmult_pos_pos _ _ Hp Hq). Arguments Qp_mult : simpl never. -Program Definition Qp_div (p : Qp) (y : positive) : Qp := - let 'mk_Qp p Hp := p return _ in - mk_Qp (p / Zpos y)%Qc _. -Next Obligation. - intros _ y p Hp. unfold Qcdiv. assert (0 < Zpos y)%Qc. - { apply (Z2Qc_inj_lt 0%Z (Zpos y)), Pos2Z.is_pos. } - by rewrite (Qcmult_lt_mono_pos_r _ _ (Zpos y)%Z), Qcmult_0_l, - <-Qcmult_assoc, Qcmult_inv_l, Qcmult_1_r. -Qed. +Definition Qp_inv (q : Qp) : Qp := + let 'mk_Qp q Hq := q return _ in + mk_Qp (/ q)%Qc (Qcinv_pos _ Hq). +Arguments Qp_inv : simpl never. + +Definition Qp_div (p q : Qp) : Qp := Qp_mult p (Qp_inv q). +Typeclasses Opaque Qp_div. Arguments Qp_div : simpl never. Infix "+" := Qp_plus : Qp_scope. Infix "-" := Qp_minus : Qp_scope. Infix "*" := Qp_mult : Qp_scope. +Notation "/ q" := (Qp_inv q) : Qp_scope. Infix "/" := Qp_div : Qp_scope. + Notation "1" := Qp_one : Qp_scope. Notation "2" := (1 + 1)%Qp : Qp_scope. Notation "3" := (1 + 2)%Qp : Qp_scope. @@ -769,7 +775,7 @@ Proof. destruct p as [p ?]. intros [q1 ?] [q2 ?]. rewrite <-!Qp_to_Qc_inj_iff; simpl. apply (inj (Qcplus p)). Qed. -Instance Qp_plus_inj_l p : Inj (=) (=) (λ q, q + p)%Qp. +Instance Qp_plus_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). @@ -779,6 +785,17 @@ Instance Qp_mult_assoc : Assoc (=) Qp_mult. Proof. intros [p ?] [q ?] [r ?]. apply Qp_to_Qc_inj_iff, Qcmult_assoc. Qed. Instance Qp_mult_comm : Comm (=) Qp_mult. Proof. intros [p ?] [q ?]; apply Qp_to_Qc_inj_iff, Qcmult_comm. Qed. +Instance Qp_mult_inj_r p : Inj (=) (=) (Qp_mult p). +Proof. + destruct p as [p ?]. intros [q1 ?] [q2 ?]. rewrite <-!Qp_to_Qc_inj_iff; simpl. + intros Hpq. + apply (anti_symm _); apply (Qcmult_le_mono_pos_l _ _ p); by rewrite ?Hpq. +Qed. +Instance Qp_mult_inj_l p : Inj (=) (=) (λ q, q * p). +Proof. + intros q1 q2 Hpq. apply (inj (Qp_mult p)). by rewrite !(comm_L Qp_mult p). +Qed. + Lemma Qp_mult_plus_distr_r 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. Lemma Qp_mult_plus_distr_l p q r : (p + q) * r = p * r + q * r. @@ -791,27 +808,70 @@ Proof. destruct p; apply Qp_to_Qc_inj_iff, Qcmult_1_r. Qed. Lemma Qp_plus_diag p : p + p = (2 * p). Proof. by rewrite Qp_mult_plus_distr_l, !Qp_mult_1_l. Qed. -Lemma Qp_div_1 p : p / 1 = p. +Lemma Qp_mult_inv_l p : /p * p = 1. Proof. - destruct p as [p ?]. apply Qp_to_Qc_inj_iff; simpl. - rewrite <-(Qcmult_div_r p 1) at 2 by done. by rewrite Qcmult_1_l. + destruct p as [p ?]. + by apply Qp_to_Qc_inj_iff, Qcmult_inv_l, not_symmetry, Qclt_not_eq. Qed. -Lemma Qp_div_S p y : p / (2 * y) + p / (2 * y) = p / y. +Lemma Qp_mult_inv_r p : p * /p = 1. +Proof. by rewrite (comm_L Qp_mult), Qp_mult_inv_l. Qed. +Lemma Qp_inv_mult_distr p q : /(p * q) = /p * /q. Proof. - destruct p as [p ?]. apply Qp_to_Qc_inj_iff; simpl. unfold Qcdiv. - rewrite <-Qcmult_plus_distr_l, Pos2Z.inj_mul, Z2Qc_inj_mul, Z2Qc_inj_2. - rewrite Qcplus_diag. by field_simplify. + apply (inj (Qp_mult (p * q))). + rewrite Qp_mult_inv_r, (comm_L Qp_mult p), <-(assoc_L _), (assoc_L Qp_mult p). + by rewrite Qp_mult_inv_r, Qp_mult_1_l, Qp_mult_inv_r. Qed. +Lemma Qp_inv_involutive p : / /p = p. +Proof. + rewrite <-(Qp_mult_1_l (/ /p)), <-(Qp_mult_inv_r p), <-(assoc_L _). + by rewrite Qp_mult_inv_r, Qp_mult_1_r. +Qed. +Instance Qp_inv_inj : Inj (=) (=) Qp_inv. +Proof. + intros p1 p2 Hp. apply (inj (Qp_mult (/p1))). + by rewrite Qp_mult_inv_l, Hp, Qp_mult_inv_l. +Qed. +Lemma Qp_inv_1 : /1 = 1. +Proof. apply (bool_decide_unpack _); by compute. Qed. +Lemma Qp_inv_half_half : /2 + /2 = 1. +Proof. apply (bool_decide_unpack _); by compute. Qed. + +Lemma Qp_div_diag p : p / p = 1. +Proof. apply Qp_mult_inv_r. Qed. +Lemma Qp_mult_div_l p q : (p / q) * q = p. +Proof. unfold Qp_div. by rewrite <-(assoc_L _), Qp_mult_inv_l, Qp_mult_1_r. Qed. +Lemma Qp_mult_div_r p q : q * (p / q) = p. +Proof. by rewrite (comm_L Qp_mult q), Qp_mult_div_l. Qed. +Lemma Qp_div_plus_distr p q r : (p + q) / r = p / r + q / r. +Proof. apply Qp_mult_plus_distr_l. Qed. +Lemma Qp_div_div p q r : (p / q) / r = p / (q * r). +Proof. unfold Qp_div. by rewrite Qp_inv_mult_distr, (assoc_L _). Qed. +Lemma Qp_div_mult_cancel_l p q r : (r * p) / (r * q) = p / q. +Proof. + rewrite <-Qp_div_div. f_equiv. unfold Qp_div. + by rewrite (comm_L Qp_mult r), <-(assoc_L _), Qp_mult_inv_r, Qp_mult_1_r. +Qed. +Lemma Qp_div_mult_cancel_r p q r : (p * r) / (q * r) = p / q. +Proof. by rewrite <-!(comm_L Qp_mult r), Qp_div_mult_cancel_l. Qed. +Lemma Qp_div_1 p : p / 1 = p. +Proof. by rewrite <-(Qp_mult_1_r (p / 1)), Qp_mult_div_l. Qed. Lemma Qp_div_2 p : p / 2 + p / 2 = p. Proof. - change 2%positive with (2 * 1)%positive. by rewrite Qp_div_S, Qp_div_1. + rewrite <-Qp_div_plus_distr, Qp_plus_diag. + rewrite <-(Qp_mult_1_r 2) at 2. by rewrite Qp_div_mult_cancel_l, Qp_div_1. Qed. +Lemma Qp_div_S p q : p / (2 * q) + p / (2 * q) = p / q. +Proof. by rewrite <-Qp_div_plus_distr, Qp_plus_diag, Qp_div_mult_cancel_l. Qed. Lemma Qp_half_half : 1 / 2 + 1 / 2 = 1. Proof. apply (bool_decide_unpack _); by compute. Qed. Lemma Qp_quarter_three_quarter : 1 / 4 + 3 / 4 = 1. Proof. apply (bool_decide_unpack _); by compute. Qed. Lemma Qp_three_quarter_quarter : 3 / 4 + 1 / 4 = 1. Proof. apply (bool_decide_unpack _); by compute. Qed. +Instance Qp_div_inj_r p : Inj (=) (=) (Qp_div p). +Proof. unfold Qp_div; apply _. Qed. +Instance Qp_div_inj_l p : Inj (=) (=) (λ q, q / p)%Qp. +Proof. unfold Qp_div; apply _. Qed. Instance Qp_le_po : PartialOrder (≤)%Qp. Proof. @@ -878,12 +938,12 @@ Qed. Lemma Qp_mult_le_mono_r p q r : p ≤ q ↔ p * r ≤ q * r. Proof. rewrite !(comm_L Qp_mult _ r). apply Qp_mult_le_mono_l. Qed. -Lemma Qcmult_lt_mono_l p q r : p < q ↔ r * p < r * q. +Lemma Qp_mult_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. Qed. -Lemma Qcmult_lt_mono_r p q r : p < q ↔ p * r < q * r. -Proof. rewrite !(comm_L Qp_mult _ r). apply Qcmult_lt_mono_l. Qed. +Lemma Qp_mult_lt_mono_r p q r : p < q ↔ p * r < q * r. +Proof. rewrite !(comm_L Qp_mult _ r). apply Qp_mult_lt_mono_l. Qed. Lemma Qp_lt_plus_r q p : p < q + p. Proof. @@ -945,19 +1005,31 @@ Proof. by apply Qc_minus_None. Qed. Lemma Qp_plus_minus p q : (p + q) - p = Some q. Proof. by apply Qc_minus_Some. Qed. -Lemma Qp_div_lt q y : (1 < y)%positive → q / y < q. -Proof. - intros. destruct q as [q Hq]. apply Qp_to_Qc_inj_lt; unfold Qp_minus; simpl. - apply (Qcmult_lt_mono_pos_l _ _ (Z.pos y)); [done|]. - rewrite Qcmult_div_r by done. rewrite <- (Qcmult_1_l q) at 1. - apply Qcmult_lt_mono_pos_r; [done|]. by rewrite <-Z2Qc_inj_1, <-Z2Qc_inj_lt. -Qed. -Lemma Qp_div_le q y : q / y ≤ q. +Lemma Qp_inv_lt_mono p q : p < q ↔ /q < /p. Proof. - destruct (Pos.lt_total y 1) as [[]%Pos.nlt_1_r|[->|?]]. - - by rewrite Qp_div_1. - - by apply Qp_lt_le_weak, Qp_div_lt. + revert p q. cut (∀ p q, p < q → / q < / p). + { intros help p q. split; [apply help|]. intros. + rewrite <-(Qp_inv_involutive p), <-(Qp_inv_involutive q). by apply help. } + intros p q Hpq. apply (Qp_mult_lt_mono_l _ _ q). rewrite Qp_mult_inv_r. + apply (Qp_mult_lt_mono_r _ _ p). rewrite <-(assoc_L _), Qp_mult_inv_l. + by rewrite Qp_mult_1_l, Qp_mult_1_r. Qed. +Lemma Qp_inv_le_mono p q : p ≤ q ↔ /q ≤ /p. +Proof. by rewrite !Qp_le_ngt, Qp_inv_lt_mono. Qed. + +Lemma Qp_div_le_mono_l p q r : q ≤ p ↔ r / p ≤ r / q. +Proof. unfold Qp_div. by rewrite <-Qp_mult_le_mono_l, Qp_inv_le_mono. Qed. +Lemma Qp_div_le_mono_r p q r : p ≤ q ↔ p / r ≤ q / r. +Proof. apply Qp_mult_le_mono_r. Qed. +Lemma Qp_div_lt_mono_l p q r : q < p ↔ r / p < r / q. +Proof. unfold Qp_div. by rewrite <-Qp_mult_lt_mono_l, Qp_inv_lt_mono. Qed. +Lemma Qp_div_lt_mono_r p q r : p < q ↔ p / r < q / r. +Proof. apply Qp_mult_lt_mono_r. Qed. + +Lemma Qp_div_lt p q : 1 < q → p / q < p. +Proof. by rewrite (Qp_div_lt_mono_l _ _ p), Qp_div_1. Qed. +Lemma Qp_div_le p q : 1 ≤ q → p / q ≤ p. +Proof. by rewrite (Qp_div_le_mono_l _ _ p), Qp_div_1. Qed. Lemma Qp_lower_bound q1 q2 : ∃ q q1' q2', q1 = q + q1' ∧ q2 = q + q2'. Proof. @@ -1004,7 +1076,7 @@ Proof. destruct (Qp_lt_le_dec r p) as [[q ->]%Qp_lt_sum|?]. { by exists r, q. } exists (p / 2)%Qp, (p / 2)%Qp; split. - + trans p; [|done]. apply Qp_div_le. + + trans p; [|done]. by apply Qp_div_le. + by rewrite Qp_div_2. Qed. -- GitLab From b2903d4f332d4bda4694f500421e982092561eed Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Sat, 3 Oct 2020 13:33:17 +0200 Subject: [PATCH 05/12] 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 From da606ab124e00e243ca8e55580b2acc2d1db1565 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Sat, 3 Oct 2020 14:18:04 +0200 Subject: [PATCH 06/12] Define `Qp` numerals in terms of `pos_to_Qp`. --- theories/numbers.v | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/theories/numbers.v b/theories/numbers.v index 491d4522..20a835ca 100644 --- a/theories/numbers.v +++ b/theories/numbers.v @@ -685,8 +685,6 @@ Proof. by rewrite <-Qp_to_Qc_inj_iff. Defined. -Definition Qp_one : Qp := mk_Qp 1 eq_refl. - Definition Qp_plus (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). @@ -718,10 +716,14 @@ Infix "*" := Qp_mult : Qp_scope. Notation "/ q" := (Qp_inv q) : Qp_scope. Infix "/" := Qp_div : Qp_scope. -Notation "1" := Qp_one : Qp_scope. -Notation "2" := (1 + 1)%Qp : Qp_scope. -Notation "3" := (1 + 2)%Qp : Qp_scope. -Notation "4" := (1 + 3)%Qp : 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. + +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. @@ -764,10 +766,6 @@ 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. @@ -809,13 +807,15 @@ Proof. destruct p; apply Qp_to_Qc_inj_iff, Qcmult_1_l. Qed. Lemma Qp_mult_1_r p : p * 1 = p. Proof. destruct p; apply Qp_to_Qc_inj_iff, Qcmult_1_r. Qed. +Lemma Qp_one_one : 1 + 1 = 2. +Proof. apply (bool_decide_unpack _); by compute. Qed. Lemma Qp_plus_diag p : p + p = (2 * p). -Proof. by rewrite Qp_mult_plus_distr_l, !Qp_mult_1_l. Qed. +Proof. by rewrite <-Qp_one_one, Qp_mult_plus_distr_l, !Qp_mult_1_l. Qed. Lemma Qp_mult_inv_l p : /p * p = 1. Proof. - destruct p as [p ?]. - by apply Qp_to_Qc_inj_iff, Qcmult_inv_l, not_symmetry, Qclt_not_eq. + 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). Qed. Lemma Qp_mult_inv_r p : p * /p = 1. Proof. by rewrite (comm_L Qp_mult), Qp_mult_inv_l. Qed. -- GitLab From a30f6ade1667018b8e33aaf16b4ec51901ce3e0d Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Tue, 6 Oct 2020 21:28:04 +0200 Subject: [PATCH 07/12] =?UTF-8?q?Rename=20`Qp=5Fplus`=20=E2=86=92=20`Qp=5F?= =?UTF-8?q?add`,=20`Qp=5Fmult`=20=E2=86=92=20`Qp=5Fmul`,=20and=20`Qp=5Fmin?= =?UTF-8?q?us`=20=E2=86=92=20`Qp=5Fsub`.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- theories/numbers.v | 220 ++++++++++++++++++++++----------------------- 1 file changed, 110 insertions(+), 110 deletions(-) diff --git a/theories/numbers.v b/theories/numbers.v index 20a835ca..e55811ea 100644 --- a/theories/numbers.v +++ b/theories/numbers.v @@ -685,34 +685,34 @@ Proof. by rewrite <-Qp_to_Qc_inj_iff. Defined. -Definition Qp_plus (p q : Qp) : Qp := +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). -Arguments Qp_plus : simpl never. +Arguments Qp_add : simpl never. -Definition Qp_minus (p q : Qp) : option Qp := +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). -Arguments Qp_minus : simpl never. +Arguments Qp_sub : simpl never. -Definition Qp_mult (p q : Qp) : Qp := +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). -Arguments Qp_mult : simpl never. +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). Arguments Qp_inv : simpl never. -Definition Qp_div (p q : Qp) : Qp := Qp_mult p (Qp_inv q). +Definition Qp_div (p q : Qp) : Qp := Qp_mul p (Qp_inv q). Typeclasses Opaque Qp_div. Arguments Qp_div : simpl never. -Infix "+" := Qp_plus : Qp_scope. -Infix "-" := Qp_minus : Qp_scope. -Infix "*" := Qp_mult : Qp_scope. +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. @@ -768,72 +768,72 @@ Infix "`min`" := Qp_min : Qp_scope. Instance Qp_inhabited : Inhabited Qp := populate 1. -Instance Qp_plus_assoc : Assoc (=) Qp_plus. +Instance Qp_add_assoc : Assoc (=) Qp_add. Proof. intros [p ?] [q ?] [r ?]; apply Qp_to_Qc_inj_iff, Qcplus_assoc. Qed. -Instance Qp_plus_comm : Comm (=) Qp_plus. +Instance Qp_add_comm : Comm (=) Qp_add. Proof. intros [p ?] [q ?]; apply Qp_to_Qc_inj_iff, Qcplus_comm. Qed. -Instance Qp_plus_inj_r p : Inj (=) (=) (Qp_plus p). +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)). Qed. -Instance Qp_plus_inj_l p : Inj (=) (=) (λ q, q + p). +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). Qed. -Instance Qp_mult_assoc : Assoc (=) Qp_mult. +Instance Qp_mul_assoc : Assoc (=) Qp_mul. Proof. intros [p ?] [q ?] [r ?]. apply Qp_to_Qc_inj_iff, Qcmult_assoc. Qed. -Instance Qp_mult_comm : Comm (=) Qp_mult. +Instance Qp_mul_comm : Comm (=) Qp_mul. Proof. intros [p ?] [q ?]; apply Qp_to_Qc_inj_iff, Qcmult_comm. Qed. -Instance Qp_mult_inj_r p : Inj (=) (=) (Qp_mult p). +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 Hpq. apply (anti_symm _); apply (Qcmult_le_mono_pos_l _ _ p); by rewrite ?Hpq. Qed. -Instance Qp_mult_inj_l p : Inj (=) (=) (λ q, q * p). +Instance Qp_mul_inj_l p : Inj (=) (=) (λ q, q * p). Proof. - intros q1 q2 Hpq. apply (inj (Qp_mult p)). by rewrite !(comm_L Qp_mult p). + intros q1 q2 Hpq. apply (inj (Qp_mul p)). by rewrite !(comm_L Qp_mul p). Qed. -Lemma Qp_mult_plus_distr_r p q r : p * (q + r) = p * q + p * r. +Lemma Qp_mul_add_distr_r 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. -Lemma Qp_mult_plus_distr_l p q r : (p + q) * r = p * r + q * r. +Lemma Qp_mul_add_distr_l 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. -Lemma Qp_mult_1_l p : 1 * p = p. +Lemma Qp_mul_1_l p : 1 * p = p. Proof. destruct p; apply Qp_to_Qc_inj_iff, Qcmult_1_l. Qed. -Lemma Qp_mult_1_r p : p * 1 = p. +Lemma Qp_mul_1_r p : p * 1 = p. Proof. destruct p; apply Qp_to_Qc_inj_iff, Qcmult_1_r. Qed. Lemma Qp_one_one : 1 + 1 = 2. Proof. apply (bool_decide_unpack _); by compute. Qed. -Lemma Qp_plus_diag p : p + p = (2 * p). -Proof. by rewrite <-Qp_one_one, Qp_mult_plus_distr_l, !Qp_mult_1_l. Qed. +Lemma Qp_add_diag p : p + p = (2 * p). +Proof. by rewrite <-Qp_one_one, Qp_mul_add_distr_l, !Qp_mul_1_l. Qed. -Lemma Qp_mult_inv_l p : /p * p = 1. +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). Qed. -Lemma Qp_mult_inv_r p : p * /p = 1. -Proof. by rewrite (comm_L Qp_mult), Qp_mult_inv_l. Qed. -Lemma Qp_inv_mult_distr p q : /(p * q) = /p * /q. +Lemma Qp_mul_inv_r p : p * /p = 1. +Proof. by rewrite (comm_L Qp_mul), Qp_mul_inv_l. Qed. +Lemma Qp_inv_mul_distr p q : /(p * q) = /p * /q. Proof. - apply (inj (Qp_mult (p * q))). - rewrite Qp_mult_inv_r, (comm_L Qp_mult p), <-(assoc_L _), (assoc_L Qp_mult p). - by rewrite Qp_mult_inv_r, Qp_mult_1_l, Qp_mult_inv_r. + apply (inj (Qp_mul (p * q))). + rewrite Qp_mul_inv_r, (comm_L Qp_mul p), <-(assoc_L _), (assoc_L Qp_mul p). + by rewrite Qp_mul_inv_r, Qp_mul_1_l, Qp_mul_inv_r. Qed. Lemma Qp_inv_involutive p : / /p = p. Proof. - rewrite <-(Qp_mult_1_l (/ /p)), <-(Qp_mult_inv_r p), <-(assoc_L _). - by rewrite Qp_mult_inv_r, Qp_mult_1_r. + rewrite <-(Qp_mul_1_l (/ /p)), <-(Qp_mul_inv_r p), <-(assoc_L _). + by rewrite Qp_mul_inv_r, Qp_mul_1_r. Qed. Instance Qp_inv_inj : Inj (=) (=) Qp_inv. Proof. - intros p1 p2 Hp. apply (inj (Qp_mult (/p1))). - by rewrite Qp_mult_inv_l, Hp, Qp_mult_inv_l. + intros p1 p2 Hp. apply (inj (Qp_mul (/p1))). + by rewrite Qp_mul_inv_l, Hp, Qp_mul_inv_l. Qed. Lemma Qp_inv_1 : /1 = 1. Proof. apply (bool_decide_unpack _); by compute. Qed. @@ -841,31 +841,31 @@ Lemma Qp_inv_half_half : /2 + /2 = 1. Proof. apply (bool_decide_unpack _); by compute. Qed. Lemma Qp_div_diag p : p / p = 1. -Proof. apply Qp_mult_inv_r. Qed. -Lemma Qp_mult_div_l p q : (p / q) * q = p. -Proof. unfold Qp_div. by rewrite <-(assoc_L _), Qp_mult_inv_l, Qp_mult_1_r. Qed. -Lemma Qp_mult_div_r p q : q * (p / q) = p. -Proof. by rewrite (comm_L Qp_mult q), Qp_mult_div_l. Qed. -Lemma Qp_div_plus_distr p q r : (p + q) / r = p / r + q / r. -Proof. apply Qp_mult_plus_distr_l. Qed. +Proof. apply Qp_mul_inv_r. Qed. +Lemma Qp_mul_div_l p q : (p / q) * q = p. +Proof. unfold Qp_div. by rewrite <-(assoc_L _), Qp_mul_inv_l, Qp_mul_1_r. Qed. +Lemma Qp_mul_div_r p q : q * (p / q) = p. +Proof. by rewrite (comm_L Qp_mul q), Qp_mul_div_l. Qed. +Lemma Qp_div_add_distr p q r : (p + q) / r = p / r + q / r. +Proof. apply Qp_mul_add_distr_l. Qed. Lemma Qp_div_div p q r : (p / q) / r = p / (q * r). -Proof. unfold Qp_div. by rewrite Qp_inv_mult_distr, (assoc_L _). Qed. -Lemma Qp_div_mult_cancel_l p q r : (r * p) / (r * q) = p / q. +Proof. unfold Qp_div. by rewrite Qp_inv_mul_distr, (assoc_L _). Qed. +Lemma Qp_div_mul_cancel_l p q r : (r * p) / (r * q) = p / q. Proof. rewrite <-Qp_div_div. f_equiv. unfold Qp_div. - by rewrite (comm_L Qp_mult r), <-(assoc_L _), Qp_mult_inv_r, Qp_mult_1_r. + by rewrite (comm_L Qp_mul r), <-(assoc_L _), Qp_mul_inv_r, Qp_mul_1_r. Qed. -Lemma Qp_div_mult_cancel_r p q r : (p * r) / (q * r) = p / q. -Proof. by rewrite <-!(comm_L Qp_mult r), Qp_div_mult_cancel_l. Qed. +Lemma Qp_div_mul_cancel_r p q r : (p * r) / (q * r) = p / q. +Proof. by rewrite <-!(comm_L Qp_mul r), Qp_div_mul_cancel_l. Qed. Lemma Qp_div_1 p : p / 1 = p. -Proof. by rewrite <-(Qp_mult_1_r (p / 1)), Qp_mult_div_l. Qed. +Proof. by rewrite <-(Qp_mul_1_r (p / 1)), Qp_mul_div_l. Qed. Lemma Qp_div_2 p : p / 2 + p / 2 = p. Proof. - rewrite <-Qp_div_plus_distr, Qp_plus_diag. - rewrite <-(Qp_mult_1_r 2) at 2. by rewrite Qp_div_mult_cancel_l, Qp_div_1. + rewrite <-Qp_div_add_distr, Qp_add_diag. + rewrite <-(Qp_mul_1_r 2) at 2. by rewrite Qp_div_mul_cancel_l, Qp_div_1. Qed. Lemma Qp_div_S p q : p / (2 * q) + p / (2 * q) = p / q. -Proof. by rewrite <-Qp_div_plus_distr, Qp_plus_diag, Qp_div_mult_cancel_l. Qed. +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. apply (bool_decide_unpack _); by compute. Qed. Lemma Qp_quarter_three_quarter : 1 / 4 + 3 / 4 = 1. @@ -923,64 +923,64 @@ Proof. split; auto using Qp_le_not_lt, Qp_not_lt_le. Qed. Lemma Qp_lt_nge p q : p < q ↔ ¬q ≤ p. Proof. split; auto using Qp_lt_not_le, Qp_not_le_lt. Qed. -Lemma Qp_plus_le_mono_l p q r : p ≤ q ↔ r + p ≤ r + q. +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. -Lemma Qp_plus_le_mono_r p q r : p ≤ q ↔ p + r ≤ q + r. -Proof. rewrite !(comm_L Qp_plus _ r). apply Qp_plus_le_mono_l. Qed. -Lemma Qp_le_plus_compat q p n m : q ≤ n → p ≤ m → q + p ≤ n + m. -Proof. intros. etrans; [by apply Qp_plus_le_mono_l|by apply Qp_plus_le_mono_r]. 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_le_add_compat q p n m : q ≤ n → p ≤ m → q + p ≤ n + m. +Proof. intros. etrans; [by apply Qp_add_le_mono_l|by apply Qp_add_le_mono_r]. Qed. -Lemma Qp_plus_lt_mono_l p q r : p < q ↔ r + p < r + q. -Proof. by rewrite !Qp_lt_nge, <-Qp_plus_le_mono_l. Qed. -Lemma Qp_plus_lt_mono_r p q r : p < q ↔ p + r < q + r. -Proof. by rewrite !Qp_lt_nge, <-Qp_plus_le_mono_r. Qed. +Lemma Qp_add_lt_mono_l p q r : p < q ↔ r + p < r + q. +Proof. by rewrite !Qp_lt_nge, <-Qp_add_le_mono_l. Qed. +Lemma Qp_add_lt_mono_r p q r : p < q ↔ p + r < q + r. +Proof. by rewrite !Qp_lt_nge, <-Qp_add_le_mono_r. Qed. -Lemma Qp_mult_le_mono_l p q r : p ≤ q ↔ r * p ≤ r * q. +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. Qed. -Lemma Qp_mult_le_mono_r p q r : p ≤ q ↔ p * r ≤ q * r. -Proof. rewrite !(comm_L Qp_mult _ r). apply Qp_mult_le_mono_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. -Lemma Qp_mult_lt_mono_l p q r : p < q ↔ r * p < r * q. +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. Qed. -Lemma Qp_mult_lt_mono_r p q r : p < q ↔ p * r < q * r. -Proof. rewrite !(comm_L Qp_mult _ r). apply Qp_mult_lt_mono_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. -Lemma Qp_lt_plus_r q p : p < q + p. +Lemma Qp_lt_add_r q p : p < q + p. Proof. destruct p as [p ?], q as [q ?]. apply Qp_to_Qc_inj_lt; simpl. rewrite <- (Qcplus_0_l p) at 1. by rewrite <-Qcplus_lt_mono_r. Qed. -Lemma Qp_lt_plus_l q p : q < q + p. -Proof. rewrite (comm_L Qp_plus). apply Qp_lt_plus_r. Qed. +Lemma Qp_lt_add_l q p : q < q + p. +Proof. rewrite (comm_L Qp_add). apply Qp_lt_add_r. Qed. -Lemma Qp_not_plus_ge q p : ¬(q + p ≤ q). -Proof. apply Qp_lt_not_le, Qp_lt_plus_l. Qed. -Lemma Qp_plus_id_free q p : q + p ≠ q. -Proof. intro Heq. apply (Qp_not_plus_ge q p). by rewrite Heq. Qed. +Lemma Qp_not_add_ge q p : ¬(q + p ≤ q). +Proof. apply Qp_lt_not_le, Qp_lt_add_l. Qed. +Lemma Qp_add_id_free q p : q + p ≠ q. +Proof. intro Heq. apply (Qp_not_add_ge q p). by rewrite Heq. Qed. -Lemma Qp_le_plus_r q p : p ≤ q + p. -Proof. apply Qp_lt_le_weak, Qp_lt_plus_r. Qed. -Lemma Qp_le_plus_l q p : q ≤ q + p. -Proof. apply Qp_lt_le_weak, Qp_lt_plus_l. Qed. +Lemma Qp_le_add_r q p : p ≤ q + p. +Proof. apply Qp_lt_le_weak, Qp_lt_add_r. Qed. +Lemma Qp_le_add_l q p : q ≤ q + p. +Proof. apply Qp_lt_le_weak, Qp_lt_add_l. Qed. -Lemma Qp_plus_weak_r q p o : q + p ≤ o → q ≤ o. -Proof. intros. etrans; [apply Qp_le_plus_l|done]. Qed. -Lemma Qp_plus_weak_l q p o : q + p ≤ o → p ≤ o. -Proof. rewrite (comm_L Qp_plus). apply Qp_plus_weak_r. Qed. +Lemma Qp_add_weak_r q p o : q + p ≤ o → q ≤ o. +Proof. intros. etrans; [apply Qp_le_add_l|done]. Qed. +Lemma Qp_add_weak_l q p o : q + p ≤ o → p ≤ o. +Proof. rewrite (comm_L Qp_add). apply Qp_add_weak_r. Qed. -Lemma Qp_plus_weak_2_r q p o : q ≤ o → q ≤ p + o. -Proof. intros. etrans; [done|apply Qp_le_plus_r]. Qed. -Lemma Qp_plus_weak_2_l q p o : q ≤ p → q ≤ p + o. -Proof. rewrite (comm_L Qp_plus). apply Qp_plus_weak_2_r. Qed. +Lemma Qp_add_weak_2_r q p o : q ≤ o → q ≤ p + o. +Proof. intros. etrans; [done|apply Qp_le_add_r]. Qed. +Lemma Qp_add_weak_2_l q p o : q ≤ p → q ≤ p + o. +Proof. rewrite (comm_L Qp_add). apply Qp_add_weak_2_r. Qed. -Lemma Qc_minus_Some p q r : p - q = Some r ↔ p = q + r. +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_minus, Qp_plus; simpl; rewrite <-Qp_to_Qc_inj_iff; simpl. split. + 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. @@ -999,36 +999,36 @@ Proof. rewrite <-(Qcplus_0_r p) at 1. by apply Qcplus_lt_mono_l. Qed. -Lemma Qc_minus_None p q : p - q = None ↔ p ≤ q. +Lemma Qp_sub_None p q : p - q = None ↔ p ≤ q. Proof. rewrite Qp_le_ngt, Qp_lt_sum, eq_None_not_Some. - by setoid_rewrite <-Qc_minus_Some. + by setoid_rewrite <-Qp_sub_Some. Qed. -Lemma Qp_minus_diag p : p - p = None. -Proof. by apply Qc_minus_None. Qed. -Lemma Qp_plus_minus p q : (p + q) - p = Some q. -Proof. by apply Qc_minus_Some. Qed. +Lemma Qp_sub_diag p : p - p = None. +Proof. by apply Qp_sub_None. Qed. +Lemma Qp_add_minus p q : (p + q) - p = Some q. +Proof. by apply Qp_sub_Some. Qed. Lemma Qp_inv_lt_mono p q : p < q ↔ /q < /p. Proof. revert p q. cut (∀ p q, p < q → / q < / p). { intros help p q. split; [apply help|]. intros. rewrite <-(Qp_inv_involutive p), <-(Qp_inv_involutive q). by apply help. } - intros p q Hpq. apply (Qp_mult_lt_mono_l _ _ q). rewrite Qp_mult_inv_r. - apply (Qp_mult_lt_mono_r _ _ p). rewrite <-(assoc_L _), Qp_mult_inv_l. - by rewrite Qp_mult_1_l, Qp_mult_1_r. + intros p q Hpq. apply (Qp_mul_lt_mono_l _ _ q). rewrite Qp_mul_inv_r. + apply (Qp_mul_lt_mono_r _ _ p). rewrite <-(assoc_L _), Qp_mul_inv_l. + by rewrite Qp_mul_1_l, Qp_mul_1_r. Qed. Lemma Qp_inv_le_mono p q : p ≤ q ↔ /q ≤ /p. Proof. by rewrite !Qp_le_ngt, Qp_inv_lt_mono. Qed. Lemma Qp_div_le_mono_l p q r : q ≤ p ↔ r / p ≤ r / q. -Proof. unfold Qp_div. by rewrite <-Qp_mult_le_mono_l, Qp_inv_le_mono. Qed. +Proof. unfold Qp_div. by rewrite <-Qp_mul_le_mono_l, Qp_inv_le_mono. Qed. Lemma Qp_div_le_mono_r p q r : p ≤ q ↔ p / r ≤ q / r. -Proof. apply Qp_mult_le_mono_r. Qed. +Proof. apply Qp_mul_le_mono_r. Qed. Lemma Qp_div_lt_mono_l p q r : q < p ↔ r / p < r / q. -Proof. unfold Qp_div. by rewrite <-Qp_mult_lt_mono_l, Qp_inv_lt_mono. Qed. +Proof. unfold Qp_div. by rewrite <-Qp_mul_lt_mono_l, Qp_inv_lt_mono. Qed. Lemma Qp_div_lt_mono_r p q r : p < q ↔ p / r < q / r. -Proof. apply Qp_mult_lt_mono_r. Qed. +Proof. apply Qp_mul_lt_mono_r. Qed. Lemma Qp_div_lt p q : 1 < q → p / q < p. Proof. by rewrite (Qp_div_lt_mono_l _ _ p), Qp_div_1. Qed. @@ -1065,14 +1065,14 @@ Proof. destruct (Qp_lt_le_dec a c) as [?|[?| ->]%Qp_le_lt_or_eq]. - auto. - destruct (help c d a b); [done..|]. naive_solver. - - apply (inj (Qp_plus a)) in Habcd as ->. + - apply (inj (Qp_add a)) in Habcd as ->. destruct (Qp_lower_bound a d) as (q&a'&d'&->&->). - exists a', q, q, d'. repeat split; done || by rewrite (comm_L Qp_plus). } - intros a b c d [e ->]%Qp_lt_sum. rewrite <-(assoc_L _). intros ->%(inj (Qp_plus a)). + exists a', q, q, d'. repeat split; done || by rewrite (comm_L Qp_add). } + intros a b c d [e ->]%Qp_lt_sum. rewrite <-(assoc_L _). intros ->%(inj (Qp_add a)). destruct (Qp_lower_bound a d) as (q&a'&d'&->&->). - eexists a', q, (q + e)%Qp, d'; split_and?; [by rewrite (comm_L Qp_plus)|..|done]. - - by rewrite (assoc_L _), (comm_L Qp_plus e). - - by rewrite (assoc_L _), (comm_L Qp_plus a'). + eexists a', q, (q + e)%Qp, d'; split_and?; [by rewrite (comm_L Qp_add)|..|done]. + - by rewrite (assoc_L _), (comm_L Qp_add e). + - by rewrite (assoc_L _), (comm_L Qp_add a'). Qed. Lemma Qp_bounded_split p r : ∃ q1 q2 : Qp, q1 ≤ r ∧ p = q1 + q2. @@ -1119,7 +1119,7 @@ Proof. rewrite (comm_L Qp_max q). apply Qp_le_max_l. Qed. Lemma Qp_max_plus q p : q `max` p ≤ q + p. Proof. unfold Qp_max. - destruct (decide (q ≤ p)); [apply Qp_le_plus_r|apply Qp_le_plus_l]. + destruct (decide (q ≤ p)); [apply Qp_le_add_r|apply Qp_le_add_l]. Qed. Lemma Qp_max_lub_l q p o : q `max` p ≤ o → q ≤ o. @@ -1177,9 +1177,9 @@ 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). +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. -Lemma pos_to_Qp_mult x y : pos_to_Qp x * pos_to_Qp y = pos_to_Qp (x * y). +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. Local Close Scope Qp_scope. -- GitLab From b2f40d2a0a43eea9f74ee229207ffaa4a36f6309 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Tue, 6 Oct 2020 22:14:26 +0200 Subject: [PATCH 08/12] Make `Qp` lemma names consistent with those for `Nat`, `Z` and friends. --- theories/numbers.v | 99 ++++++++++++++++++++++++---------------------- 1 file changed, 52 insertions(+), 47 deletions(-) diff --git a/theories/numbers.v b/theories/numbers.v index e55811ea..6d085fc0 100644 --- a/theories/numbers.v +++ b/theories/numbers.v @@ -798,9 +798,9 @@ Proof. intros q1 q2 Hpq. apply (inj (Qp_mul p)). by rewrite !(comm_L Qp_mul p). Qed. -Lemma Qp_mul_add_distr_r p q r : p * (q + r) = p * q + p * r. +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. -Lemma Qp_mul_add_distr_l p q r : (p + q) * r = p * r + q * r. +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. Lemma Qp_mul_1_l p : 1 * p = p. Proof. destruct p; apply Qp_to_Qc_inj_iff, Qcmult_1_l. Qed. @@ -809,8 +809,8 @@ Proof. destruct p; apply Qp_to_Qc_inj_iff, Qcmult_1_r. Qed. Lemma Qp_one_one : 1 + 1 = 2. Proof. apply (bool_decide_unpack _); by compute. Qed. -Lemma Qp_add_diag p : p + p = (2 * p). -Proof. by rewrite <-Qp_one_one, Qp_mul_add_distr_l, !Qp_mul_1_l. Qed. +Lemma Qp_add_diag p : p + p = 2 * p. +Proof. by rewrite <-Qp_one_one, Qp_mul_add_distr_r, !Qp_mul_1_l. Qed. Lemma Qp_mul_inv_l p : /p * p = 1. Proof. @@ -847,7 +847,7 @@ Proof. unfold Qp_div. by rewrite <-(assoc_L _), Qp_mul_inv_l, Qp_mul_1_r. Qed. Lemma Qp_mul_div_r p q : q * (p / q) = p. Proof. by rewrite (comm_L Qp_mul q), Qp_mul_div_l. Qed. Lemma Qp_div_add_distr p q r : (p + q) / r = p / r + q / r. -Proof. apply Qp_mul_add_distr_l. Qed. +Proof. apply Qp_mul_add_distr_r. Qed. Lemma Qp_div_div p q r : (p / q) / r = p / (q * r). Proof. unfold Qp_div. by rewrite Qp_inv_mul_distr, (assoc_L _). Qed. Lemma Qp_div_mul_cancel_l p q r : (r * p) / (r * q) = p / q. @@ -893,14 +893,15 @@ Qed. Instance Qp_le_total: Total (≤)%Qp. Proof. intros p q. rewrite !Qp_to_Qc_inj_le. apply (total Qcle). Qed. -Lemma Qp_lt_le_weak p q : p < q → p ≤ q. +Lemma Qp_lt_le_incl p q : p < q → p ≤ q. Proof. rewrite Qp_to_Qc_inj_lt, Qp_to_Qc_inj_le. apply Qclt_le_weak. Qed. -Lemma Qp_le_lt_or_eq p q : p ≤ q → p < q ∨ p = q. +Lemma Qp_le_lteq p q : p ≤ q ↔ p < q ∨ p = q. Proof. - rewrite Qp_to_Qc_inj_lt, Qp_to_Qc_inj_le. - intros [? | ->%Qp_to_Qc_inj_iff]%Qcle_lt_or_eq; auto. + rewrite Qp_to_Qc_inj_lt, Qp_to_Qc_inj_le, <-Qp_to_Qc_inj_iff. split. + - intros [?| ->]%Qcle_lt_or_eq; auto. + - intros [?| ->]; auto using Qclt_le_weak. Qed. -Lemma Qp_lt_le_dec p q : {p < q} + {q ≤ p}. +Lemma Qp_lt_ge_cases p q : {p < q} + {q ≤ p}. Proof. refine (cast_if (Qclt_le_dec (Qp_to_Qc p) (Qp_to_Qc q)%Qc)); [by apply Qp_to_Qc_inj_lt|by apply Qp_to_Qc_inj_le]. @@ -910,30 +911,30 @@ Proof. rewrite !Qp_to_Qc_inj_lt, Qp_to_Qc_inj_le. apply Qcle_lt_trans. Qed. Lemma Qp_lt_le_trans p q r : p < q → q ≤ r → p < r. Proof. rewrite !Qp_to_Qc_inj_lt, Qp_to_Qc_inj_le. apply Qclt_le_trans. Qed. -Lemma Qp_le_not_lt p q : p ≤ q → ¬q < p. -Proof. rewrite !Qp_to_Qc_inj_lt, Qp_to_Qc_inj_le. apply Qcle_not_lt. Qed. -Lemma Qp_not_lt_le p q : ¬p < q → q ≤ p. -Proof. rewrite !Qp_to_Qc_inj_lt, Qp_to_Qc_inj_le. apply Qcnot_lt_le. Qed. -Lemma Qp_lt_not_le p q : p < q → ¬q ≤ p. -Proof. rewrite !Qp_to_Qc_inj_lt, Qp_to_Qc_inj_le. apply Qclt_not_le. Qed. -Lemma Qp_not_le_lt p q : ¬p ≤ q →q < p. -Proof. rewrite !Qp_to_Qc_inj_lt, Qp_to_Qc_inj_le. apply Qcnot_le_lt. Qed. Lemma Qp_le_ngt p q : p ≤ q ↔ ¬q < p. -Proof. split; auto using Qp_le_not_lt, Qp_not_lt_le. Qed. +Proof. + rewrite !Qp_to_Qc_inj_lt, Qp_to_Qc_inj_le. + split; auto using Qcle_not_lt, Qcnot_lt_le. +Qed. Lemma Qp_lt_nge p q : p < q ↔ ¬q ≤ p. -Proof. split; auto using Qp_lt_not_le, Qp_not_le_lt. Qed. +Proof. + rewrite !Qp_to_Qc_inj_lt, Qp_to_Qc_inj_le. + split; auto using Qclt_not_le, Qcnot_le_lt. +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. 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_le_add_compat q p n m : q ≤ n → p ≤ m → q + p ≤ n + m. +Lemma Qp_add_le_mono q p n m : q ≤ n → p ≤ m → q + p ≤ n + m. Proof. intros. etrans; [by apply Qp_add_le_mono_l|by apply Qp_add_le_mono_r]. Qed. Lemma Qp_add_lt_mono_l p q r : p < q ↔ r + p < r + q. Proof. by rewrite !Qp_lt_nge, <-Qp_add_le_mono_l. Qed. Lemma Qp_add_lt_mono_r p q r : p < q ↔ p + r < q + r. Proof. by rewrite !Qp_lt_nge, <-Qp_add_le_mono_r. Qed. +Lemma Qp_add_lt_mono q p n m : q < n → p < m → q + p < n + m. +Proof. intros. etrans; [by apply Qp_add_lt_mono_l|by apply Qp_add_lt_mono_r]. Qed. Lemma Qp_mul_le_mono_l p q r : p ≤ q ↔ r * p ≤ r * q. Proof. @@ -941,6 +942,8 @@ Proof. 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. +Lemma Qp_mul_le_mono q p n m : q ≤ n → p ≤ m → q * p ≤ n * m. +Proof. intros. etrans; [by apply Qp_mul_le_mono_l|by apply Qp_mul_le_mono_r]. Qed. Lemma Qp_mul_lt_mono_l p q r : p < q ↔ r * p < r * q. Proof. @@ -948,32 +951,34 @@ Proof. 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. +Lemma Qp_mul_lt_mono q p n m : q < n → p < m → q * p < n * m. +Proof. intros. etrans; [by apply Qp_mul_lt_mono_l|by apply Qp_mul_lt_mono_r]. Qed. -Lemma Qp_lt_add_r q p : p < q + p. +Lemma Qp_lt_add_l q p : p < q + p. Proof. destruct p as [p ?], q as [q ?]. apply Qp_to_Qc_inj_lt; simpl. rewrite <- (Qcplus_0_l p) at 1. by rewrite <-Qcplus_lt_mono_r. Qed. -Lemma Qp_lt_add_l q p : q < q + p. -Proof. rewrite (comm_L Qp_add). apply Qp_lt_add_r. Qed. +Lemma Qp_lt_add_r q p : q < q + p. +Proof. rewrite (comm_L Qp_add). apply Qp_lt_add_l. Qed. Lemma Qp_not_add_ge q p : ¬(q + p ≤ q). -Proof. apply Qp_lt_not_le, Qp_lt_add_l. Qed. +Proof. apply Qp_lt_nge, Qp_lt_add_r. Qed. Lemma Qp_add_id_free q p : q + p ≠ q. Proof. intro Heq. apply (Qp_not_add_ge q p). by rewrite Heq. Qed. -Lemma Qp_le_add_r q p : p ≤ q + p. -Proof. apply Qp_lt_le_weak, Qp_lt_add_r. Qed. -Lemma Qp_le_add_l q p : q ≤ q + p. -Proof. apply Qp_lt_le_weak, Qp_lt_add_l. Qed. +Lemma Qp_le_add_l q p : p ≤ q + p. +Proof. apply Qp_lt_le_incl, Qp_lt_add_l. Qed. +Lemma Qp_le_add_r q p : q ≤ q + p. +Proof. apply Qp_lt_le_incl, Qp_lt_add_r. Qed. Lemma Qp_add_weak_r q p o : q + p ≤ o → q ≤ o. -Proof. intros. etrans; [apply Qp_le_add_l|done]. Qed. +Proof. intros. etrans; [apply Qp_le_add_r|done]. Qed. Lemma Qp_add_weak_l q p o : q + p ≤ o → p ≤ o. Proof. rewrite (comm_L Qp_add). apply Qp_add_weak_r. Qed. Lemma Qp_add_weak_2_r q p o : q ≤ o → q ≤ p + o. -Proof. intros. etrans; [done|apply Qp_le_add_r]. Qed. +Proof. intros. etrans; [done|apply Qp_le_add_l]. Qed. Lemma Qp_add_weak_2_l q p o : q ≤ p → q ≤ p + o. Proof. rewrite (comm_L Qp_add). apply Qp_add_weak_2_r. Qed. @@ -1006,8 +1011,8 @@ Proof. Qed. Lemma Qp_sub_diag p : p - p = None. Proof. by apply Qp_sub_None. Qed. -Lemma Qp_add_minus p q : (p + q) - p = Some q. -Proof. by apply Qp_sub_Some. Qed. +Lemma Qp_add_sub p q : (p + q) - q = Some p. +Proof. apply Qp_sub_Some. by rewrite (comm_L Qp_add). Qed. Lemma Qp_inv_lt_mono p q : p < q ↔ /q < /p. Proof. @@ -1040,8 +1045,8 @@ Proof. revert q1 q2. cut (∀ q1 q2 : Qp, q1 ≤ q2 → ∃ q q1' q2', q1 = q + q1' ∧ q2 = q + q2'). { intros help q1 q2. - destruct (Qp_le_dec q1 q2) as [LE|LE%Qp_lt_nge%Qp_lt_le_weak]; [by eauto|]. - destruct (help q2 q1) as (q&q1'&q2'&?&?); eauto. } + destruct (Qp_lt_ge_cases q2 q1) as [Hlt|Hle]; eauto. + destruct (help q2 q1) as (q&q1'&q2'&?&?); eauto using Qp_lt_le_incl. } intros q1 q2 Hq. exists (q1 / 2)%Qp, (q1 / 2)%Qp. assert (q1 / 2 < q2) as [q2' ->]%Qp_lt_sum. { eapply Qp_lt_le_trans, Hq. by apply Qp_div_lt. } @@ -1062,7 +1067,7 @@ Proof. a < c → a + b = c + d → ∃ ac ad bc bd, ac + ad = a ∧ bc + bd = b ∧ ac + bc = c ∧ ad + bd = d)%Qp. { intros help a b c d Habcd. - destruct (Qp_lt_le_dec a c) as [?|[?| ->]%Qp_le_lt_or_eq]. + destruct (Qp_lt_ge_cases a c) as [?|[?| ->]%Qp_le_lteq]. - auto. - destruct (help c d a b); [done..|]. naive_solver. - apply (inj (Qp_add a)) in Habcd as ->. @@ -1077,7 +1082,7 @@ Qed. Lemma Qp_bounded_split p r : ∃ q1 q2 : Qp, q1 ≤ r ∧ p = q1 + q2. Proof. - destruct (Qp_lt_le_dec r p) as [[q ->]%Qp_lt_sum|?]. + destruct (Qp_lt_ge_cases r p) as [[q ->]%Qp_lt_sum|?]. { by exists r, q. } exists (p / 2)%Qp, (p / 2)%Qp; split. + trans p; [|done]. by apply Qp_div_le. @@ -1087,19 +1092,19 @@ Qed. Lemma Qp_max_spec q p : (q < p ∧ q `max` p = p) ∨ (p ≤ q ∧ q `max` p = q). Proof. unfold Qp_max. - destruct (decide (q ≤ p)) as [[?| ->]%Qp_le_lt_or_eq|?]; [by auto..|]. - right. split; [|done]. by apply Qp_lt_le_weak, Qp_not_le_lt. + destruct (decide (q ≤ p)) as [[?| ->]%Qp_le_lteq|?]; [by auto..|]. + right. split; [|done]. by apply Qp_lt_le_incl, Qp_lt_nge. Qed. Lemma Qp_max_spec_le q p : (q ≤ p ∧ q `max` p = p) ∨ (p ≤ q ∧ q `max` p = q). -Proof. destruct (Qp_max_spec q p) as [[?%Qp_lt_le_weak?]|]; [left|right]; done. Qed. +Proof. destruct (Qp_max_spec q p) as [[?%Qp_lt_le_incl?]|]; [left|right]; done. Qed. Instance Qp_max_assoc : Assoc (=) Qp_max. Proof. intros q p o. unfold Qp_max. destruct (decide (q ≤ p)), (decide (p ≤ o)); try by rewrite ?decide_True by (by etrans). rewrite decide_False by done. - by rewrite decide_False by (apply Qp_lt_not_le; etrans; by apply Qp_lt_nge). + by rewrite decide_False by (apply Qp_lt_nge; etrans; by apply Qp_lt_nge). Qed. Instance Qp_max_comm : Comm (=) Qp_max. Proof. @@ -1116,10 +1121,10 @@ Proof. unfold Qp_max. by destruct (decide (q ≤ p)). Qed. Lemma Qp_le_max_r q p : p ≤ q `max` p. Proof. rewrite (comm_L Qp_max q). apply Qp_le_max_l. Qed. -Lemma Qp_max_plus q p : q `max` p ≤ q + p. +Lemma Qp_max_add q p : q `max` p ≤ q + p. Proof. unfold Qp_max. - destruct (decide (q ≤ p)); [apply Qp_le_add_r|apply Qp_le_add_l]. + destruct (decide (q ≤ p)); [apply Qp_le_add_l|apply Qp_le_add_r]. Qed. Lemma Qp_max_lub_l q p o : q `max` p ≤ o → q ≤ o. @@ -1130,19 +1135,19 @@ Proof. rewrite (comm _ q). apply Qp_max_lub_l. Qed. Lemma Qp_min_spec q p : (q < p ∧ q `min` p = q) ∨ (p ≤ q ∧ q `min` p = p). Proof. unfold Qp_min. - destruct (decide (q ≤ p)) as [[?| ->]%Qp_le_lt_or_eq|?]; [by auto..|]. - right. split; [|done]. by apply Qp_lt_le_weak, Qp_not_le_lt. + destruct (decide (q ≤ p)) as [[?| ->]%Qp_le_lteq|?]; [by auto..|]. + right. split; [|done]. by apply Qp_lt_le_incl, Qp_lt_nge. Qed. Lemma Qp_min_spec_le q p : (q ≤ p ∧ q `min` p = q) ∨ (p ≤ q ∧ q `min` p = p). -Proof. destruct (Qp_min_spec q p) as [[?%Qp_lt_le_weak?]|]; [left|right]; done. Qed. +Proof. destruct (Qp_min_spec q p) as [[?%Qp_lt_le_incl ?]|]; [left|right]; done. Qed. Instance Qp_min_assoc : Assoc (=) Qp_min. Proof. intros q p o. unfold Qp_min. destruct (decide (q ≤ p)), (decide (p ≤ o)); eauto using decide_False. - by rewrite !decide_True by (by etrans). - - by rewrite decide_False by (apply Qp_lt_not_le; etrans; by apply Qp_lt_nge). + - by rewrite decide_False by (apply Qp_lt_nge; etrans; by apply Qp_lt_nge). Qed. Instance Qp_min_comm : Comm (=) Qp_min. Proof. -- GitLab From f106ebdd476c0372b02f621f69188877e825a33c Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Wed, 7 Oct 2020 10:40:04 +0200 Subject: [PATCH 09/12] Add lemmas for 1/4 + 1/4. --- theories/numbers.v | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/theories/numbers.v b/theories/numbers.v index 6d085fc0..5f283840 100644 --- a/theories/numbers.v +++ b/theories/numbers.v @@ -839,6 +839,8 @@ Lemma Qp_inv_1 : /1 = 1. Proof. apply (bool_decide_unpack _); by compute. Qed. Lemma Qp_inv_half_half : /2 + /2 = 1. Proof. apply (bool_decide_unpack _); by compute. Qed. +Lemma Qp_inv_quarter_quarter : /4 + /4 = /2. +Proof. apply (bool_decide_unpack _); by compute. Qed. Lemma Qp_div_diag p : p / p = 1. Proof. apply Qp_mul_inv_r. Qed. @@ -868,6 +870,8 @@ Lemma Qp_div_S 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. apply (bool_decide_unpack _); by compute. Qed. +Lemma Qp_quarter_quarter : 1 / 4 + 1 / 4 = 1 / 2. +Proof. apply (bool_decide_unpack _); by compute. Qed. Lemma Qp_quarter_three_quarter : 1 / 4 + 3 / 4 = 1. Proof. apply (bool_decide_unpack _); by compute. Qed. Lemma Qp_three_quarter_quarter : 3 / 4 + 1 / 4 = 1. -- GitLab From c701258333cb8c6e6829bc83b1861446b6d5508a Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Tue, 27 Oct 2020 14:59:01 +0100 Subject: [PATCH 10/12] Tweaks based on feedback Ralf. --- theories/numbers.v | 35 ++++++++++++++--------------------- 1 file changed, 14 insertions(+), 21 deletions(-) diff --git a/theories/numbers.v b/theories/numbers.v index 5f283840..ed42de03 100644 --- a/theories/numbers.v +++ b/theories/numbers.v @@ -807,10 +807,10 @@ Proof. destruct p; apply Qp_to_Qc_inj_iff, 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. -Lemma Qp_one_one : 1 + 1 = 2. +Lemma Qp_1_1 : 1 + 1 = 2. Proof. apply (bool_decide_unpack _); by compute. Qed. Lemma Qp_add_diag p : p + p = 2 * p. -Proof. by rewrite <-Qp_one_one, Qp_mul_add_distr_r, !Qp_mul_1_l. Qed. +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. @@ -866,7 +866,7 @@ Proof. rewrite <-Qp_div_add_distr, Qp_add_diag. rewrite <-(Qp_mul_1_r 2) at 2. by rewrite Qp_div_mul_cancel_l, Qp_div_1. Qed. -Lemma Qp_div_S p q : p / (2 * q) + p / (2 * q) = p / q. +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. apply (bool_decide_unpack _); by compute. Qed. @@ -958,34 +958,27 @@ Proof. rewrite !(comm_L Qp_mul _ r). apply Qp_mul_lt_mono_l. Qed. Lemma Qp_mul_lt_mono q p n m : q < n → p < m → q * p < n * m. Proof. intros. etrans; [by apply Qp_mul_lt_mono_l|by apply Qp_mul_lt_mono_r]. Qed. -Lemma Qp_lt_add_l q p : p < q + p. +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_l p) at 1. by rewrite <-Qcplus_lt_mono_r. + rewrite <- (Qcplus_0_r p) at 1. by rewrite <-Qcplus_lt_mono_l. Qed. -Lemma Qp_lt_add_r q p : q < q + p. +Lemma Qp_lt_add_r p q : q < p + q. Proof. rewrite (comm_L Qp_add). apply Qp_lt_add_l. Qed. -Lemma Qp_not_add_ge q p : ¬(q + p ≤ q). +Lemma Qp_not_add_le_l p q : ¬(p + q ≤ p). +Proof. apply Qp_lt_nge, Qp_lt_add_l. Qed. +Lemma Qp_not_add_le_r p q : ¬(p + q ≤ q). Proof. apply Qp_lt_nge, Qp_lt_add_r. Qed. + Lemma Qp_add_id_free q p : q + p ≠ q. -Proof. intro Heq. apply (Qp_not_add_ge q p). by rewrite Heq. Qed. +Proof. intro Heq. apply (Qp_not_add_le_l q p). by rewrite Heq. Qed. -Lemma Qp_le_add_l q p : p ≤ q + p. +Lemma Qp_le_add_l p q : p ≤ p + q. Proof. apply Qp_lt_le_incl, Qp_lt_add_l. Qed. -Lemma Qp_le_add_r q p : q ≤ q + p. +Lemma Qp_le_add_r p q : q ≤ p + q. Proof. apply Qp_lt_le_incl, Qp_lt_add_r. Qed. -Lemma Qp_add_weak_r q p o : q + p ≤ o → q ≤ o. -Proof. intros. etrans; [apply Qp_le_add_r|done]. Qed. -Lemma Qp_add_weak_l q p o : q + p ≤ o → p ≤ o. -Proof. rewrite (comm_L Qp_add). apply Qp_add_weak_r. Qed. - -Lemma Qp_add_weak_2_r q p o : q ≤ o → q ≤ p + o. -Proof. intros. etrans; [done|apply Qp_le_add_l]. Qed. -Lemma Qp_add_weak_2_l q p o : q ≤ p → q ≤ p + o. -Proof. rewrite (comm_L Qp_add). apply Qp_add_weak_2_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]. @@ -1128,7 +1121,7 @@ Proof. rewrite (comm_L Qp_max q). apply Qp_le_max_l. Qed. Lemma Qp_max_add q p : q `max` p ≤ q + p. Proof. unfold Qp_max. - destruct (decide (q ≤ p)); [apply Qp_le_add_l|apply Qp_le_add_r]. + destruct (decide (q ≤ p)); [apply Qp_le_add_r|apply Qp_le_add_l]. Qed. Lemma Qp_max_lub_l q p o : q `max` p ≤ o → q ≤ o. -- GitLab From e8adfd04076260af268343d726c18f0192d31ccd Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Wed, 28 Oct 2020 20:13:34 +0100 Subject: [PATCH 11/12] CHANGELOG. --- CHANGELOG.md | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 3dded487..fa7cf357 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -15,6 +15,29 @@ Coq 8.8 and 8.9 are no longer supported. `zip_with` and `Forall2` versions of `∪`, `∖`, and `##`. - Remove unused type classes `DisjointE`, `DisjointList`, `LookupE`, and `InsertE`. +- Overhaul of the theory of positive rationals `Qp`: + + Add the orders `Qp_le` and `Qp_lt`. + + Rename `Qp_plus` into `Qp_add` and `Qp_mult` into `Qp_mul` to be consistent + with the corresponding names for `nat`, `N`, and `Z`. + + Add a function `Qp_inv` for the multiplicative inverse. + + Define the division function `Qp_div` in terms of `Qp_inv`, and generalize + the second argument from `positive` to `Qp`. + + Add a function `pos_to_Qp` that converts a `positive` into a positive + rational `Qp`. + + Add many lemmas and missing type class instances, especially for orders, + multiplication, multiplicative inverse, division, and the conversion. + + Remove the coercion from `Qp` to `Qc`. This follows our recent tradition of + getting rid of coercions since they are more often confusing than useful. + + Rename the conversion from `Qp_car : Qp → Qc` into `Qp_to_Qc` to be + consistent with other conversion functions in std++. Also rename the lemma + `Qp_eq` into `Qp_to_Qc_inj_iff`. + + Use `let '(..) = ...` in the definitions of `Qp_plus`, `Qp_mult`, `Qp_inv`, + `Qp_le` and `Qp_lt` to avoid Coq tactics (like `injection`) to unfold these + definitions eagerly. + + Define the `Qp` literals 1, 2, 3, 4 in terms of `pos_to_Qp` instead of + iterated addition. + + Rename and restate many lemmas so as to be consistent with the conventions + for Coq's number types `nat`, `N`, and `Z`. The following `sed` script should perform most of the renaming (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`): -- GitLab From 420e57f67edb94250ddbf64d8ba35046479d4d4d Mon Sep 17 00:00:00 2001 From: Robbert Krebbers Date: Thu, 29 Oct 2020 11:00:00 +0100 Subject: [PATCH 12/12] Update sed script. --- CHANGELOG.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index fa7cf357..d4f13b19 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -43,7 +43,8 @@ The following `sed` script should perform most of the renaming (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`): ``` sed -i ' -s/\bQp_not_plus_q_ge_1\b/Qp_not_plus_ge/g +s/\bQp_plus/Qp_add/g +s/\bQp_mult/Qp_mul/g ' $(find theories -name "*.v") ``` -- GitLab