Require Import intervals rescale tactic syntax.
Require taylor chebyshev approx.
Import IPrimFloat.
Notation "x ∈ X" := (Icontains X x) (at level 80).
Definition f {C: Ops1} (x: C): C := sqrt (pi + x * x).
Eval simpl in @f ROps1 5%R.
Compute @f FOps1 5%float.
Compute @f IOps1 (fromQ 5).
Lemma rf C D (R: Rel1 C D): forall x y, R x y -> R (f x) (f y).
Proof.
intros x y H. unfold f.
apply rsqrt.
apply radd.
apply rpi.
apply rmul.
assumption.
assumption.
Restart.
intros. rel.
Qed.
Check IRel1. (* `` ROps is related to IOps via ∈ '' *)
Lemma rf' x X: x ∈ X -> f x ∈ f X.
Proof.
apply rf.
Qed.
Definition t (x: I) := (x * x + fromZ 2) / (fromZ 2 * x).
Definition r (x: I) := abs (x - t x) / (1 - fromQ 0.12).
Compute r (fromQ 1.41421356).
(** the tactic [approx] solves conjunctions of inequations (<,<=,<>)
it supports the following operations on reals:
+, -, *, /, sqrt, cos, abs, 0, 1, pi, fromZ, fromQ
as well as integration of univariate functions built from
+, -, *, /, sqrt, and constant expressions as above
*)
Goal 1.4 <= sqrt 2 <= 1.5.
Proof.
approx.
Qed.
Goal sqrt 2 < 1.5 /\ -1 <= cos pi.
Proof.
approx.
Qed.
Goal 0.3333 <= RInt (fun x => x*x) 0 1 <= 0.3334.
Proof.
approx.
Qed.
Goal 1.578 <= RInt (fun x => sqrt (2+x)) 0 1 <= 1.579.
Proof.
approx.
Qed.
Goal 0.1249 <= RInt (fun x => sin x * cos x) (pi/4) (pi/3) <= 0.1251.
approx fourier.
Qed.
(** [approx] also makes it possible to compare
univariate functions on a given interval
*)
Goal forall x, 0.1<=x<=0.9 -> x < sqrt x.
approx.
Qed.
Goal forall x, 0.1<=x<=0.9 -> x <> sqrt x.
approx.
Qed.
Goal forall x, 0.001<=x<=0.999 -> x <> sqrt x.
approx (i_deg 70).
Qed.
Goal forall x, 0.001<=x<=0.5 -> x <> sqrt x.
approx (i_deg 30).
Qed.
Goal forall x, 0.5<=x<=0.999 -> x <> sqrt x.
approx (i_deg 50).
Qed.
(** the tactic [estimate e] makes it possible to compute and print
an interval enclosing the expression [e]
this would typically be the estimation used by the [approx] tactic.
*)
Goal True.
estimate (RInt (fun t => (1+t)/(sqrt (pi+t))) 0 (sqrt 2)).
estimate (RInt (fun t => (1+t)/(sqrt (pi+t))) 0 (sqrt 2)) (i_deg 50).
estimate (RInt (fun x => sqrt (1+x)) (-1) 1).
estimate (RInt (fun x => sin x * cos x) (pi/4) (pi/3)) fourier.
estimate (RInt (fun x => sin x / (2+cos x)) 0 pi) (fourier, i_deg 50).
estimate (RInt (fun x => sin x / (2+cos x)) 0 pi) (fourier, i_deg 10, bigint120).
estimate (RInt (fun x => x * sin x) 0 pi) (fourier).
Abort.