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.
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+.
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.
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.
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.
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.
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.
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.
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.
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.
Next Obligation. auto with qarith. Qed.
Notation "1" := Qpos_one : Qpos_scope.
Lemma Q_Qpos_one : (1%Q+:Q)=(1:Q).
Proof. trivial. Qed.
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.
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.
Ltac QposRing :=
unfold canonical_names.equiv, QposEq;
autorewrite with QposElim;
ring.
Ltac QposField :=
unfold canonical_names.equiv, QposEq;
autorewrite with QposElim;
field.
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.
a< b →
{c:Q+ | b==(a+c)}.
Proof.
intros.
assert (0<b-a).
apply: shift_zero_less_minus.
assumption.
∃ (mkQpos H0).
QposRing.
Defined.
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.
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.
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.
(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.
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.
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.