CoRN.stdlib_omissions.Q

Require Import
  QArith ZArith NArith Qpower Qround
  Qround Qabs List.

Require stdlib_omissions.Z.

Set Automatic Introduction.

Notation "x <= y < z" := (x y y < z) : Q_scope.
Notation "x < y <= z" := (x < y y z) : Q_scope.
Notation "x < y < z" := (x < y y < z) : Q_scope.

Open Scope Q_scope.

Lemma Qnum_nonneg (x : Q) : (0 Qnum x)%Z (0 x)%Q.
Proof.
  destruct x as [n d].
  unfold Qle. simpl.
  now rewrite Zmult_1_r.
Qed.

Lemma Qnum_nonpos (x : Q) : (Qnum x 0)%Z (x 0)%Q.
Proof.
  destruct x as [n d].
  unfold Qle. simpl.
  now rewrite Zmult_1_r.
Qed.

Lemma Qle_dec x y: {Qle x y} + {¬Qle x y}.
  intros.
  destruct (Qlt_le_dec y x); [right | left]; [apply Qlt_not_le |]; assumption.
Defined.


Lemma Zplus_Qplus (m n: Z): inject_Z (m + n) = inject_Z m + inject_Z n.
Proof.
 unfold Qplus. simpl. unfold inject_Z.
 do 2 rewrite Zmult_1_r. reflexivity.
Qed.

Lemma Zsucc_Qplus (z: Z): inject_Z (Zsucc z) = inject_Z z + 1.
Proof. apply Zplus_Qplus. Qed.

Lemma Zmult_Qmult (x y: Z): inject_Z (x × y) = inject_Z x × inject_Z y.
Proof. reflexivity. Qed.

Lemma S_Qplus (n: nat): inject_Z (Z_of_nat (S n)) = inject_Z (Z_of_nat n) + 1.
Proof. rewrite inj_S. apply Zplus_Qplus. Qed.

Lemma Pmult_Qmult (x y: positive): inject_Z (' (Pmult x y)) = inject_Z (' x) × inject_Z (' y).
Proof. rewrite Zpos_mult_morphism. apply Zmult_Qmult. Qed.

Lemma Zle_Qle (x y: Z): (x y)%Z = (inject_Z x inject_Z y).
Proof.
 unfold Qle. intros. simpl.
 do 2 rewrite Zmult_1_r. reflexivity.
Qed.

Lemma Zlt_Qlt (x y: Z): (x < y)%Z = (inject_Z x < inject_Z y).
Proof.
 unfold Qlt. intros. simpl.
 do 2 rewrite Zmult_1_r. reflexivity.
Qed.

Lemma Zdiv_Qdiv (n m: Z): (n / m)%Z = Qfloor (inject_Z n / inject_Z m).
Proof with simpl; try reflexivity.
 unfold Qfloor. intros. simpl.
 destruct m...
   rewrite Zdiv_0_r.
   rewrite Zmult_0_r...
  rewrite Zmult_1_r...
 rewrite <- Zopp_eq_mult_neg_1.
 rewrite <- (Zopp_involutive (Zpos p)).
 rewrite Zdiv_opp_opp...
Qed.

Lemma Qle_nat (n: nat): 0 inject_Z (Z_of_nat n).
Proof. rewrite <- (Zle_Qle 0). apply Zle_0_nat. Qed.

Lemma inject_Z_injective (a b: Z): inject_Z a = inject_Z b a = b.
Proof. unfold inject_Z. split; congruence. Qed.

Lemma Qeq_Zeq (a b: Z): (inject_Z a == inject_Z b) = (a = b).
Proof.
 unfold Qeq.
 simpl.
 intros.
 do 2 rewrite Zmult_1_r.
 reflexivity.
Qed.

Lemma positive_nonzero_in_Q (p: positive): ¬ inject_Z (Zpos p) == 0.
Proof. discriminate. Qed.

Hint Immediate positive_nonzero_in_Q.


Lemma Qmult_injective_l (z: Q) (Znz: ¬ z == 0): x y, (x × z == y × z x == y).
Proof.
 split; intro E.
  rewrite <- (Qmult_1_r x).
  rewrite <- (Qmult_1_r y).
  rewrite <- (Qmult_inv_r _ Znz).
  do 2 rewrite Qmult_assoc.
  rewrite E. reflexivity.
 rewrite E. reflexivity.
Qed.

Lemma Qmult_injective_r (z: Q) (Znz: ¬ z == 0): x y, (z × x == z × y x == y).
Proof.
 intros. do 2 rewrite (Qmult_comm z).
 apply Qmult_injective_l. assumption.
Qed.

Lemma Qplus_injective_l (z: Q): x y, (x + z == y + z x == y)%Q.
Proof with intuition.
 split; intro E.
  setoid_replace x with (x + z - z)%Q by (simpl; ring).
  setoid_replace y with (y + z - z)%Q by (simpl; ring).
  rewrite E...
 rewrite E...
Qed.

Lemma Qminus_eq (x y: Q): (x - y == 0 x == y)%Q.
Proof.
 rewrite <- (Qplus_injective_l (-y) x y).
 rewrite Qplus_opp_r.
 reflexivity.
Qed.

Lemma Qinv_char x q: (x × q == 1) (x == / q ¬ q == 0).
Proof with auto.
 split.
  intros A.
  assert (¬ q == 0).
   intro B. apply Q_apart_0_1. rewrite <- A, B. ring.
  intuition.
  apply (Qmult_injective_l q)...
  rewrite A. field...
 intros [A ?]. rewrite A. field...
Qed.

Lemma Qdiv_1_r (q: Q): q / 1 == q.
Proof. field. Qed.

Lemma show_is_Qinv x q: x × q == 1 → x == / q.
Proof. intros. apply Qinv_char. assumption. Qed.

Lemma Qabs_Qminus x y: Qabs (x - y) == Qabs (y - x).
Proof.
 unfold Qminus.
 intros.
 rewrite <- (Qopp_opp x) at 1.
 rewrite <- Qopp_plus.
 rewrite Qplus_comm.
 apply Qabs_opp.
Qed.

Lemma Qlt_floor_alt (x : Q) :
  x - 1 < inject_Z (Qfloor x).
Proof.
  apply Qplus_lt_l with 1.
  ring_simplify.
  change 1 with (inject_Z 1).
  rewrite <-inject_Z_plus.
  apply Qlt_floor.
Qed.

Lemma Qfloor_pos (x : Q) :
  1 x → (0 < Qfloor x)%Z.
Proof.
  intros E.
  rewrite Zlt_Qlt.
  apply Qle_lt_trans with (x - 1).
   apply Qplus_le_l with 1.
   now ring_simplify.
  apply Qlt_floor_alt.
Qed.

Lemma Qpower_not_0 (a : Q) (n : Z) :
  ¬a==0 → ¬a ^ n == 0.
Proof.
  intros E1.
  destruct n; simpl.
    discriminate.
   now apply Qpower_not_0_positive.
  intros E2.
  destruct (Qpower_not_0_positive a p).
   easy.
  now rewrite <-Qinv_involutive, E2.
Qed.

Lemma Qpower_0_lt (a : Q) (n : Z) :
  0 < a → 0 < a ^ n.
Proof.
  intros E1.
  destruct (Qle_lt_or_eq 0 (a ^ n)) as [E2|E2]; try assumption.
   now apply Qpower_pos, Qlt_le_weak.
  symmetry in E2. contradict E2.
  apply Qpower_not_0.
  intros E3. symmetry in E3.
  now destruct (Qlt_not_eq 0 a).
Qed.

Lemma Qneq_symmetry (x y : Q) :
  ¬x == y¬y == x.
Proof. firstorder. Qed.

Lemma Qdiv_flip_le (x y : Q) :
  0 < xx y/y /x.
Proof.
  intros E1 E2.
  assert (0 < y) by now apply Qlt_le_trans with x.
  apply Qmult_le_l with x; try assumption.
  apply Qmult_le_l with y; try assumption.
  field_simplify.
    unfold Qdiv. now rewrite 2!Qmult_1_r.
   now apply Qneq_symmetry, Qlt_not_eq.
  now apply Qneq_symmetry, Qlt_not_eq.
Qed.

Lemma Qdiv_flip_lt (x y : Q) :
  0 < xx < y/y < /x.
Proof.
  intros E1 E2.
  assert (0 < y) by now apply Qlt_trans with x.
  apply Qmult_lt_l with x; try assumption.
  apply Qmult_lt_l with y; try assumption.
  field_simplify.
    unfold Qdiv. now rewrite 2!Qmult_1_r.
   now apply Qneq_symmetry, Qlt_not_eq.
  now apply Qneq_symmetry, Qlt_not_eq.
Qed.


Lemma Qpos_nonNeg (n d: positive): 0 Zpos n # d.
Proof. discriminate. Qed.

Hint Immediate Qpos_nonNeg.

Lemma Qplus_le_l (z x y : Q): x + z y + z x y.
Proof with auto with ×.
 split; intros.
  setoid_replace x with (x + z + -z) by (simpl; ring).
  setoid_replace y with (y + z + -z) by (simpl; ring).
  apply Qplus_le_compat...
 apply Qplus_le_compat...
Qed.

Lemma Qplus_le_r (z x y : Q): z + x z + y x y.
Proof. do 2 rewrite (Qplus_comm z). apply Qplus_le_l. Qed.

Lemma Qplus_lt_r (x y: Q) : x < y z, z + x < z + y.
Proof. intros E z. do 2 rewrite (Qplus_comm z). apply Qplus_lt_l. assumption. Qed.

Lemma Qmult_le_compat_l (x y z : Q): x y → 0 zz × x z × y.
Proof. do 2 rewrite (Qmult_comm z). apply Qmult_le_compat_r. Qed.

Lemma Qopp_Qlt_0_l (x: Q): 0 < -x x < 0.
Proof.
 split.
  rewrite <- (Qopp_opp x) at 2.
  apply (Qopp_lt_compat 0 (-x)).
 apply (Qopp_lt_compat x 0).
Qed.

Lemma Qopp_Qlt_0_r (x: Q): -x < 0 0 < x.
Proof. rewrite <- Qopp_Qlt_0_l, Qopp_opp. reflexivity. Qed.

Lemma Qmult_lt_0_compat (x y: Q): 0 < x → 0 < y → 0 < x × y.
Proof.
 destruct x, y. unfold Qlt. simpl.
 repeat rewrite Zmult_1_r.
 apply Zmult_lt_0_compat.
Qed.

Hint Resolve Qmult_lt_0_compat.

Lemma Qmult_nonneg_nonpos (x y: Q):
  0 xy 0 → x × y 0.
Proof with auto.
 unfold Qle. simpl.
 repeat rewrite Zmult_1_r. intros.
 rewrite <- (Zmult_0_r (Qnum x)).
 apply (Zmult_le_compat_l (Qnum y) 0 (Qnum x))...
Qed.

Lemma Qmult_neg_pos (x y : Q) : x < 0 → 0 < yx × y < 0.
Proof.
intros H1 H2.
apply Qopp_Qlt_0_l. setoid_replace (- (x × y)) with ((- x) × y) by ring.
apply Qmult_lt_0_compat; trivial. now apply Qopp_Qlt_0_l.
Qed.

Lemma Qmult_pos_neg (x y : Q) : 0 < xy < 0 → x × y < 0.
Proof. intros H1 H2. rewrite Qmult_comm. now apply Qmult_neg_pos. Qed.

Lemma Qmult_pos_r : x y : Q, 0 x → 0 < x × y → 0 < y.
Proof.
intros x y H1 H2.
destruct (Q_dec y 0) as [[? | ?] | H]; trivial.
+ exfalso. apply (Qlt_irrefl 0), Qlt_le_trans with (y := x × y); trivial.
  now apply Qmult_nonneg_nonpos; [| apply Qlt_le_weak].
+ rewrite H, Qmult_0_r in H2. exfalso; now apply (Qlt_irrefl 0).
Qed.

Lemma Qmult_pos_l : x y : Q, 0 y → 0 < x × y → 0 < x.
Proof. intros x y H1 H2. rewrite Qmult_comm in H2. now apply (Qmult_pos_r y x). Qed.

Lemma Qplus_lt_le_0_compat x y: 0 < x → 0 y → 0 < x + y.
Proof with auto.
 unfold Qlt, Qle. simpl.
 repeat rewrite Zmult_1_r. intros.
 apply Z.add_pos_nonneg.
  apply Zmult_lt_0_compat...
  reflexivity.
 apply Zmult_le_0_compat...
 discriminate.
Qed.

Lemma Qplus_le_lt_0_compat x y: 0 x → 0 < y → 0 < x + y.
Proof.
 rewrite Qplus_comm. intros.
 apply (Qplus_lt_le_0_compat y x); assumption.
Qed.

Lemma Qplus_nonneg (x y: Q): 0 x → 0 y → 0 x + y.
Proof.
 intros.
 change (0 + 0 x + y).
 apply Qplus_le_compat; assumption.
Qed.

Lemma Qplus_pos_compat (x y : Q) : 0 < x → 0 < y → 0 < x + y.
Proof. intros; apply Qplus_lt_le_0_compat; [| apply Qlt_le_weak]; trivial. Qed.

Lemma Qminus_less (x y : Q) : 0 yx - y x.
Proof.
intro H. rewrite <- (Qplus_0_r x) at 2. apply Qplus_le_r. change 0 with (-0).
now apply Qopp_le_compat.
Qed.

Lemma Qabs_Qle x y: (Qabs x y) (-y x y).
Proof with intuition.
 split.
  split.
   rewrite <- (Qopp_opp x).
   apply Qopp_le_compat.
   apply Qle_trans with (Qabs (-x)).
    apply Qle_Qabs.
   rewrite Qabs_opp...
  apply Qle_trans with (Qabs x)...
  apply Qle_Qabs.
 intros.
 apply Qabs_case...
 rewrite <- (Qopp_opp y).
 apply Qopp_le_compat...
Qed.

Lemma Qabs_diff_Qle x y r: (Qabs (x - y) r) (x - r y x + r).
Proof with try ring.
 intros.
 rewrite Qabs_Qle.
 rewrite <- (Qplus_le_r (r + y) (-r) (x- y)).
 rewrite <- (Qplus_le_r (y - r) (x-y) r).
 setoid_replace (r + y + -r) with y...
 setoid_replace (r + y + (x - y)) with (x + r)...
 setoid_replace (y - r + (x - y)) with (x - r)...
 setoid_replace (y - r + r) with y...
 intuition.
Qed.

Lemma Qabs_zero (x : Q) : Qabs x == 0 x == 0.
Proof.
split; intro H; [| now rewrite H].
destruct (Q_dec x 0) as [[x_neg | x_pos] | x_zero]; [| | trivial].
+ rewrite Qabs_neg in H; [| apply Qlt_le_weak; trivial].
  now rewrite <- (Qopp_involutive x), H.
+ rewrite Qabs_pos in H; [| apply Qlt_le_weak]; trivial.
Qed.

Lemma Qabs_nonpos (x : Q) : Qabs x 0 → x == 0.
Proof.
intro H. apply Qle_lteq in H. destruct H as [H | H].
+ elim (Qlt_not_le _ _ H (Qabs_nonneg x)).
+ now apply Qabs_zero.
Qed.

Lemma Qabs_le_nonneg (x y : Q) : 0 x → (Qabs x y x y).
Proof.
 intro A. rewrite Qabs_Qle_condition.
 split; [intros [_ ?]; trivial | intro A1; split; [| trivial]].
 apply Qle_trans with (y := 0); [| trivial].
 apply (Qopp_le_compat 0); eapply Qle_trans; eauto.
Qed.

Lemma Qdiv_le_1 (x y: Q): 0 x yx / y 1.
Proof with intuition.
 intros.
 assert (0 y) as ynnP by (apply Qle_trans with x; intuition).
 destruct y.
 destruct Qnum.
   change (x × 0 1).
   rewrite Qmult_0_r...
  rewrite <- (Qmult_inv_r ('p # Qden)).
   unfold Qdiv.
   apply Qmult_le_compat_r...
  discriminate.
 exfalso. apply ynnP...
Qed.


Lemma Qle_shift_div_l : a b c, 0 < c → (a × c b a b / c).
Proof.
intros a b c A; split; [now apply Qle_shift_div_l |].
intro A1. apply (Qmult_le_r _ _ (/c)); [now apply Qinv_lt_0_compat |].
rewrite <- Qmult_assoc, Qmult_inv_r; [now rewrite Qmult_1_r | auto with qarith].
Qed.

Lemma Qle_shift_div_r : a b c, 0 < b → (a c × b a / b c).
Proof.
intros a b c A; split; [now apply Qle_shift_div_r |].
intro A1. apply (Qmult_le_r _ _ (/b)); [now apply Qinv_lt_0_compat |].
rewrite <- Qmult_assoc, Qmult_inv_r; [now rewrite Qmult_1_r | auto with qarith].
Qed.

Lemma Qle_div_l : a b c, 0 < b → 0 < c → (a / b c a / c b).
Proof.
intros a b c A1 A2.
rewrite <- Qle_shift_div_r; [| easy]. rewrite (Qmult_comm c b). rewrite Qle_shift_div_r; easy.
Qed.

Lemma Qle_div_r : a b c, 0 < b → 0 < c → (b a / c c a / b).
Proof.
intros a b c A1 A2.
rewrite <- Qle_shift_div_l; [| easy]. rewrite (Qmult_comm b c). rewrite Qle_shift_div_l; easy.
Qed.

Lemma Qle_half (x : Q) : 0 x(1 # 2) × x x.
Proof.
intro H. rewrite <- (Qmult_1_l x) at 2. apply Qmult_le_compat_r; auto with qarith.
Qed.

Lemma nat_lt_Qlt n m: (n < m)%nat → (inject_Z (Z_of_nat n) + (1#2) < inject_Z (Z_of_nat m))%Q.
Proof with intuition.
 unfold lt.
 intros.
 apply Qlt_le_trans with (inject_Z (Z_of_nat n) + 1).
  do 2 rewrite (Qplus_comm (inject_Z (Z_of_nat n))).
  apply Qplus_lt_l...
 pose proof (inj_le _ _ H).
 rewrite Zle_Qle in H0.
 rewrite <- S_Qplus...
Qed.

Lemma inject_Z_nonneg (z: Z): (0 z)%Z → 0 inject_Z z.
Proof with auto.
 intro.
 change (inject_Z 0 inject_Z z).
 rewrite <- Zle_Qle.
 assumption.
Qed.

Hint Resolve inject_Z_nonneg.

Lemma positive_in_Q (p: positive): 0 < inject_Z (Zpos p).
Proof.
 change (inject_Z 0 < inject_Z (' p)).
 rewrite <- Zlt_Qlt.
 reflexivity.
Qed.

Hint Immediate positive_in_Q.

SearchAbout (_ - ?x < _ - ?x)%Q.

Lemma Qlt_Qceiling (q : Q) : inject_Z (Qceiling q) < q + 1.
Proof.
apply Qplus_lt_l with (z := (-1 # 1)). setoid_replace (q + 1 + (-1 # 1))%Q with q.
+ assert (A := Qceiling_lt q). unfold Z.sub in A.
  now rewrite inject_Z_plus, inject_Z_opp in A.
+ now rewrite <- Qplus_assoc, Qplus_opp_r, Qplus_0_r.
Qed.

Lemma Zle_Qle_Qceiling (q : Q) (z : Z) : (Qceiling q z)%Z q inject_Z z.
Proof.
split; intro A.
+ rewrite Zle_Qle in A. apply Qle_trans with (y := inject_Z (Qceiling q)); [apply Qle_ceiling | trivial].
+ apply Z.lt_pred_le. rewrite Zlt_Qlt. now apply Qlt_le_trans with (y := q); [apply Qceiling_lt |].
Qed.

Lemma le_Qle_Qceiling_to_nat (q : Q) (n : nat) :
  (Z.to_nat (Qceiling q) n)%nat q inject_Z (Z.of_nat n).
Proof. rewrite Z.le_Zle_to_nat; apply Zle_Qle_Qceiling. Qed.

Lemma Qlt_Zlt_inject_Z (q : Q) (z : Z) : inject_Z z < q (z < Qceiling q)%Z.
Proof.
assert (A : (x y : Q), not (x y)%Q (y < x)%Q).
+ intros; split; [apply Qnot_le_lt | apply Qlt_not_le].
+ assert (A1 := Zle_Qle_Qceiling q z). apply Z.iff_not in A1.
  now rewrite A, Z.nle_gt in A1.
Qed.

Lemma Qlt_lt_of_nat_inject_Z (q : Q) (n : nat) :
  inject_Z (Z.of_nat n) < q (n < Z.to_nat (Qceiling q))%nat.
Proof. rewrite (Qlt_Zlt_inject_Z q (Z.of_nat n)); apply Z.lt_Zlt_to_nat. Qed.

NoDup isn't /directly/ useful for Q because Q does not use a canonical representation and NoDup doesn't support setoid equalities such as Qeq. However, since we have Qred, which yields canonical representations, we can use:

Definition QNoDup (l: list Q): Prop := NoDup (map Qred l).

Instance: Proper (Qeq ==> eq) Qred.
Proof. repeat intro. apply Qred_complete. assumption. Qed.