| products/sources/formale sprachen/Coq/test-suite/success/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Sugar.thy Sprache: CoqOriginal von: Coq© |
|
||||||
|
Require Import Reals.
Axiom y : R -> R. Axiom d_y : derivable y. Axiom n_y : forall x : R, y x <> 0%R. Axiom dy_0 : derive_pt y 0 (d_y 0%R) = 1%R. Lemma essai0 : continuity_pt (fun x : R => ((x + 2) / y x + x / y x)%R) 0. assert (H := d_y). assert (H0 := n_y). reg. Qed. Lemma essai1 : derivable_pt (fun x : R => (/ 2 * sin x)%R) 1. reg. Qed. Lemma essai2 : continuity (fun x : R => (Rsqr x * cos (x * x) + x)%R). reg. Qed. Lemma essai3 : derivable_pt (fun x : R => (x * (Rsqr x + 3))%R) 0. reg. Qed. Lemma essai4 : derivable (fun x : R => ((x + x) * sin x)%R). reg. Qed. Lemma essai5 : derivable (fun x : R => (1 + sin (2 * x + 3) * cos (cos x))%R). reg. Qed. Lemma essai6 : derivable (fun x : R => cos (x + 3)). reg. Qed. Lemma essai7 : derivable_pt (fun x : R => (cos (/ sqrt x) * Rsqr (sin x + 1))%R) 1. reg. apply Rlt_0_1. red; intro; rewrite sqrt_1 in H; assert (H0 := R1_neq_R0); elim H0; assumption. Qed. Lemma essai8 : derivable_pt (fun x : R => sqrt (Rsqr x + sin x + 1)) 0. reg. rewrite sin_0. rewrite Rsqr_0. replace (0 + 0 + 1)%R with 1%R; [ apply Rlt_0_1 | ring ]. Qed. Lemma essai9 : derivable_pt (id + sin) 1. reg. Qed. Lemma essai10 : derivable_pt (fun x : R => (x + 2)%R) 0. reg. Qed. Lemma essai11 : derive_pt (fun x : R => (x + 2)%R) 0 essai10 = 1%R. reg. Qed. Lemma essai12 : derivable (fun x : R => (x + Rsqr (x + 2))%R). reg. Qed. Lemma essai13 : derive_pt (fun x : R => (x + Rsqr (x + 2))%R) 0 (essai12 0%R) = 5%R. reg. Qed. Lemma essai14 : derivable_pt (fun x : R => (2 * x + x)%R) 2. reg. Qed. Lemma essai15 : derive_pt (fun x : R => (2 * x + x)%R) 2 essai14 = 3%R. reg. Qed. Lemma essai16 : derivable_pt (fun x : R => (x + sin x)%R) 0. reg. Qed. Lemma essai17 : derive_pt (fun x : R => (x + sin x)%R) 0 essai16 = 2%R. reg. rewrite cos_0. reflexivity. Qed. Lemma essai18 : derivable_pt (fun x : R => (x + y x)%R) 0. assert (H := d_y). reg. Qed. Lemma essai19 : derive_pt (fun x : R => (x + y x)%R) 0 essai18 = 2%R. assert (H := dy_0). assert (H0 := d_y). reg. Qed. Axiom z : R -> R. Axiom d_z : derivable z. Lemma essai20 : derivable_pt (fun x : R => z (y x)) 0. reg. apply d_y. apply d_z. Qed. Lemma essai21 : derive_pt (fun x : R => z (y x)) 0 essai20 = 1%R. assert (H := dy_0). reg. Abort. Lemma essai22 : derivable (fun x : R => (sin (z x) + Rsqr (z x) / y x)%R). assert (H := d_y). reg. apply n_y. apply d_z. Qed. (* Pour tester la continuite de sqrt en 0 *) Lemma essai23 : continuity_pt (fun x : R => (sin (sqrt (x - 1)) + exp (Rsqr (sqrt x + 3)))%R) 1. reg. left; apply Rlt_0_1. right; unfold Rminus; rewrite Rplus_opp_r; reflexivity. Qed. Lemma essai24 : derivable (fun x : R => (sqrt (x * x + 2 * x + 2) + Rabs (x * x + 1))%R). reg. replace (x * x + 2 * x + 2)%R with (Rsqr (x + 1) + 1)%R. apply Rplus_le_lt_0_compat; [ apply Rle_0_sqr | apply Rlt_0_1 ]. unfold Rsqr; ring. red; intro; cut (0 < x * x + 1)%R. intro; rewrite H in H0; elim (Rlt_irrefl _ H0). apply Rplus_le_lt_0_compat; [ replace (x * x)%R with (Rsqr x); [ apply Rle_0_sqr | reflexivity ] | apply Rlt_0_1 ]. Qed. ¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
