Require Import Vbase Classical QArith.

Set Implicit Arguments.

Global Opaque Qred Qplus.

Lemma Qred_Qred x : Qred (Qred x) = Qred x.
Proof.
  by apply Qred_complete; rewrite Qred_correct.
Qed.

Lemma Qred_zero: Qred 0 = 0.
Proof.
  done.
Qed.

Lemma Qopp_zero: Qopp 0 = 0.
Proof.
  done.
Qed.

Lemma Qeq_weaken: ∀ (a b: Q), a = b → a == b.
Proof.
 ins; desf.
Qed.

Lemma Qplus_comm_red: ∀ a b, Qred (a + b) = Qred (b + a).
Proof.
  ins; apply Qred_complete, Qplus_comm.
Qed.

Lemma Qred_Qred_plus: ∀ a b, Qred (Qred a + b) = Qred (a + b).
Proof.
  by ins; apply Qred_complete; rewrite Qred_correct.
Qed.

Lemma Qred_Qred_plus2: ∀ a b, Qred (a + Qred b) = Qred (a + b).
Proof.
  by ins; apply Qred_complete; rewrite Qred_correct.
Qed.

Lemma Qplus_assoc_red: ∀ a b c, Qred (a + (b + c)) = Qred (a + b + c).
Proof.
  ins; apply Qred_complete, Qplus_assoc.
Qed.

Lemma Qplus_opp_l: ∀ q, Qopp q + q == 0.
Proof.
  by ins; rewrite Qplus_comm, Qplus_opp_r.
Qed.

Lemma adding_nonnegative_l: ∀ (a b c: Q), a + b ≤ c → a ≥ 0 → b ≤ c.
Proof.
  intros a b c LEQ POS.
  apply Qopp_le_compat in POS.
  specialize (Qplus_le_compat _ _ _ _ POS LEQ).
  by rewrite Qplus_assoc, Qplus_opp_l, Qopp_zero, !Qplus_0_l.
Qed.

Lemma adding_nonnegative_r: ∀ (a b c: Q), a + b ≤ c → b ≥ 0 → a ≤ c.
Proof.
  eby ins; rewrite Qplus_comm in *; eapply adding_nonnegative_l.
Qed.

Lemma nonnegative_sum: ∀ (a b: Q), a ≥ 0 → b ≥ 0 → a + b ≥ 0.
Proof.
  ins.
  rewrite <- (Qplus_0_l 0).
  by apply Qplus_le_compat.
Qed.

Lemma nonnegative_sum_eq_zero: ∀ (a b: Q), a ≥ 0 → b ≥ 0 → a + b == 0 → a == 0 ∧ b == 0.
Proof.
  ins. apply Qle_lt_or_eq in H; desf.
  × exfalso.
    exploit Qplus_lt_le_compat; eauto.
    rewrite Qplus_0_l; ins.
    eapply Qlt_not_eq; eauto.
    by symmetry.
  × split; try by symmetry.
    by rewrite <- H, Qplus_0_l in H1.
Qed.

Lemma Qopp_equal: ∀ (a b: Q), a == b ↔ -a == -b.
Proof.
  split; ins.
  × rewrite <- Qplus_inj_l. instantiate (1 := a); rewrite Qplus_opp_r.
    rewrite <- Qplus_inj_r. instantiate (1 := b); rewrite <- Qplus_assoc, Qplus_opp_l.
    by rewrite Qplus_0_l, Qplus_0_r; symmetry.
  × rewrite <- Qplus_inj_l. instantiate (1 := -a); rewrite Qplus_opp_l.
    rewrite <- Qplus_inj_r. instantiate (1 := -b); rewrite <- Qplus_assoc, Qplus_opp_r.
    by rewrite Qplus_0_l, Qplus_0_r; symmetry.
Qed.

Lemma Qneq a b: ¬ a == b → a < b ∨ b < a.
Proof.
  ins; apply NNPP; intro.
  destruct H; apply not_or_and in H0; desf.
  by apply Qle_antisym; apply Qnot_lt_le.
Qed.


Definition frac (a b: nat) := if (b == 0%nat)%bool then 0 else Z.of_nat a # Pos.of_nat b.

Lemma sum_halves a b: frac a (2 × b) + frac a (2 × b) == frac a b.
Proof.
  Transparent Qplus.
  unfold frac, Qplus; ins; desf; desf; rewrite Nat.add_0_r in ×.
    by apply Nat.eq_add_0 in Heq; desf.
  unfold Qeq; ins.
  rewrite <- Z.mul_add_distr_l, <- Z.mul_assoc.
  f_equal.
  rewrite Nat2Pos.inj_add; try done.
  by rewrite Pos2Z.inj_mul, Pos2Z.inj_add, !Z.mul_add_distr_r, !Z.mul_add_distr_l.
  Opaque Qplus.
Qed.

Lemma frac_plus_1: ∀ n, frac (n + 1) 1 == frac n 1 + 1.
Proof.
  Transparent Qplus.
  ins; unfold frac; desf; desf.
  unfold Qplus, Qeq; ins.
  by rewrite Nat2Z.inj_add, !Z.mul_1_r.
  Opaque Qplus.
Qed.

Lemma frac11: frac 1 1 == 1.
Proof.
  unfold frac; desf.
Qed.

Lemma Q_to_frac q : q ≥ 0 → ∃ a b, q == frac a b.
Proof.
  ins; destruct q.
  ∃ (Z.to_nat Qnum), (Pos.to_nat Qden).
  unfold frac; desf.
    by specialize (Pos2Nat.is_pos Qden); omega.
  rewrite Pos2Nat.id, Z2Nat.id; try done.
  by destruct Qnum.
Qed.