CoRN.model.structures.Qpossec

Require Export QArith.
Require Import Qpower.
Require Import Qordfield.
Require Import COrdFields2.
Require Import Eqdep_dec.
Require Import CornTac.
Require Import Qround.
Require Import Qabs.
Require Import stdlib_omissions.Q.

Open Local Scope Q_scope.

Q⁺

Definition Q⁺: Set := sig (Qlt 0).

Program Definition QposMake (num den: positive): Q⁺ := num # den.
Next Obligation. auto with ×. Qed.

Notation "a # b" := (QposMake a b) (at level 55, no associativity) : Qpos_scope.

Bind Scope Qpos_scope with Q⁺.
Delimit Scope Qpos_scope with Q⁺.

Program Definition integral_Qpos (p: positive): Q⁺ := (p:Q).

Coercion integral_Qpos: positive >-> Q⁺.

There is an injection from Q⁺ to Q that we make into a coercion.

Definition QposAsQ: Q⁺ → Q := @proj1_sig _ _.

Coercion QposAsQ : Q⁺ >-> Q.

Basic properties about Q⁺

Definition Qpos_prf : ∀ a:Q⁺, 0 < a := @proj2_sig _ _.

Hint Immediate Qpos_prf.

Lemma Qpos_nonzero : ∀ x:Q⁺, (x:Q )[#]0.
Proof.
intros ?.
apply: pos_ap_zero.
apply Qpos_prf.
Qed.

Lemma Qpos_nonzero' (q: Q⁺): ¬ q == 0.
Proof. apply Qpos_nonzero. Qed.

Hint Immediate Qpos_nonzero'.

Lemma Qpos_nonneg : ∀ a:Q⁺, 0 ≤ a.
Proof. intros [??]. auto with ×. Qed.

Hint Immediate Qpos_nonneg.

Lemma Qopp_Qpos_neg (x: Q⁺): -x < 0.
Proof. apply Qopp_Qlt_0_r. auto. Qed.

Hint Immediate Qopp_Qpos_neg.

Any positive rational number can be transformed into a Q⁺.

Definition mkQpos: ∀ (a:Q) (p:0 < a), Q⁺ := @exist Q (Qlt 0).

Lemma QposAsmkQpos : ∀ (a:Q) (p:0<a), (QposAsQ (mkQpos p))=a.
Proof.
intros [[|an|an] ad] p.
   discriminate.
  reflexivity.
discriminate.
Qed.

Lemma positive_Z (z: Z): Zlt 0 z → sig (fun p: positive ⇒ Zpos p = z).
destruct z; intros.
   intros.
   elim (Zlt_irrefl _ H).
  ∃ p.
  reflexivity.
exfalso.
apply (Zlt_asym _ _ H).
auto with ×.
Defined.

Require Eqdep_dec.
Definition comparison_eq_dec (a b: comparison): { a = b } + { a ≠ b }.
destruct a, b; try (left; reflexivity); try (right; discriminate).
Defined.

Lemma Zlt_uniq (a b: Z) (p q: (a < b)%Z): p = q.
Proof.
unfold Zlt in ×. destruct p. intros.
apply (Eqdep_dec.K_dec_set comparison_eq_dec).
reflexivity.
Qed.

Lemma Qlt_uniq (a b: Q) (p q: a < b): p = q.
Proof. intros. apply Zlt_uniq. Qed.

Program Definition Qpos_as_positive_ratio (q: Q⁺):
  sig (fun ps: positive × positive ⇒ q = QposMake (fst ps) (snd ps)) :=
  (positive_Z (Qnum q) _, Qden q ).

Next Obligation.
destruct q as [[??] ?]. unfold Qlt in ×. simpl in ×. auto with ×.
Qed.

Next Obligation.
destruct q as [[??] ?]. simpl.
destruct positive_Z. simpl.
subst. unfold QposMake.
f_equal. apply Qlt_uniq.
Qed.

Lemma Qpos_positive_numerator_rect (P: Q⁺ → Type):
  (∀ (a b: positive), P (a # b)%Q⁺) → ∀ q, P q.
Proof.
intros H q.
destruct (Qpos_as_positive_ratio q).
subst.
apply H.
Defined.

Lemma QposAsQposMake : ∀ a b, (QposAsQ (QposMake a b)) = (Zpos a )#b.
Proof.
trivial.
Qed.

Equality

Definition QposEq (a b:Q⁺) := Qeq a b.
Instance Qpos_default : @DefaultRelation Q⁺ QposEq | 2.

Add Relation Q⁺ QposEq
reflexivity proved by (fun (x:Q⁺) ⇒ Qeq_refl x)
symmetry proved by (fun (x y:Q⁺) ⇒ Qeq_sym x y)
transitivity proved by (fun (x y z:Q⁺) ⇒ Qeq_trans x y z) as QposSetoid.

Definition QposAp (a b:Q⁺) := Qap a b.

Definition Qpos_PI (a b: Q⁺): (a: Q ) = b → a = b.
Proof.
destruct a, b.
simpl. intros. subst.
f_equal. apply Qlt_uniq.
Qed.

Addition

Program Definition Qpos_plus (x y:Q⁺) : Q⁺ := Qplus x y.

Next Obligation.
apply: plus_resp_pos; apply Qpos_prf.
Qed.

Infix "+" := Qpos_plus : Qpos_scope.
Lemma Q_Qpos_plus : ∀ (x y:Q⁺), ((x + y)%Q⁺:Q )=(x:Q )+(y:Q ).
Proof.
trivial.
Qed.

One

Program Definition Qpos_one : Q⁺ := 1.
Next Obligation. auto with qarith. Qed.
Notation "1" := Qpos_one : Qpos_scope.

Lemma Q_Qpos_one : (1%Q⁺:Q )=(1:Q ).
Proof. trivial. Qed.

Multiplication

Program Definition Qpos_mult (x y:Q⁺) : Q⁺ := Qmult x y.

Infix "×" := Qpos_mult : Qpos_scope.
Lemma Q_Qpos_mult : ∀ (x y:Q⁺), ((x × y)%Q⁺:Q )=(x:Q )*(y:Q ).
Proof.
trivial.
Qed.

Inverse

Program Definition Qpos_inv (x:Q⁺): Q⁺ := / x.

Next Obligation.
apply Qinv_lt_0_compat.
destruct x.
assumption.
Qed.

Lemma Q_Qpos_inv : ∀ (x:Q⁺), Qpos_inv x = / x :> Q.
Proof.
trivial.
Qed.
Hint Rewrite Q_Qpos_inv : QposElim.

Notation "a / b" := (Qpos_mult a (Qpos_inv b)) : Qpos_scope.

Tactics

These tactics solve Ring and Field equations over Q⁺ by converting them to problems over Q.

Ltac QposRing :=
unfold canonical_names.equiv, QposEq;
autorewrite with QposElim;
ring.

Ltac QposField :=
unfold canonical_names.equiv, QposEq;
autorewrite with QposElim;
field.

This is a standard way of decomposing a rational b that is greater than a into a plus a positive value c.

Lemma Qpos_lt_plus : ∀ (a b:Q),
a < b →
{c:Q⁺ | b ==(a +c)}.
Proof.
intros.
assert (0<b-a).
apply: shift_zero_less_minus.
assumption.
∃ (mkQpos H0).
QposRing.
Defined.

Power

Lemma Qpos_power_pos : ∀ (x:Q⁺) z, 0 < x ^z.
Proof.
intros x z.
destruct (Qle_lt_or_eq _ _ (Qpower_pos x z (Qlt_le_weak _ _ (Qpos_prf x))));[assumption|].
destruct z.
   discriminate H.
  elim (Qpower_not_0_positive x p).
   apply Qpos_nonzero.
  symmetry; assumption.
elim (Qpower_not_0_positive (/x) p).
  change (¬(Qpos_inv x) == 0).
  apply Qpos_nonzero.
change ((/x)^p==0).
rewrite → Qinv_power.
symmetry; assumption.
Qed.

Definition Qpos_power (x:Q⁺) (z:Z) : Q⁺.
Proof.
apply mkQpos with (x^z).
apply Qpos_power_pos.
Defined.

Infix "^" := Qpos_power : Qpos_scope.
Lemma Q_Qpos_power : ∀ (x:Q⁺) z, ((x ^z)%Q⁺:Q )==(x:Q )^z.
Proof.
intros.
unfold Qpos_power.
autorewrite with QposElim.
reflexivity.
Qed.
Hint Rewrite Q_Qpos_power : QposElim.

Summing lists

Definition QposSum (l:list Q⁺) : Q := fold_right
(fun (x:Q⁺) (y:Q) ⇒ x +y) ([0]:Q) l.

Lemma QposSumNonNeg : ∀ l, 0 ≤ QposSum l.
Proof.
induction l.
  apply: leEq_reflexive.
simpl.
apply: plus_resp_nonneg.
  apply: less_leEq.
  apply Qpos_prf.
assumption.
Qed.

A version of Qred for Q⁺.

Lemma QposRed_prf : ∀ (a:Q), (0 < a) → (0 < Qred a).
Proof.
intros a Ha.
rewrite → Qred_correct.
assumption.
Qed.

Definition QposRed (a:Q⁺) : Q⁺ := mkQpos (QposRed_prf a (Qpos_prf a)).

Instance QposRed_complete: Proper (QposEq ==> eq) QposRed.
Proof.
intros p q H.
unfold QposRed.
generalize (QposRed_prf p (Qpos_prf p)).
generalize (QposRed_prf q (Qpos_prf q)).
rewrite (Qred_complete p q H).
unfold Qlt, Zlt.
intros A B.
assert (X:∀ x y : comparison, x = y ∨ x ≠ y).
  decide equality.
rewrite (eq_proofs_unicity X A B).
reflexivity.
Qed.

Lemma QposRed_correct : ∀ p, QposRed p == p.
Proof.
unfold QposRed.
intros p.
simpl.
apply Qred_correct.
Qed.

Definition QposCeiling (q: Q⁺): positive :=
  match Qceiling q with
  | Zpos p ⇒ p
  | _ ⇒ 1%positive
  end.

Lemma QposCeiling_Qceiling (q: Q⁺): (QposCeiling q: Z ) = Qceiling q.
Proof with auto with ×.
unfold QposCeiling.
pose proof Qle_ceiling q.
destruct (Qceiling q); try reflexivity; exfalso; destruct q; simpl in ×.
  apply (Qlt_not_le 0 x q)...
apply (Qlt_irrefl 0).
apply Qlt_le_trans with x...
apply Qle_trans with (Zneg p)...
Qed.

Definition QabsQpos (x : Q) : Q⁺ :=
  match x with
  | 0 # _ ⇒ (1%Q⁺)
  | (Zpos an) # ad ⇒ (an # ad)%Q⁺
  | (Zneg an) # ad ⇒ (an # ad)%Q⁺
  end.

Lemma QabsQpos_correct x : ¬x == 0 → QabsQpos x == Qabs x.
Proof with auto with qarith.
intros E. destruct x as [n d]. simpl.
destruct n...
destruct E...
Qed.

Lemma QabsQpos_Qpos (x : Q⁺) : QposEq (QabsQpos x) x.
Proof with auto with qarith.
unfold QposEq.
rewrite QabsQpos_correct...
apply Qabs_pos...
Qed.