QuantumLib.RealAux
Supplement to Coq's axiomatized Reals
Open Scope R_scope.
Lemma Rle_minus_l : ∀ a b c,(a - c ≤ b ↔ a ≤ b + c).
Lemma Rlt_minus_r : ∀ a b c,(a < b - c ↔ a + c < b).
Lemma Rlt_minus_l : ∀ a b c,(a - c < b ↔ a < b + c).
Lemma Rle_minus_r : ∀ a b c,(a ≤ b - c ↔ a + c ≤ b).
Lemma Rminus_le_0 : ∀ a b, a ≤ b ↔ 0 ≤ b - a.
Lemma Rminus_lt_0 : ∀ a b, a < b ↔ 0 < b - a.
Lemma Rminus_unfold : ∀ r1 r2, (r1 - r2 = r1 + -r2).
Lemma Rdiv_unfold : ∀ r1 r2, (r1 / r2 = r1 ×/ r2).
Hint Rewrite Rminus_unfold Rdiv_unfold Ropp_0 Ropp_involutive Rplus_0_l
Rplus_0_r Rmult_0_l Rmult_0_r Rmult_1_l Rmult_1_r : R_db.
Hint Rewrite <- Ropp_mult_distr_l Ropp_mult_distr_r : R_db.
Hint Rewrite Rinv_l Rinv_r sqrt_sqrt using lra : R_db.
Notation "√ n" := (sqrt n) (at level 20) : R_scope.
Other useful facts
Lemma Rmult_div_assoc : ∀ (x y z : R), x × (y / z) = x × y / z.
Lemma Rmult_div : ∀ r1 r2 r3 r4 : R, r2 ≠ 0 → r4 ≠ 0 →
r1 / r2 × (r3 / r4) = r1 × r3 / (r2 × r4).
Lemma Rdiv_cancel : ∀ r r1 r2 : R, r1 = r2 → r / r1 = r / r2.
Lemma Rsum_nonzero : ∀ r1 r2 : R, r1 ≠ 0 ∨ r2 ≠ 0 → r1 × r1 + r2 × r2 ≠ 0.
Lemma Rpow_le1: ∀ (x : R) (n : nat), 0 ≤ x ≤ 1 → x ^ n ≤ 1.
Lemma Rle_pow_le1: ∀ (x : R) (m n : nat),
0 ≤ x ≤ 1 → (m ≤ n)%nat → x ^ n ≤ x ^ m.
Lemma pow2_sqrt : ∀ x:R, 0 ≤ x → (√ x) ^ 2 = x.
Lemma sqrt_pow : ∀ (r : R) (n : nat), (0 ≤ r)%R → (√ (r ^ n) = √ r ^ n)%R.
Lemma pow2_sqrt2 : (√ 2) ^ 2 = 2.
Lemma pown_sqrt : ∀ (x : R) (n : nat),
0 ≤ x → √ x ^ (S (S n)) = x × √ x ^ n.
Lemma sqrt_neq_0_compat : ∀ r : R, 0 < r → √ r ≠ 0.
Lemma sqrt_inv : ∀ (r : R), 0 < r → √ (/ r) = (/ √ r)%R.
Lemma sqrt2_div2 : (√ 2 / 2)%R = (1 / √ 2)%R.
Lemma sqrt2_inv : √ (/ 2) = (/ √ 2)%R.
Lemma sqrt_sqrt_inv : ∀ (r : R), 0 < r → (√ r × √ / r)%R = 1.
Lemma sqrt2_sqrt2_inv : (√ 2 × √ / 2)%R = 1.
Lemma sqrt2_inv_sqrt2 : ((√ / 2) × √ 2)%R = 1.
Lemma sqrt2_inv_sqrt2_inv : ((√ / 2) × (√ / 2) = /2)%R.
Lemma sqrt_1_unique : ∀ x, 1 = √ x → x = 1.
Lemma lt_ep_helper : ∀ (ϵ : R),
ϵ > 0 ↔ ϵ / √ 2 > 0.
Ltac R_field_simplify := repeat field_simplify_eq [pow2_sqrt2 sqrt2_inv].
Ltac R_field := R_field_simplify; easy.
Lemma sin_upper_bound_aux : ∀ x : R, 0 < x < 1 → sin x ≤ x.
Lemma sin_upper_bound : ∀ x : R, Rabs (sin x) ≤ Rabs x.
Hint Rewrite sin_0 sin_PI4 sin_PI2 sin_PI cos_0 cos_PI4 cos_PI2
cos_PI sin_neg cos_neg : trig_db.
Definition is_lower_bound (E:R → Prop) (m:R) := ∀ x:R, E x → m ≤ x.
Definition bounded_below (E:R → Prop) := ∃ m : R, is_lower_bound E m.
Definition is_glb (E:R → Prop) (m:R) :=
is_lower_bound E m ∧ (∀ b:R, is_lower_bound E b → b ≤ m).
Definition neg_Rset (E : R → Prop) :=
fun r ⇒ E (-r).
Lemma lb_negset_ub : ∀ (E : R → Prop) (b : R),
is_lower_bound E b ↔ is_upper_bound (neg_Rset E) (-b).
Lemma ub_negset_lb : ∀ (E : R → Prop) (b : R),
is_upper_bound E b ↔ is_lower_bound (neg_Rset E) (-b).
Lemma negset_bounded_above : ∀ (E : R → Prop),
bounded_below E → (bound (neg_Rset E)).
Lemma negset_glb : ∀ (E : R → Prop) (m : R),
is_lub (neg_Rset E) m → is_glb E (-m).
Lemma glb_completeness :
∀ E:R → Prop,
bounded_below E → (∃ x : R, E x) → { m:R | is_glb E m }.
Program Instance R_is_monoid : Monoid R :=
{ Gzero := 0
; Gplus := Rplus
}.
Solve All Obligations with program_simpl; try lra.
Program Instance R_is_group : Group R :=
{ Gopp := Ropp }.
Solve All Obligations with program_simpl; try lra.
Program Instance R_is_comm_group : Comm_Group R.
Solve All Obligations with program_simpl; lra.
Program Instance R_is_ring : Ring R :=
{ Gone := 1
; Gmult := Rmult
}.
Solve All Obligations with program_simpl; lra.
Program Instance R_is_comm_ring : Comm_Ring R.
Solve All Obligations with program_simpl; lra.
Program Instance R_is_field : Field R :=
{ Ginv := Rinv }.
Program Instance R_is_vector_space : Vector_Space R R :=
{ Vscale := Rmult }.
Solve All Obligations with program_simpl; lra.